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