| minus(X, 0) | ⇒ | X
|
| minus(s(Y), s(U)) | ⇒ | minus(Y, U)
|
| quot(0, s(V)) | ⇒ | 0
|
| quot(s(W), s(P)) | ⇒ | s(quot(minus(W, P), s(P)))
|
| plus(0, X1) | ⇒ | X1
|
| plus(s(Y1), U1) | ⇒ | s(plus(Y1, U1))
|
| plus(minus(V1, s(0)), minus(W1, s(s(P1)))) | ⇒ | plus(minus(W1, s(s(P1))), minus(V1, s(0)))
|
| plus(plus(X2, s(0)), plus(Y2, s(s(U2)))) | ⇒ | plus(plus(Y2, s(s(U2))), plus(X2, s(0)))
|
| map(H2, nil) | ⇒ | nil
|
| map(I2, cons(P2, X3)) | ⇒ | cons(I2 · P2, map(I2, X3))
|
| filter(Z3, nil) | ⇒ | nil
|
| filter(G3, cons(V3, W3)) | ⇒ | filter2(G3 · V3, G3, V3, W3)
|
| filter2(true, J3, X4, Y4) | ⇒ | cons(X4, filter(J3, Y4))
|
| filter2(false, G4, V4, W4) | ⇒ | filter(G4, W4)
|