Alphabet

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

Variables

X:d
Y:d
U:d
V:d
W:d
P:d
F1:d → d
Z1:d → d
U1:d
V1:d
I1:d → c
J1:d → c
X2:d
Y2:d
G2:d → c
V2:d
W2:d
J2:d → c
X3:d
Y3:d

Rules

f(s(X))⇒f(X)
g(cons(0, Y))⇒g(Y)
g(cons(s(U), V))⇒s(U)
h(cons(W, P))⇒h(g(cons(W, P)))
map(F1, nil)⇒nil
map(Z1, cons(U1, V1))⇒cons(Z1 · U1, map(Z1, V1))
filter(I1, nil)⇒nil
filter(J1, cons(X2, Y2))⇒filter2(J1 · X2, J1, X2, Y2)
filter2(true, G2, V2, W2)⇒cons(V2, filter(G2, W2))
filter2(false, J2, X3, Y3)⇒filter(J2, Y3)