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

Proof of a(charq,eq) = p1. 

----> UNIT CONFLICT at   0.16 sec ----> 99 [binary,98.1,85.1] $F.

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

Proof


19 [reference] p1 x!=p2 x |eq x =p1.
20 [reference] p1 x=p2 x |eq x =p2.
33 [reference] charq xf=p1|xf noteq(isp1 xf,xf) !=p1.
34 [reference] charq xf=p1|xf noteq(isp1 xf,xf) !=p2.
44 [assumption to refute] charq eq!=p1.
48 [ur,44,34] eq noteq(isp1 eq,eq)!=p2.
49 [ur,44,33] eq noteq(isp1 eq,eq)!=p1.
85 [ur,48,20,flip.1] p2 noteq(isp1 eq,eq)=p1 noteq(isp1 eq,eq).
98 [ur,49,19,flip.1] p2 noteq(isp1 eq,eq)!=p1 noteq(isp1 eq,eq).
99 [binary,98.1,85.1] $F.

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