Alphabet

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

Variables

X:b
Y:b
U:b
V:b
W:b
P:b
X1:b
Y1:b
U1:b
V1:b
W1:b
P1:b
X2:c
Y2:c
U2:c
V2:c
W2:b
P2:b
X3:c
Y3:b
U3:b
V3:c
W3:c
P3:b
X4:b
Z4:b → b
G4:b → b
V4:b
W4:c
J4:b → a
F5:b → a
Y5:b
U5:c
H5:b → a
W5:b
P5:c
F6:b → a
Y6:b
U6:c

Rules

minus(X, 0)⇒X
minus(s(Y), s(U))⇒minus(Y, U)
minus(minus(V, W), P)⇒minus(V, plus(W, P))
quot(0, s(X1))⇒0
quot(s(Y1), s(U1))⇒s(quot(minus(Y1, U1), s(U1)))
plus(0, V1)⇒V1
plus(s(W1), P1)⇒s(plus(W1, P1))
app(nil, X2)⇒X2
app(Y2, nil)⇒Y2
app(cons(W2, V2), U2)⇒cons(W2, app(V2, U2))
sum(cons(P2, nil))⇒cons(P2, nil)
sum(cons(Y3, cons(U3, X3)))⇒sum(cons(plus(Y3, U3), X3))
sum(app(W3, cons(P3, cons(X4, V3))))⇒sum(app(W3, sum(cons(P3, cons(X4, V3)))))
map(Z4, nil)⇒nil
map(G4, cons(V4, W4))⇒cons(G4 · V4, map(G4, W4))
filter(J4, nil)⇒nil
filter(F5, cons(Y5, U5))⇒filter2(F5 · Y5, F5, Y5, U5)
filter2(true, H5, W5, P5)⇒cons(W5, filter(H5, P5))
filter2(false, F6, Y6, U6)⇒filter(F6, U6)