Proof of a basic property of closure

Proof of a basic property of `closure`

This is the proof that took the longest time for OTTER to find, of all the proofs in the present document. It took over eight and a half hours of CPU time on a 100 MHz Pentium Linux box.

----> UNIT CONFLICT at 30923.91 sec ----> 19464 [binary,19463.1,23.1] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).

Length of proof is 13.  Level of proof is 8.

Proof



2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
12 [reference] x=x.
23 [reference] p2!=p1.
26 [reference] x y!=p1|isp1 x y =p1.
27 [reference] x y=p1|isp1 x y =p2.
64 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1.
68 [reference] subset x=p1|p1 x notsub(p1 x,p2 x) =p1.
69 [reference] subset x=p1|p2 x notsub(p1 x,p2 x) !=p1.
76 [reference] subset pair(xs,closure pair(xs,xf))=p1.
79 [reference] closure x y=p1|closure x y =p2.
82 [reference] closedunder pair(x2,p2 x1)=p2|subset pair(p1 x1,x2) =p2|subset pair(closure x1,x2) =p1.
83 [reference] xset x!=p1|x=x1|remove_singleton pair(xset,k(x1)) x =p1.
98 [reference] closedunder pair(remove_singleton pair(closure pair(xs,xf),k(x)),xf)=p1|xs x =p1|xf notclosed(remove_singleton pair(closure pair(xs,xf),k(x)),xf) =x.
99 [reference] subset pair(xs,remove_singleton pair(xs,k(x)))=p2|xs x !=p1.
100 [assumption to refute] badf x!=bad|$ans(x).
101 [assumption to refute] closure pair(bads,badf) bad!=p2.
102 [assumption to refute] bads bad!=p1.
106 [ur,101,79] closure pair(bads,badf) bad=p1.
117 [ur,102,98,100] closedunder pair(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)=p1|$ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).
131,130 [ur,102,27] isp1 bads bad=p2.
138 [ur,106,99] subset pair(closure pair(bads,badf),remove_singleton pair(closure pair(bads,badf),k(bad)))=p2.
167 [para_from,117.1.2,23.1.2,flip.1] closedunder pair(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)!=p2|$ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).
182 [para_into,138.1.1,82.3.1,demod,3,2,unit_del,23,167] subset pair(bads,remove_singleton pair(closure pair(bads,badf),k(bad)))=p2|$ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).
212 [para_into,182.1.1,69.1.1,demod,3,2,3,unit_del,23] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|remove_singleton pair(closure pair(bads,badf),k(bad)) notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) !=p1.
213 [para_into,182.1.1,68.1.1,demod,2,2,3,unit_del,23] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|bads notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) =p1.
242 [para_into,212.2.1,83.3.1,unit_del,12] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|closure pair(bads,badf) notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) !=p1|notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad)))=bad.
250 [ur,213,26] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|isp1 bads notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) =p1.
10198 [para_from,242.2.1,250.2.1.2,demod,131,unit_del,23] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|closure pair(bads,badf) notsub(bads,remove_singleton pair(closure pair(bads,badf),k(bad))) !=p1.
19461 [ur,10198,64,213] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|subset pair(bads,closure pair(bads,badf)) =p2.
19463 [para_into,19461.2.1,76.1.1,flip.2] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf))|p2=p1.
19464 [binary,19463.1,23.1] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).

up show outline