| 0 | : | b |
| 1 | : | b |
| cons | : | [e × f] ⟶ f |
| f | : | [c] ⟶ a |
| false | : | d |
| filter | : | [e → d × f] ⟶ f |
| filter2 | : | [d × e → d × e × f] ⟶ f |
| g | : | [b × b] ⟶ c |
| map | : | [e → e × f] ⟶ f |
| nil | : | f |
| s | : | [b] ⟶ c |
| true | : | d |
| X | : | b |
| Z | : | e → e |
| G | : | e → e |
| V | : | e |
| W | : | f |
| J | : | e → d |
| F1 | : | e → d |
| Y1 | : | e |
| U1 | : | f |
| H1 | : | e → d |
| W1 | : | e |
| P1 | : | f |
| F2 | : | e → d |
| Y2 | : | e |
| U2 | : | f |
| f(s(X)) | ⇒ | f(g(X, X)) |
| g(0, 1) | ⇒ | s(0) |
| 0 | ⇒ | 1 |
| map(Z, nil) | ⇒ | nil |
| map(G, cons(V, W)) | ⇒ | cons(G · V, map(G, W)) |
| filter(J, nil) | ⇒ | nil |
| filter(F1, cons(Y1, U1)) | ⇒ | filter2(F1 · Y1, F1, Y1, U1) |
| filter2(true, H1, W1, P1) | ⇒ | cons(W1, filter(H1, P1)) |
| filter2(false, F2, Y2, U2) | ⇒ | filter(F2, U2) |