| le(0, X) | ⇒ | true
|
| le(s(Y), 0) | ⇒ | false
|
| le(s(U), s(V)) | ⇒ | le(U, V)
|
| eq(0, 0) | ⇒ | true
|
| eq(0, s(W)) | ⇒ | false
|
| eq(s(P), 0) | ⇒ | false
|
| eq(s(X1), s(Y1)) | ⇒ | eq(X1, Y1)
|
| if(true, U1, V1) | ⇒ | U1
|
| if(false, W1, P1) | ⇒ | P1
|
| minsort(nil) | ⇒ | nil
|
| minsort(cons(X2, Y2)) | ⇒ | cons(min(X2, Y2), minsort(del(min(X2, Y2), cons(X2, Y2))))
|
| min(U2, nil) | ⇒ | U2
|
| min(V2, cons(W2, P2)) | ⇒ | if(le(V2, W2), min(V2, P2), min(W2, P2))
|
| del(X3, nil) | ⇒ | nil
|
| del(Y3, cons(U3, V3)) | ⇒ | if(eq(Y3, U3), V3, cons(U3, del(Y3, V3)))
|
| map(I3, nil) | ⇒ | nil
|
| map(J3, cons(X4, Y4)) | ⇒ | cons(J3 · X4, map(J3, Y4))
|
| filter(G4, nil) | ⇒ | nil
|
| filter(H4, cons(W4, P4)) | ⇒ | filter2(H4 · W4, H4, W4, P4)
|
| filter2(true, F5, Y5, U5) | ⇒ | cons(Y5, filter(F5, U5))
|
| filter2(false, H5, W5, P5) | ⇒ | filter(H5, P5)
|