Alphabet
f
:
[nat × nat] ⟶ nat
g
:
[nat → nat] ⟶ nat
Variables
X
:
nat → nat
Rules
f
(
g
(
X
),
g
(
X
))
⇒
X
·
g
(
X
)