push respects the partition of the universe by pushset, that is, pushset x = pushset (push x)

list(usable).
a(a(closure,pair(a(notp1,charq),setof)),x) = p2 | a(a(closure,pair(a(notp1,charq),setof)),a(push,x)) = p1.
end_of_list.

Proof that if x is in pushset then push x is in pushset. | OTTER output file

If push x is in pushset then x is in pushset.

list(usable).
a(a(closure,pair(a(notp1,charq),setof)),x) = p1 | a(a(closure,pair(a(notp1,charq),setof)),a(push,x)) = p2.     %    (not used in later proofs)
end_of_list.

Proof that if push x is in pushset then x is in pushset. | OTTER output file

For every x, pushset (push x) = pushset x.

list(usable).
a(a(closure,pair(a(notp1,charq),setof)),x) = a(a(closure,pair(a(notp1,charq),setof)),a(push,x)).
end_of_list.

list(demodulators).
a(a(closure,pair(a(notp1,charq),setof)),a(push,x)) = a(a(closure,pair(a(notp1,charq),setof)),x).
end_of_list.

Proof that pushset (push x) = pushset x | OTTER output file

up show outline