Alphabet

0:nat
plus:[nat × nat] ⟶ nat
rec:[nat × nat × nat → nat → nat] ⟶ nat
s:[nat] ⟶ nat
succ:nat → nat → nat
xap:[nat → nat → nat × nat] ⟶ nat → nat
yap:[nat → 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
H1:nat → nat → nat
W1:nat
J1:nat → nat
X2:nat

Rules

rec(0, X, λ%X:nat.λ%Y:nat.yap(xap(Z, %X), %Y))⇒X
rec(s(U), V, λ%Z:nat.λ%U:nat.yap(xap(I, %Z), %U))⇒yap(xap(I, U), rec(U, V, λ%V:nat.λ%W:nat.yap(xap(I, %V), %W)))
succ · P · X1⇒s(X1)
plus(Y1, U1)⇒rec(Y1, U1, succ)
xap(H1, W1)⇒H1 · W1
yap(J1, X2)⇒J1 · X2