Alphabet

0:nat
mult:nat → nat → nat
plus:nat → nat → nat
plus3:nat → nat → nat → nat
rec:nat → nat → (nat → nat → nat) → nat
s:nat → nat
succ2: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
V1:nat
W1:nat
P1:nat
X2:nat
Y2: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))
succ2 · P · X1⇒s · X1
plus · Y1 · U1⇒rec · Y1 · U1 · (λ%G:nat.λ%F:nat.succ2 · %G · %F)
plus3 · V1 · W1 · P1⇒plus · V1 · (plus · W1 · P1)
mult · X2 · Y2⇒rec · X2 · 0 · (λ%I:nat.λ%H:nat.plus3 · Y2 · %I · %H)