Alphabet

0:b
cons:[b × a] ⟶ a
curry:[b → b → b × b] ⟶ b → b
double:a → a
inc:a → a
map:[b → b] ⟶ a → a
nil:a
plus:b → b → b
s:[b] ⟶ b
times:b → b → b

Variables

X:b
Y:b
U:b
V:b
W:b
P:b
F1:b → b → b
Y1:b
U1:b
H1:b → b
I1:b → b
P1:b
X2:a

Rules

plus · 0 · X⇒X
plus · s(Y) · U⇒s(plus · Y · U)
times · 0 · V⇒0
times · s(W) · P⇒plus · (times · W · P) · P
curry(F1, Y1) · U1⇒F1 · Y1 · U1
map(H1) · nil⇒nil
map(I1) · cons(P1, X2)⇒cons(I1 · P1, map(I1) · X2)
inc⇒map(curry(plus, s(0)))
double⇒map(curry(times, s(s(0))))