closure and remove_singletonT is the closure of S under f and T - {x} is not closed under f and x is not a member of Sc such that c is a member of Tf c = x.c = notclosed(remove_singleton pair(closure pair(S,f), k(x)), f), as shown by the answer literal in the proof.list(usable). a(closedunder,pair(a(remove_singleton,pair(a(closure,pair(xs,xf)),k(x))),xf)) = p1 | a(xs,x) = p1 | a(a(closure,pair(xs,xf)),notclosed(a(remove_singleton,pair(a(closure,pair(xs,xf)),k(x))),xf)) = p1. % (not used in later proofs) a(closedunder,pair(a(remove_singleton,pair(a(closure,pair(xs,xf)),k(x))),xf)) = p1 | a(xs,x) = p1 | a(xf,notclosed(a(remove_singleton,pair(a(closure,pair(xs,xf)),k(x))),xf)) = x. end_of_list.
Proof of key lemma on closure and remove_singleton | OTTER output file
If x is a member of S then S is not a subset of S - {x}.
list(usable). a(subset,pair(xs,a(remove_singleton,pair(xs,k(x))))) = p2 | a(xs,x) != p1. end_of_list.
Proof that if x is a member of S then S is not a subset of S - {x}. | OTTER output file
If x is in the closure of S under f, then either x is in the range of f or x is a member of S.
list(usable). a(xf,notclosed(a(remove_singleton,pair(a(closure,pair(xs,xf)),k(x))),xf)) = x | a(a(closure,pair(xs,xf)),x) = p2 | a(xs,x) = p1. end_of_list.
Proof of a basic property of closure | OTTER output file