Alphabet
0
:
a
rec
:
[a → b → b × b × a] ⟶ b
s
:
[a] ⟶ a
Variables
F
:
a → b → b
Y
:
b
G
:
a → b → b
V
:
b
W
:
a
Rules
rec
(
F
,
Y
,
0
)
⇒
Y
rec
(
G
,
V
,
s
(
W
))
⇒
G
·
s
(
W
) ·
rec
(
G
,
V
,
W
)