Alphabet

0:a
cons:[c × d] ⟶ d
double:[a] ⟶ a
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
plus:[a × a] ⟶ a
s:[a] ⟶ a
true:b

Variables

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

Rules

minus(X, 0)⇒X
minus(s(Y), s(U))⇒minus(Y, U)
double(0)⇒0
double(s(V))⇒s(s(double(V)))
plus(0, W)⇒W
plus(s(P), X1)⇒s(plus(P, X1))
plus(s(Y1), U1)⇒plus(Y1, s(U1))
plus(s(V1), W1)⇒s(plus(minus(V1, W1), double(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)