Alphabet
f
:
[nat × nat × nat] ⟶ nat
g
:
[nat × nat → nat] ⟶ nat
h
:
[nat × nat] ⟶ nat
s
:
[nat] ⟶ nat
Variables
X
:
nat
Y
:
nat
U
:
nat
Rules
f
(
X
,
Y
,
s
(
U
))
⇒
g
(
h
(
X
,
Y
), λ
%X
:nat.
f
(
%X
,
X
,
U
))
h
(
X
,
X
)
⇒
f
(
X
,
s
(
X
),
s
(
s
(
X
)))