Alphabet

0:b
cons:[b × a] ⟶ a
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
Z1:b → b
U1:b
V1: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
map(F1) · nil⇒nil
map(Z1) · cons(U1, V1)⇒cons(Z1 · U1, map(Z1) · V1)
inc⇒map(plus(s(0)))
double⇒map(times(s(s(0))))