Alphabet
rec
:
N → a → (N → a → a) → a
s
:
N → N
z
:
N
Variables
X
:
a
Z
:
N → a → a
U
:
N
V
:
a
I
:
N → a → a
Rules
rec
·
z
·
X
· (λ
%X
:N.
Z
·
%X
)
⇒
X
rec
· (
s
·
U
) ·
V
· (λ
%Y
:N.
I
·
%Y
)
⇒
I
·
U
· (
rec
·
U
·
V
· (λ
%Z
:N.
I
·
%Z
))