Alphabet

comp:[c → c × c → c] ⟶ c → c
cons:[a × b] ⟶ b
map:[a → a × b] ⟶ b
nil:b
twice:[c → c] ⟶ c → c

Variables

F:a → a
Z:a → a
U:a
V:b
I:c → c
J:c → c
X1:c
Z1:c → c

Rules

map(F, nil)⇒nil
map(Z, cons(U, V))⇒cons(Z · U, map(Z, V))
comp(I, J) · X1⇒I · (J · X1)
twice(Z1)⇒comp(Z1, Z1)