Proof of a(p1,x) = a(p2,x) | a(eq,x) = p2.

----> UNIT CONFLICT at   0.12 sec ----> 51 [binary,49.1,21.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof



5 [reference] pair(p1 x,p2 x)=x.
16 [reference] x=y|eq pair(x,y) =p2.
20 [assumption to refute] p1 bad!=p2 bad.
21 [assumption to refute] eq bad!=p2.
49 [ur,20,16,demod,5] eq bad=p2.
51 [binary,49.1,21.1] $F.

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