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