Proof of converse defining property for subset

Proof of converse defining property for `subset`

To obtain this proof I used OTTER's para_into_units_only and para_from_units_only options.

----> UNIT CONFLICT at   4.36 sec ----> 356 [binary,355.1,19.1] $ans(noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))).

Length of proof is 8.  Level of proof is 7.

Proof



1 [reference] k(x) y=x.
2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
4 [reference] pair(x,y) z=pair(x z,y z).
6 [reference] abst x y z=x k(z) (y z).
17 [reference] x=y|x noteq(x,y) !=y noteq(x,y).
19 [reference] p2!=p1.
20 [reference] p1 x!=p2 x |eq x =p1.
21 [reference] p1 x=p2 x |eq x =p2.
22 [reference] x y!=p1|isp1 x y =p1.
52 [reference] pair(x1,y1)!=pair(x2,y2)|x1=x2.
53 [reference] pair(x1,y1)!=pair(x2,y2)|y1=y2.
57 [reference] subset=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(k(k(pair(p1,p2))),pair(p1,abst k(isp1) p2))).
59 [assumption to refute] -p|subset pair(bad1,bad2) !=p1.
60 [assumption to refute] bad1 x!=p1|bad2 x =p1|$ans(x).
61 [assumption to refute] p.
62 [ur,59,61,demod,57,6,1,4,1,6,1,4,1,4,2,6,1,3] eq pair(k(p2),abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)))!=p1.
72 [ur,62,20,demod,2,3,flip.1] abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2))!=k(p2).
87 [ur,72,17,demod,6,1,4,1,4,1] eq pair(pair(p1,p2),pair(bad1 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)),
isp1 bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))))!=p2.
199 [ur,87,21,demod,2,3,flip.1] pair(bad1 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)),isp1 bad2 noteq(abst
 k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)))=pair(p1,p2).
295,294 [ur,199,53] isp1 bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))=p2.
296 [ur,199,52] bad1 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))=p1.
344 [ur,296,60] bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))=p1|$ans(noteq(abst k(eq) pair(k(pair(p1,p
2)),pair(bad1,isp1 bad2)),k(p2))).
355 [ur,344,22,demod,295] $ans(noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)))|p2=p1.
356 [binary,355.1,19.1] $ans(noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))).

up show outline