Alphabet
0
:
o
a
:
o
f
:
[o → o] ⟶ o
g
:
[o] ⟶ o
h
:
[o × o] ⟶ o
s
:
[o] ⟶ o
Variables
X
:
o
Y
:
o
U
:
o
V
:
o
Rules
a
⇒
f
(λ
%X
:o.
g
(
%X
))
f
(λ
%Y
:o.
X
)
⇒
a
g
(
Y
)
⇒
h
(
Y
,
Y
)
h
(
0
,
U
)
⇒
U
h
(
s
(
V
),
0
)
⇒
g
(
V
)