Alphabet

and:[a × a] ⟶ a
cons:[c × d] ⟶ d
false:b
filter:[c → b × d] ⟶ d
filter2:[b × c → b × c × d] ⟶ d
map:[c → c × d] ⟶ d
nil:d
not:[a] ⟶ a
or:[a × a] ⟶ a
true:b

Variables

X:a
Y:a
U:a
V:a
W:a
P:a
X1:a
Y1:a
U1:a
V1:a
W1:a
J1:c → c
F2:c → c
Y2:c
U2:d
H2:c → b
I2:c → b
P2:c
X3:d
Z3:c → b
U3:c
V3:d
I3:c → b
P3:c
X4:d

Rules

not(not(X))⇒X
not(or(Y, U))⇒and(not(Y), not(U))
not(and(V, W))⇒or(not(V), not(W))
and(P, or(X1, Y1))⇒or(and(P, X1), and(P, Y1))
and(or(V1, W1), U1)⇒or(and(U1, V1), and(U1, W1))
map(J1, nil)⇒nil
map(F2, cons(Y2, U2))⇒cons(F2 · Y2, map(F2, U2))
filter(H2, nil)⇒nil
filter(I2, cons(P2, X3))⇒filter2(I2 · P2, I2, P2, X3)
filter2(true, Z3, U3, V3)⇒cons(U3, filter(Z3, V3))
filter2(false, I3, P3, X4)⇒filter(I3, X4)