Alphabet

!colon:[a × a] ⟶ a
C: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
true:b

Variables

X:a
Y:a
U:a
V:a
I:c → c
J:c → c
X1:c
Y1:d
G1:c → b
H1:c → b
W1:c
P1:d
F2:c → b
Y2:c
U2:d
H2:c → b
W2:c
P2:d

Rules

!colon(!colon(!colon(!colon(C, Y), U), V), X)⇒!colon(!colon(Y, V), !colon(!colon(!colon(Y, U), V), X))
map(I, nil)⇒nil
map(J, cons(X1, Y1))⇒cons(J · X1, map(J, Y1))
filter(G1, nil)⇒nil
filter(H1, cons(W1, P1))⇒filter2(H1 · W1, H1, W1, P1)
filter2(true, F2, Y2, U2)⇒cons(Y2, filter(F2, U2))
filter2(false, H2, W2, P2)⇒filter(H2, P2)