Proof of piecewise characterization of push, case 1

Proof of piecewise characterization of `push`, case 1

Note that one assumption to refute, closure pair(notp1 charq,setof) bad != p1 was placed in the usable list, while the other, push bad != bad was placed in the set of support. Notice also that this proof uses only the axioms of TRC, and clauses 21 and 51 in the proof, which are consequences of the axioms of TRC.

----> UNIT CONFLICT at   2.14 sec ----> 334 [binary,332.1,77.1] $F.

Length of proof is 3.  Level of proof is 3.

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).
5 [reference] pair(p1 x,p2 x)=x.
6 [reference] abst x y z=x k(z) (y z).
8 [reference] x=x.
9 [reference] k(x) y=x.
21 [reference] p1 x=p2 x |eq x =p2.
51 [reference] abst k(x) k(y)=k(x y).
75 [reference] push=abst (abst k(eq) pair(k(k(p1)),abst k(closure pair(notp1 charq,setof)))) pair(setof,pair(p1,p2)).
76 [assumption to refute] p.
77 [assumption to refute] closure pair(notp1 charq,setof) bad!=p1.
78 [assumption to refute] -p|push bad !=bad.
79 [ur,78,76,demod,75,6,6,1,4,1,51,4,4,5] eq pair(k(p1),k(closure pair(notp1 charq,setof) bad)) pair(setof bad,bad)!=bad.
271 [para_into,79.1.1.1,21.2.1,demod,3,2,3,unit_del,8,flip.1] k(closure pair(notp1 charq,setof) bad)=k(p1).
332 [para_from,271.1.1,9.1.1.1,demod,1,flip.1] closure pair(notp1 charq,setof) bad=p1.
334 [binary,332.1,77.1] $F.

up show outline