Alphabet

0:a
cons:[c × c] ⟶ c
copy:[a × c × c] ⟶ c
f:[c] ⟶ c
false:b
filter:[c → b × c] ⟶ c
filter2:[b × c → b × c × c] ⟶ c
map:[c → c × c] ⟶ c
n:a
nil:c
s:[a] ⟶ a
true:b

Variables

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

Rules

f(cons(nil, X))⇒X
f(cons(f(cons(nil, Y)), U))⇒copy(n, Y, U)
copy(0, V, W)⇒f(W)
copy(s(P), X1, Y1)⇒copy(P, X1, cons(f(X1), 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)