Alphabet

cons:[b × c] ⟶ c
false:a
filter:[b → a × c] ⟶ c
filtersub:[a × b → a × c] ⟶ c
nil:c
true:a

Variables

F:b → a
Z:b → a
U:b
V:c
I:b → a
P:b
X1:c
Z1:b → a
U1:b
V1:c

Rules

filter(F, nil)⇒nil
filter(Z, cons(U, V))⇒filtersub(Z · U, Z, cons(U, V))
filtersub(true, I, cons(P, X1))⇒cons(P, filter(I, X1))
filtersub(false, Z1, cons(U1, V1))⇒filter(Z1, V1)