Alphabet

append:[a × a] ⟶ a
concat:[a] ⟶ a
cons:[a × a] ⟶ a
flatten:a → a
map:[a → a × a] ⟶ a
nil:a
node:[a × a] ⟶ a

Variables

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

Rules

map(F, nil)⇒nil
map(Z, cons(U, V))⇒cons(Z · U, map(Z, V))
flatten · node(W, P)⇒cons(W, concat(map(flatten, P)))
concat(nil)⇒nil
concat(cons(X1, Y1))⇒append(X1, concat(Y1))
append(nil, U1)⇒U1
append(cons(V1, W1), P1)⇒cons(V1, append(W1, P1))