Alphabet

0:b
1:b
c:[b] ⟶ b
cons:[c × d] ⟶ d
f:[b] ⟶ a
false:a
filter:[c → a × d] ⟶ d
filter2:[a × c → a × c × d] ⟶ d
g:[b × b] ⟶ b
if:[a × b × b] ⟶ b
map:[c → c × d] ⟶ d
nil:d
s:[b] ⟶ b
true:a

Variables

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

Rules

f(0)⇒true
f(1)⇒false
f(s(X))⇒f(X)
if(true, s(Y), s(U))⇒s(Y)
if(false, s(V), s(W))⇒s(W)
g(P, c(X1))⇒c(g(P, X1))
g(Y1, c(U1))⇒g(Y1, if(f(Y1), c(g(s(Y1), U1)), c(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)