Proof of a(x,y) != p1 | a(a(notp1,x),y) = p2.

Proof of `a(x,y) != p1 | a(a(notp1,x),y) = p2.`

----> UNIT CONFLICT at   0.10 sec ----> 67 [binary,66.1,8.1] $F.

Length of proof is 5.  Level of proof is 4.

Proof



1 [reference] k(x) y=x.
4 [reference] pair(x,y) z=pair(x z,y z).
6 [reference] abst x y z=x k(z) (y z).
8 [reference] x=x.
16 [reference] x=y|eq pair(x,y) =p2.
18 [reference] p1!=p2.
19 [reference] x y!=p1|isp1 x y =p1.
23 [reference] notp1=abst k(abst k(eq)) pair(k(k(p2)),isp1).
25 [assumption to refute] bad1 bad2=p1.
26 [assumption to refute] notp1 bad1 bad2!=p2.
28,27 [ur,25,19] isp1 bad1 bad2=p1.
42 [para_from,25.1.2,18.1.1] bad1 bad2!=p2.
50 [para_into,42.1.1,25.1.1,flip.1] p2!=p1.
55,54 [ur,50,16] eq pair(p2,p1)=p2.
66 [para_into,26.1.1.1.1,23.1.1,demod,6,1,4,1,6,1,4,1,28,55] p2!=p2.
67 [binary,66.1,8.1] $F.