| minus(0, X) | ⇒ | 0
|
| minus(s(Y), 0) | ⇒ | s(Y)
|
| minus(s(U), s(V)) | ⇒ | minus(U, V)
|
| le(0, W) | ⇒ | true
|
| le(s(P), 0) | ⇒ | false
|
| le(s(X1), s(Y1)) | ⇒ | le(X1, Y1)
|
| if(true, U1, V1) | ⇒ | U1
|
| if(false, W1, P1) | ⇒ | P1
|
| perfectp(0) | ⇒ | false
|
| perfectp(s(X2)) | ⇒ | f(X2, s(0), s(X2), s(X2))
|
| f(0, U2, 0, Y2) | ⇒ | true
|
| f(0, W2, s(P2), V2) | ⇒ | false
|
| f(s(Y3), 0, U3, X3) | ⇒ | f(Y3, X3, minus(U3, s(Y3)), X3)
|
| f(s(W3), s(P3), X4, V3) | ⇒ | if(le(W3, P3), f(s(W3), minus(P3, W3), X4, V3), f(W3, V3, X4, V3))
|
| map(Z4, nil) | ⇒ | nil
|
| map(G4, cons(V4, W4)) | ⇒ | cons(G4 · V4, map(G4, W4))
|
| filter(J4, nil) | ⇒ | nil
|
| filter(F5, cons(Y5, U5)) | ⇒ | filter2(F5 · Y5, F5, Y5, U5)
|
| filter2(true, H5, W5, P5) | ⇒ | cons(W5, filter(H5, P5))
|
| filter2(false, F6, Y6, U6) | ⇒ | filter(F6, U6)
|