0 :: c
cons :: a → b → b
div :: c → c → c
map :: (a → a) → b → b
minus :: c → c → c
nil :: b
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, X1)
div(0, s(Y1)) → 0
div(s(U1), s(V1)) → s(div(minus(U1, V1), s(V1)))