| compose | : | [a → a × a → a] ⟶ a → a |
| cons | : | [a × a] ⟶ a |
| hd | : | a → a |
| init | : | a → a |
| last | : | a → a |
| nil | : | a |
| reverse | : | a → a |
| reverse2 | : | [a × a] ⟶ a |
| tl | : | a → a |
| 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 |
| compose(F, Z) · U | ⇒ | Z · (F · U) |
| reverse · V | ⇒ | reverse2(V, nil) |
| reverse2(nil, W) | ⇒ | W |
| reverse2(cons(X1, Y1), P) | ⇒ | reverse2(Y1, cons(X1, P)) |
| hd · cons(U1, V1) | ⇒ | U1 |
| tl · cons(W1, P1) | ⇒ | P1 |
| last | ⇒ | compose(hd, reverse) |
| init | ⇒ | compose(reverse, compose(tl, reverse)) |