Alphabet

0:nat
rec:[nat × a × nat → a → a] ⟶ a
s:[nat] ⟶ nat
xap:[nat → a → a × nat] ⟶ a → a
yap:[a → a × a] ⟶ a

Variables

X:a
Z:nat → a → a
U:nat
V:a
I:nat → a → a
J:nat → a → a
X1:nat
Z1:a → a
U1:a

Rules

rec(0, X, λ%X:nat.λ%Y:a.yap(xap(Z, %X), %Y))⇒X
rec(s(U), V, λ%Z:nat.λ%U:a.yap(xap(I, %Z), %U))⇒yap(xap(I, U), rec(U, V, λ%V:nat.λ%W:a.yap(xap(I, %V), %W)))
xap(J, X1)⇒J · X1
yap(Z1, U1)⇒Z1 · U1