Alphabet
0
:
nat
I
:
[nat] ⟶ nat
s
:
[nat] ⟶ nat
twice
:
[nat → nat] ⟶ nat → nat
Variables
X
:
nat
Z
:
nat → nat
Rules
I
(
0
)
⇒
0
I
(
s
(
X
))
⇒
s
(
twice
(λ
%X
:nat.
I
(
%X
)) ·
X
)
twice
(
Z
)
⇒
λ
%Y
:nat.
Z
· (
Z
·
%Y
)