| 0 | : | a |
| cons | : | [a × b] ⟶ b |
| double | : | [b] ⟶ b |
| inc | : | [b] ⟶ b |
| map | : | [a → a × b] ⟶ b |
| nil | : | b |
| plus | : | [a] ⟶ a → a |
| s | : | [a] ⟶ a |
| times | : | [a] ⟶ a → a |
| X | : | a |
| Y | : | a |
| U | : | a |
| V | : | a |
| W | : | a |
| P | : | a |
| X1 | : | b |
| Y1 | : | b |
| G1 | : | a → a |
| H1 | : | a → a |
| W1 | : | a |
| P1 | : | b |
| plus(0) · X | ⇒ | X |
| plus(s(Y)) · U | ⇒ | s(plus(Y) · U) |
| times(0) · V | ⇒ | 0 |
| times(s(W)) · P | ⇒ | plus(times(W) · P) · P |
| inc(X1) | ⇒ | map(plus(s(0)), X1) |
| double(Y1) | ⇒ | map(times(s(s(0))), Y1) |
| map(G1, nil) | ⇒ | nil |
| map(H1, cons(W1, P1)) | ⇒ | cons(H1 · W1, map(H1, P1)) |