The function push is onto the characteristic functions

The function `push` is onto the characteristic functions

This is the grand finale: The following clause says that if x is a characteristic function then push c = x where c = x or c = notclosed(remove_singleton pair(closure pair(notp1 charq, push), k(x)), push).

list(usable).
a(charq,x) != p1 | a(push,x) = x | a(push,notclosed(a(remove_singleton,pair(a(closure,pair(a(notp1,charq),push)),k(x))),push)) = x.     %    (not used in later proofs)
end_of_list.

Proof that push is onto the characteristic functions | OTTER output file

up show outline