Alphabet

0:c
cons:[a × b] ⟶ b
div:[c × c] ⟶ c
map:[a → a × b] ⟶ b
minus:[c × c] ⟶ c
nil:b
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

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, X1)
div(0, s(Y1))⇒0
div(s(U1), s(V1))⇒s(div(minus(U1, V1), s(V1)))