Alphabet

0:nat
rec:nat → nat → (nat → nat → nat) → nat
s:nat → nat
xplus:nat → nat → nat
xtimes:nat → nat → nat

Variables

X:nat
Y:nat
U:nat
V:nat
I:nat → nat → nat
P:nat
X1:nat
Z1:nat → nat → nat
U1:nat
V1:nat

Rules

xplus · X · 0⇒X
xplus · Y · (s · U)⇒s · (xplus · Y · U)
rec · 0 · V · (λ%Y:nat.λ%X:nat.I · %Y · %X)⇒V
rec · (s · P) · X1 · (λ%U:nat.λ%Z:nat.Z1 · %U · %Z)⇒Z1 · P · (rec · P · X1 · (λ%W:nat.λ%V:nat.Z1 · %W · %V))
xtimes · U1 · V1⇒rec · V1 · 0 · (λ%G:nat.λ%F:nat.xplus · U1 · %F)