remove_singleton removes one element from a set.remove_singleton is the only term introduced in this document that is not used, directly or indirectly, in building up the the definition of the term push. Instead, it will be used later to concisely state a key technical lemma used to help prove that push is onto the characteristic functions.Definition of remove_singleton
Basic defining properties of remove_singleton
If s is closed under f, but s - {x} is not closed under f, then f c = x where c witnesses the fact that s - {x} is not closed under f.
list(usable).
a(closedunder,pair(xs,xf)) = p2 | a(closedunder,pair(a(remove_singleton,pair(xs,k(x))),xf)) = p1 | a(xf,notclosed(a(remove_singleton,pair(xs,k(x))),xf)) = x.
end_of_list.
Proof of important lemma on closedunder and remove_singleton | OTTER output file