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
plus:[a × a] ⟶ a
s:[a] ⟶ a
times:[a × a] ⟶ a
true:b

Variables

X:a
Y:a
U:a
V:a
W:a
P:a
X1:a
Y1:a
U1:a
H1:c → c
I1:c → c
P1:c
X2:d
Z2:c → b
G2:c → b
V2:c
W2:d
J2:c → b
X3:c
Y3:d
G3:c → b
V3:c
W3:d

Rules

times(X, 0)⇒0
times(Y, s(U))⇒plus(times(Y, U), Y)
plus(V, 0)⇒V
plus(0, W)⇒W
plus(P, s(X1))⇒s(plus(P, X1))
plus(s(Y1), U1)⇒s(plus(Y1, U1))
map(H1, nil)⇒nil
map(I1, cons(P1, X2))⇒cons(I1 · P1, map(I1, X2))
filter(Z2, nil)⇒nil
filter(G2, cons(V2, W2))⇒filter2(G2 · V2, G2, V2, W2)
filter2(true, J2, X3, Y3)⇒cons(X3, filter(J2, Y3))
filter2(false, G3, V3, W3)⇒filter(G3, W3)