Alphabet
0
:
a
rec
:
(b → (a → c) → a → c) → c → a → c
s
:
b → b
Variables
F
:
a → c
Z
:
b → (a → c) → a → c
G
:
b → c
H
:
b → (a → c) → a → c
W
:
b
Rules
rec
·
Z
· (
F
·
0
)
⇒
F
rec
·
H
· (
G
· (
s
·
W
))
⇒
H
·
W
· (
rec
·
H
· (
G
·
W
))