| 0 | : | a |
| eq | : | [a × a] ⟶ c |
| false | : | c |
| fork | : | [b × a × b] ⟶ b |
| if | : | [c × c × c] ⟶ c |
| lt | : | [a × a] ⟶ c |
| member | : | [a × b] ⟶ c |
| null | : | b |
| s | : | [a] ⟶ a |
| true | : | c |
| X | : | a |
| Y | : | a |
| U | : | a |
| V | : | a |
| W | : | a |
| P | : | a |
| X1 | : | a |
| Y1 | : | a |
| U1 | : | a |
| V1 | : | b |
| W1 | : | a |
| P1 | : | b |
| lt(s(X), s(Y)) | ⇒ | lt(X, Y) |
| lt(0, s(U)) | ⇒ | true |
| lt(V, 0) | ⇒ | false |
| eq(W, W) | ⇒ | true |
| eq(s(P), 0) | ⇒ | false |
| eq(0, s(X1)) | ⇒ | false |
| member(Y1, null) | ⇒ | false |
| member(U1, fork(V1, W1, P1)) | ⇒ | if(lt(U1, W1), member(U1, V1), if(eq(U1, W1), true, member(U1, P1))) |