* :: a → a → a
+ :: a → a → a
- :: a → a → a
0 :: a
1 :: a
D :: a → a
cons :: c → d → d
constant :: a
false :: b
filter :: (c → b) → d → d
filter2 :: b → (c → b) → c → d → d
map :: (c → c) → d → d
nil :: d
t :: a
true :: b
D(t) → 1
D(constant) → 0
D(+(X, Y)) → +(D(X), D(Y))
D(*(U, V)) → +(*(V, D(U)), *(U, D(V)))
D(-(W, P)) → -(D(W), D(P))
map(F1, nil) → nil
map(Z1, cons(U1, V1)) → cons(Z1(U1), map(Z1, V1))
filter(I1, nil) → nil
filter(J1, cons(X2, Y2)) → filter2(J1(X2), J1, X2, Y2)
filter2(true, G2, V2, W2) → cons(V2, filter(G2, W2))
filter2(false, J2, X3, Y3) → filter(J2, Y3)