Alphabet

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

Variables

X:c
Y:b
U:b
V:c
W:c
P:b
X1:c
Y1:c
U1:b
V1:c
W1:c
J1:e → e
F2:e → e
Y2:e
U2:f
H2:e → d
I2:e → d
P2:e
X3:f
Z3:e → d
U3:e
V3:f
I3:e → d
P3:e
X4:f

Rules

h(Y, e(X))⇒h(c(Y), d(Y, X))
d(U, g(0, 0))⇒e(0)
d(P, g(V, W))⇒g(e(V), d(P, W))
d(c(U1), g(g(X1, Y1), 0))⇒g(d(c(U1), g(X1, Y1)), d(U1, g(X1, Y1)))
g(e(V1), e(W1))⇒e(g(V1, W1))
map(J1, nil)⇒nil
map(F2, cons(Y2, U2))⇒cons(F2 · Y2, map(F2, U2))
filter(H2, nil)⇒nil
filter(I2, cons(P2, X3))⇒filter2(I2 · P2, I2, P2, X3)
filter2(true, Z3, U3, V3)⇒cons(U3, filter(Z3, V3))
filter2(false, I3, P3, X4)⇒filter(I3, X4)