Alphabet

0:c
cons:[c × d] ⟶ d
false:b
filter:[c → b × d] ⟶ d
filter2:[b × c → b × c × d] ⟶ d
map:[c → c × d] ⟶ d
nil:d
rev:[d] ⟶ d
rev1:[c × d] ⟶ c
rev2:[c × d] ⟶ d
s:[a] ⟶ c
true:b

Variables

X:d
Y:c
U:a
V:d
W:c
P:c
X1:c
Y1:d
U1:c
V1:c
I1:c → c
J1:c → c
X2:c
Y2:d
G2:c → b
H2:c → b
W2:c
P2:d
F3:c → b
Y3:c
U3:d
H3:c → b
W3:c
P3:d

Rules

rev(nil)⇒nil
rev(cons(Y, X))⇒cons(rev1(Y, X), rev2(Y, X))
rev1(0, nil)⇒0
rev1(s(U), nil)⇒s(U)
rev1(W, cons(P, V))⇒rev1(P, V)
rev2(X1, nil)⇒nil
rev2(U1, cons(V1, Y1))⇒rev(cons(U1, rev2(V1, Y1)))
map(I1, nil)⇒nil
map(J1, cons(X2, Y2))⇒cons(J1 · X2, map(J1, Y2))
filter(G2, nil)⇒nil
filter(H2, cons(W2, P2))⇒filter2(H2 · W2, H2, W2, P2)
filter2(true, F3, Y3, U3)⇒cons(Y3, filter(F3, U3))
filter2(false, H3, W3, P3)⇒filter(H3, P3)