| eq(0, 0) | ⇒ | true
|
| eq(0, s(X)) | ⇒ | false
|
| eq(s(Y), 0) | ⇒ | false
|
| eq(s(U), s(V)) | ⇒ | eq(U, V)
|
| or(true, W) | ⇒ | true
|
| or(false, P) | ⇒ | P
|
| union(empty, X1) | ⇒ | X1
|
| union(edge(V1, W1, U1), Y1) | ⇒ | edge(V1, W1, union(U1, Y1))
|
| reach(X2, Y2, empty, P1) | ⇒ | false
|
| reach(X3, Y3, edge(W2, P2, V2), U2) | ⇒ | if!6220reach!62201(eq(X3, W2), X3, Y3, edge(W2, P2, V2), U2)
|
| if!6220reach!62201(true, X4, Y4, edge(W3, P3, V3), U3) | ⇒ | if!6220reach!62202(eq(Y4, P3), X4, Y4, edge(W3, P3, V3), U3)
|
| if!6220reach!62201(false, X5, Y5, edge(W4, P4, V4), U4) | ⇒ | reach(X5, Y5, V4, edge(W4, P4, U4))
|
| if!6220reach!62202(true, X6, Y6, edge(W5, P5, V5), U5) | ⇒ | true
|
| if!6220reach!62202(false, X7, Y7, edge(W6, P6, V6), U6) | ⇒ | or(reach(X7, Y7, V6, U6), reach(P6, Y7, union(V6, U6), empty))
|
| map(G7, nil) | ⇒ | nil
|
| map(H7, cons(W7, P7)) | ⇒ | cons(H7 · W7, map(H7, P7))
|
| filter(F8, nil) | ⇒ | nil
|
| filter(Z8, cons(U8, V8)) | ⇒ | filter2(Z8 · U8, Z8, U8, V8)
|
| filter2(true, I8, P8, X9) | ⇒ | cons(P8, filter(I8, X9))
|
| filter2(false, Z9, U9, V9) | ⇒ | filter(Z9, V9)
|