Proof of push x y = p1 | push x y = p2

----> UNIT CONFLICT at   0.33 sec ----> 142 [binary,140.1,23.1] $F.

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

Proof

23 [reference] p2!=p1.
40 [reference] charq xf=p2|xf x =p1|xf x =p2.
85 [reference] charq (push x)=p1.
86 [assumption to refute] push bad1 bad2!=p1.
87 [assumption to refute] push bad1 bad2!=p2.
90 [hyper,86,40,unit_del,87] charq (push bad1)=p2.
140 [para_into,90.1.1,85.1.1,flip.1] p2=p1.
142 [binary,140.1,23.1] $F.

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