Alphabet
f
:
[nat × nat → nat] ⟶ nat
0
:
nat
1
:
nat
Variables
F
:
nat → nat
Rules
f
(
0
,
F
)
⇒
F
·
f
(
F
·
1
,
F
)