| le(0, X) | ⇒ | true
|
| le(s(Y), 0) | ⇒ | false
|
| le(s(U), s(V)) | ⇒ | le(U, V)
|
| pred(s(W)) | ⇒ | W
|
| minus(P, 0) | ⇒ | P
|
| minus(X1, s(Y1)) | ⇒ | pred(minus(X1, Y1))
|
| gcd(0, U1) | ⇒ | U1
|
| gcd(s(V1), 0) | ⇒ | s(V1)
|
| gcd(s(W1), s(P1)) | ⇒ | if!6220gcd(le(P1, W1), s(W1), s(P1))
|
| if!6220gcd(true, s(X2), s(Y2)) | ⇒ | gcd(minus(X2, Y2), s(Y2))
|
| if!6220gcd(false, s(U2), s(V2)) | ⇒ | gcd(minus(V2, U2), s(U2))
|
| map(I2, nil) | ⇒ | nil
|
| map(J2, cons(X3, Y3)) | ⇒ | cons(J2 · X3, map(J2, Y3))
|
| filter(G3, nil) | ⇒ | nil
|
| filter(H3, cons(W3, P3)) | ⇒ | filter2(H3 · W3, H3, W3, P3)
|
| filter2(true, F4, Y4, U4) | ⇒ | cons(Y4, filter(F4, U4))
|
| filter2(false, H4, W4, P4) | ⇒ | filter(H4, P4)
|