Alphabet

0:a
cons:[c × d] ⟶ d
false:b
filter:[c → b × d] ⟶ d
filter2:[b × c → b × c × d] ⟶ d
map:[c → c × d] ⟶ d
minus:[a × a] ⟶ a
nil:d
pred:[a] ⟶ a
quot:[a × a] ⟶ a
s:[a] ⟶ a
true:b

Variables

X:a
Y:a
U:a
V:a
W:a
P:a
X1:a
Z1:c → c
G1:c → c
V1:c
W1:d
J1:c → b
F2:c → b
Y2:c
U2:d
H2:c → b
W2:c
P2:d
F3:c → b
Y3:c
U3:d

Rules

pred(s(X))⇒X
minus(Y, 0)⇒Y
minus(U, s(V))⇒pred(minus(U, V))
quot(0, s(W))⇒0
quot(s(P), s(X1))⇒s(quot(minus(P, X1), s(X1)))
map(Z1, nil)⇒nil
map(G1, cons(V1, W1))⇒cons(G1 · V1, map(G1, W1))
filter(J1, nil)⇒nil
filter(F2, cons(Y2, U2))⇒filter2(F2 · Y2, F2, Y2, U2)
filter2(true, H2, W2, P2)⇒cons(W2, filter(H2, P2))
filter2(false, F3, Y3, U3)⇒filter(F3, U3)