$ :: a → a → a
* :: a → a → a
/ :: a → a → a
cons :: c → d → d
e :: a
false :: b
filter :: (c → b) → d → d
filter2 :: b → (c → b) → c → d → d
map :: (c → c) → d → d
nil :: d
true :: b
$(X, X) → e
$(e, Y) → Y
$(U, *(U, V)) → V
$(/(W, P), W) → P
/(X1, X1) → e
/(Y1, e) → Y1
/(*(V1, U1), U1) → V1
/(W1, $(P1, W1)) → P1
*(e, X2) → X2
*(Y2, e) → Y2
*(U2, $(U2, V2)) → V2
*(/(P2, W2), W2) → P2
map(F3, nil) → nil
map(Z3, cons(U3, V3)) → cons(Z3(U3), map(Z3, V3))
filter(I3, nil) → nil
filter(J3, cons(X4, Y4)) → filter2(J3(X4), J3, X4, Y4)
filter2(true, G4, V4, W4) → cons(V4, filter(G4, W4))
filter2(false, J4, X5, Y5) → filter(J4, Y5)