Alphabet
s
:
[nat] ⟶ nat
I
:
[nat] ⟶ nat
0
:
nat
Variables
X
:
nat
Rules
I
(
s
(
X
))
⇒
s
((λ
Z
:nat -> nat.λ
x46
:nat.
Z
· (
Z
·
x46
)) · (λ
x45
:nat.
I
(
x45
)) ·
X
)
I
(
0
)
⇒
0