up | previous | next | detailed contents | brief contents

Lemmas on closure and remove_singleton

If T is the closure of S under f and
then there is some c such that
In fact, 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


up | previous | next | detailed contents | brief contents