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
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)))