Alphabet

cons:[c × d] ⟶ d
f:[a × a] ⟶ a
false:b
filter:[c → b × d] ⟶ d
filter2:[b × c → b × c × d] ⟶ d
g:[a] ⟶ a
h:[a] ⟶ a
map:[c → c × d] ⟶ d
nil:d
true:b

Variables

X:a
Y:a
U:a
H:c → c
I:c → c
P:c
X1:d
Z1:c → b
G1:c → b
V1:c
W1:d
J1:c → b
X2:c
Y2:d
G2:c → b
V2:c
W2:d

Rules

g(h(g(X)))⇒g(X)
g(g(Y))⇒g(h(g(Y)))
h(h(U))⇒h(f(h(U), U))
map(H, nil)⇒nil
map(I, cons(P, X1))⇒cons(I · P, map(I, X1))
filter(Z1, nil)⇒nil
filter(G1, cons(V1, W1))⇒filter2(G1 · V1, G1, V1, W1)
filter2(true, J1, X2, Y2)⇒cons(X2, filter(J1, Y2))
filter2(false, G2, V2, W2)⇒filter(G2, W2)