Alphabet

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

Variables

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

Rules

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