Alphabet

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

Variables

X:b
Z:e → e
G:e → e
V:e
W:f
J:e → d
F1:e → d
Y1:e
U1:f
H1:e → d
W1:e
P1:f
F2:e → d
Y2:e
U2:f

Rules

f(s(X))f(g(X, X))
g(0, 1)s(0)
01
map(Z, nil)nil
map(G, cons(V, W))cons(G · V, map(G, W))
filter(J, nil)nil
filter(F1, cons(Y1, U1))filter2(F1 · Y1, F1, Y1, U1)
filter2(true, H1, W1, P1)cons(W1, filter(H1, P1))
filter2(false, F2, Y2, U2)filter(F2, U2)