Alphabet
f
:
[N → N × N] ⟶ N
h
:
[N] ⟶ N
g
:
N → N
Variables
X
:
N
F
:
N → N
Rules
f
(
g
,
X
)
⇒
h
(
X
)
f
(
F
,
X
)
⇒
F
·
X
h
(
X
)
⇒
f
(λ
z
:N.
z
,
X
)