Alphabet

0:a
bits:[a] ⟶ a
cons:[c × d] ⟶ d
false:b
filter:[c → b × d] ⟶ d
filter2:[b × c → b × c × d] ⟶ d
half:[a] ⟶ a
map:[c → c × d] ⟶ d
nil:d
s:[a] ⟶ a
true:b

Variables

X:a
Y:a
G:c → c
H:c → c
W:c
P:d
F1:c → b
Z1:c → b
U1:c
V1:d
I1:c → b
P1:c
X2:d
Z2:c → b
U2:c
V2:d

Rules

half(0)⇒0
half(s(0))⇒0
half(s(s(X)))⇒s(half(X))
bits(0)⇒0
bits(s(Y))⇒s(bits(half(s(Y))))
map(G, nil)⇒nil
map(H, cons(W, P))⇒cons(H · W, map(H, P))
filter(F1, nil)⇒nil
filter(Z1, cons(U1, V1))⇒filter2(Z1 · U1, Z1, U1, V1)
filter2(true, I1, P1, X2)⇒cons(P1, filter(I1, X2))
filter2(false, Z2, U2, V2)⇒filter(Z2, V2)