Alphabet

0:nat
plus:nat → nat → nat
rec:nat → nat → (nat → nat → nat) → nat
s:nat → nat
succ:nat → nat → nat

Variables

X:nat
Z:nat → nat → nat
U:nat
V:nat
I:nat → nat → nat
P:nat
X1:nat
Y1:nat
U1:nat

Rules

rec · 0 · X · (λ%Y:nat.λ%X:nat.Z · %Y · %X)⇒X
rec · (s · U) · V · (λ%U:nat.λ%Z:nat.I · %U · %Z)⇒I · U · (rec · U · V · (λ%W:nat.λ%V:nat.I · %W · %V))
succ · P · X1⇒s · X1
plus · Y1 · U1⇒rec · Y1 · U1 · (λ%G:nat.λ%F:nat.succ · %G · %F)