Proof that push is one-to-one

Proof that `push` is one-to-one

This proof is interesting for several reasons. First, it the longest proof in this document (length 35) and took a relatively long time to find (one CPU-hour on a 100-MHz Pentium Linux box). Second, it is one of the major final goals that all the other proofs have been leading to. Third, it is the only proof in this document that used a demodulator to demodulate an equality into another equality. Note however that this use of demodulation does not seem to be very crucial, being used only for the trivial rewrite of push bad1 = push bad2 as push bad2 = push bad1.

----> UNIT CONFLICT at 3684.42 sec ----> 12111 [binary,12109.1,130.1] $F.

Length of proof is 35.  Level of proof is 12.

Proof



2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
11 [reference] (eq pair(x,y) =p1)= (x=y).
12 [reference] x=x.
19 [reference] x!=y|eq pair(x,y) =p1.
20 [reference] x=y|eq pair(x,y) =p2.
23 [reference] p2!=p1.
24 [reference] p1 x!=p2 x |eq x =p1.
48 [reference] setof x!=setof y |x=y.
83 [reference] closure pair(notp1 charq,setof) x=p1|push x =x.
84 [reference] closure pair(notp1 charq,setof) x=p2|push x =setof x.
87 [reference] push x=x|push x =setof x.
90 [reference] closure pair(notp1 charq,setof) x=closure pair(notp1 charq,setof) (push x).
91 [reference] closure pair(notp1 charq,setof) (push x)=closure pair(notp1 charq,setof) x.
92 [assumption to refute] push bad1=push bad2.
93 [assumption to refute] bad1!=bad2.
94 [hyper,92,19,demod,11,flip.1] push bad2=push bad1.
95 [para_into,92.1.1,87.2.1] setof bad1=push bad2 |push bad1 =bad1.
96 [para_into,92.1.1,87.1.1,flip.1,flip.2] push bad2=bad1|setof bad1 =push bad1.
97 [para_into,92.1.1,84.2.1] setof bad1=push bad2 |closure pair(notp1 charq,setof) bad1 =p2.
98 [para_into,92.1.1,83.2.1,flip.1] push bad2=bad1|closure pair(notp1 charq,setof) bad1 =p1.
104 [para_into,92.1.2,87.2.1,flip.1] setof bad2=push bad1 |push bad2 =bad2.
106 [para_into,92.1.2,84.2.1,flip.1] setof bad2=push bad1 |closure pair(notp1 charq,setof) bad2 =p2.
107 [para_into,92.1.2,83.2.1] push bad1=bad2|closure pair(notp1 charq,setof) bad2 =p1.
111 [para_from,92.1.1,90.1.2.2,demod,91,flip.1] closure pair(notp1 charq,setof) bad2=closure pair(notp1 charq,setof) bad1.
124 [hyper,93,20] eq pair(bad1,bad2)=p2.
130 [para_into,124.1.1,24.2.1,demod,2,3,unit_del,23,flip.1] bad2!=bad1.
139 [para_into,95.1.2,87.2.1,flip.1] setof bad2=setof bad1 |push bad1 =bad1|push bad2 =bad2.
148 [para_into,95.2.1.2,95.2.2] setof bad1=push bad2 |push (push bad1) =bad1.
271 [para_from,97.2.2,23.1.1] closure pair(notp1 charq,setof) bad1!=p1|setof bad1 =push bad2.
290 [para_into,104.2.1,96.1.1,unit_del,130] setof bad2=push bad1 |setof bad1 =push bad1.
292 [para_into,104.2.1,94.1.1] setof bad2=push bad1 |push bad1 =bad2.
446 [para_from,98.2.2,23.1.2,flip.1] closure pair(notp1 charq,setof) bad1!=p2|push bad2 =bad1.
5644 [para_into,290.2.2,292.2.1] setof bad2=push bad1 |setof bad1 =bad2.
7907 [hyper,139,48,unit_del,130] push bad1=bad1|push bad2 =bad2.
7984 [para_into,7907.2.1,94.1.1] push bad1=bad1|push bad1 =bad2.
8066 [para_from,7907.1.2,130.1.2,flip.1] push bad1!=bad2|push bad2 =bad2.
8197 [para_from,7907.2.2,130.1.1] push bad2!=bad1|push bad1 =bad1.
8879 [para_from,8066.2.2,130.1.1] push bad2!=bad1|push bad1 !=bad2.
8934 [para_into,8197.1.1.2,7984.2.2] push (push bad1)!=bad1|push bad1 =bad1.
9575 [para_into,8879.1.1,94.1.1] push bad1!=bad1|push bad1 !=bad2.
9592 [para_into,8879.2.1,94.1.2] push bad2!=bad1|push bad2 !=bad2.
10074 [para_from,8934.2.1,9575.1.1,unit_del,12] push bad1!=bad2|push (push bad1) !=bad1.
10818 [para_into,271.1.2,107.2.2,unit_del,111] setof bad1=push bad2 |push bad1 =bad2.
10820 [hyper,10818,10074,148] setof bad1=push bad2.
10894 [para_into,10820.1.2,94.1.1] setof bad1=push bad1.
10928 [para_from,10820.1.2,9592.2.1] push bad2!=bad1|setof bad1 !=bad2.
11552 [para_into,446.1.2,106.2.2,unit_del,111] push bad2=bad1|setof bad2 =push bad1.
11564 [hyper,11552,10928,5644] setof bad2=push bad1.
11598 [para_into,11564.1.2,10894.1.2] setof bad2=setof bad1.
12109 [hyper,11598,48] bad2=bad1.
12111 [binary,12109.1,130.1] $F.