* :: a → a → a
+ :: a → a → a
0 :: a
cons :: c → d → d
fact :: a → a
false :: b
filter :: (c → b) → d → d
filter2 :: b → (c → b) → c → d → d
map :: (c → c) → d → d
nil :: d
p :: a → a
s :: a → a
true :: b
p(s(X)) → X
fact(0) → s(0)
fact(s(Y)) → *(s(Y), fact(p(s(Y))))
*(0, U) → 0
*(s(V), W) → +(*(V, W), W)
+(P, 0) → P
+(X1, s(Y1)) → s(+(X1, Y1))
map(G1, nil) → nil
map(H1, cons(W1, P1)) → cons(H1(W1), map(H1, P1))
filter(F2, nil) → nil
filter(Z2, cons(U2, V2)) → filter2(Z2(U2), Z2, U2, V2)
filter2(true, I2, P2, X3) → cons(P2, filter(I2, X3))
filter2(false, Z3, U3, V3) → filter(Z3, V3)