Proof of pair(x1,y1) != pair(x2,y2) | y1 = y2.

----> UNIT CONFLICT at   0.94 sec ----> 63 [binary,62.1,8.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof

3 [reference] p2 pair(x,y)=y.
8 [reference] x=x.
11 [reference] p2 pair(x,y)=y.
52 [assumption to refute] pair(bad1,bad2)=pair(bad3,bad4).
53 [assumption to refute] bad2!=bad4.
59,58 [para_from,52.1.1,11.1.1.2,demod,3] bad4=bad2.
62 [back_demod,53,demod,59] bad2!=bad2.
63 [binary,62.1,8.1] $F.

up | previous | next | detailed contents | brief contents | OTTER output file