Alphabet

0:c
cons:[a × b] ⟶ b
div:[c × c] ⟶ c
map:[a → a × b] ⟶ b
minus:[c × c] ⟶ c
nil:b
p:[c] ⟶ c
s:[c] ⟶ c

Variables

F:a → a
Z:a → a
U:a
V:b
W:c
P:c
X1:c
Y1:c
U1:c
V1:c
W1:c

Rules

map(F, nil)⇒nil
map(Z, cons(U, V))⇒cons(Z · U, map(Z, V))
minus(W, 0)⇒W
minus(s(P), s(X1))⇒minus(p(s(P)), p(s(X1)))
p(s(Y1))⇒Y1
div(0, s(U1))⇒0
div(s(V1), s(W1))⇒s(div(minus(V1, W1), s(W1)))