a(x,y) != p1 | a(a(isp1,x),y) = p1. p in lines 13 and 15 of the proof below. This is a trick (or "kludge") due to Hart and Kunen [8]. Since p occurs only in these two lines, the two lines are for the purposes of this proof equivalent to the equation isp1 bad1 bad2 != p1. The purpose of this trick is to force immediate demodulation of this equation without forcing demodulation of the other input clauses. Thus isp1 will immediately be replaced with its definition, and isp1 bad1 bad2 will be reduced as much as possible.
Also, a program was used to generate weights, giving every subterm of isp1 a weight of 1. This and related automatically generated weights are used throughout the development. The related weighting methods, not used for isp1, are to apply a lambda-term to a variable x, reduce it, and weight all subterms with weight 1. If a lambda term has the form (lambda (x y) ...) then it is additionally applied to pair(x,x). This process is carried out for all subterms of the original definition of the form (lambda ...). The resulting weights are duplicated with x replaced by the template $(1) which matches any term substituted for x.
----> UNIT CONFLICT at 1.39 sec ----> 299 [binary,298.1,14.1] $F. Length of proof is 12. Level of proof is 12.
2 [reference] k(x) y=x. 5 [reference] pair(x,y) z=pair(x z,y z). 6 [reference] pair(p1 x,p2 x)=x. 7 [reference] abst x y z=x k(z) (y z). 8 [reference] x!=y|eq pair(x,y) =p1. 12 [reference] isp1=abst k(abst k(eq)) pair(k(k(p1)),pair(p1,p2)). 13 [assumption to refute] p. 14 [assumption to refute] bad1 bad2=p1. 15 [assumption to refute] -p|isp1 bad1 bad2 !=p1. 26 [ur,15,13,demod,12] abst k(abst k(eq)) pair(k(k(p1)),pair(p1,p2)) bad1 bad2!=p1. 37 [para_into,26.1.1.1,7.1.1] k(abst k(eq)) k(bad1) (pair(k(k(p1)),pair(p1,p2)) bad1) bad2!=p1. 88 [para_into,37.1.1.1.1,2.1.1] abst k(eq) (pair(k(k(p1)),pair(p1,p2)) bad1) bad2!=p1. 98 [para_into,88.1.1,7.1.1] k(eq) k(bad2) (pair(k(k(p1)),pair(p1,p2)) bad1 bad2)!=p1. 112 [para_into,98.1.1.1,2.1.1] eq (pair(k(k(p1)),pair(p1,p2)) bad1 bad2)!=p1. 121 [para_into,112.1.1.2.1,5.1.1] eq (pair(k(k(p1)) bad1,pair(p1,p2) bad1) bad2)!=p1. 207 [para_into,121.1.1.2.1.1,2.1.1] eq (pair(k(p1),pair(p1,p2) bad1) bad2)!=p1. 217 [para_into,207.1.1.2,5.1.1] eq pair(k(p1) bad2,pair(p1,p2) bad1 bad2)!=p1. 242 [ur,217,8,flip.1] pair(p1,p2) bad1 bad2!=k(p1) bad2. 254 [para_into,242.1.2,2.1.1] pair(p1,p2) bad1 bad2!=p1. 259 [para_into,254.1.1.1,5.1.1] pair(p1 bad1,p2 bad1) bad2!=p1. 298 [para_into,259.1.1.1,6.1.1] bad1 bad2!=p1. 299 [binary,298.1,14.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file