Alphabet

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

Variables

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

Rules

f(X, c(X), c(Y))⇒f(Y, Y, f(Y, X, Y))
f(s(U), V, W)⇒f(U, s(c(V)), c(W))
f(c(P), P, X1)⇒c(X1)
g(Y1, U1)⇒Y1
g(V1, W1)⇒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)