Alphabet

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

Variables

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

Rules

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