Alphabet
0
:
nat
f
:
[nat] ⟶ nat
g
:
[nat → nat] ⟶ nat
Variables
F
:
nat → nat
Rules
f
(
0
)
⇒
g
(λ
x
:nat.
0
)
g
(
F
)
⇒
F
·
f
(
0
)