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
nil:d
quot:[a × 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

quot(0, s(X), s(Y))⇒0
quot(s(U), s(V), W)⇒quot(U, V, W)
quot(P, 0, s(X1))⇒s(quot(P, s(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)