Alphabet

0:a
1:a
2: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] ⟶ b
map:[d → d × e] ⟶ e
nil:e
true:c

Variables

X:a
Y:a
U:a
V:a
W:b
P:b
X1:b
Y1:b
G1:d → d
H1:d → d
W1:d
P1:e
F2:d → c
Z2:d → c
U2:d
V2:e
I2:d → c
P2:d
X3:e
Z3:d → c
U3:d
V3:e

Rules

f(0, 1, X)⇒f(X, X, X)
f(Y, U, V)⇒2
0⇒2
1⇒2
g(W, W, P)⇒P
g(X1, Y1, Y1)⇒X1
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)