0 :: c
cons :: c → b → b
map :: (c → c) → b → b
nil :: b
node :: a → b → c
plus :: c → c → c
s :: c → c
size :: c → c
sum :: b → c
map(F, nil) → nil
map(Z, cons(U, V)) → cons(Z(U), map(Z, V))
sum(cons(W, P)) → plus(W, sum(P))
size(node(X1, Y1)) → s(sum(map(size, Y1)))
plus(0, U1) → 0
plus(s(V1), W1) → s(plus(V1, W1))