Alphabet

0:a
lim:[a → a] ⟶ a
n:a
rec:[b × a → b → b × (a → a) → b → b × a] ⟶ b
rectuv:[b × a → b → b × (a → a) → b → b × a] ⟶ b
s:[a] ⟶ a

Variables

X:b
Z:a → b → b
G:(a → a) → b → b
V:b
I:a → b → b
J:(a → a) → b → b
X1:a
Z1:a → a
U1:b
H1:a → b → b
I1:(a → a) → b → b
P1:b
F2:a → b → b
Z2:(a → a) → b → b

Rules

rec(X, Z, G, 0)⇒X
rec(V, I, J, s(X1))⇒I · X1 · rec(V, I, J, X1)
rec(U1, H1, I1, lim(Z1))⇒I1 · Z1 · rectuv(U1, H1, I1, Z1 · n)
rectuv(P1, F2, Z2, n)⇒rec(P1, F2, Z2, n)