Alphabet
A
:
[term × term] ⟶ term
L
:
[term → term] ⟶ term
V
:
[term] ⟶ term
noabs
:
[term] ⟶ term
Variables
X
:
term
Y
:
term
Z
:
term → term
Rules
noabs
(
A
(
X
,
Y
))
⇒
A
(
noabs
(
X
),
noabs
(
Y
))
noabs
(
V
(
X
))
⇒
V
(
X
)
A
(
L
(
Z
),
Y
)
⇒
Z
·
noabs
(
Y
)