define pyk of lemma fromNotSameF(Strongest) helper2 as text unicode start of text unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode small f unicode small r unicode small o unicode small m unicode capital n unicode small o unicode small t unicode capital s unicode small a unicode small m unicode small e unicode capital f unicode left parenthesis unicode capital s unicode small t unicode small r unicode small o unicode small n unicode small g unicode small e unicode small s unicode small t unicode right parenthesis unicode space unicode small h unicode small e unicode small l unicode small p unicode small e unicode small r unicode two unicode end of text end unicode text end text end define
define tex of lemma fromNotSameF(Strongest) helper2 as text unicode start of text unicode small f unicode small r unicode small o unicode small m unicode capital n unicode small o unicode small t unicode capital s unicode small a unicode small m unicode small e unicode capital f unicode left parenthesis unicode capital s unicode small t unicode small r unicode small o unicode small n unicode small g unicode small e unicode small s unicode small t unicode right parenthesis unicode left parenthesis unicode capital h unicode small e unicode small l unicode small p unicode small e unicode small r unicode two unicode right parenthesis unicode end of text end unicode text end text end define
define statement of lemma fromNotSameF(Strongest) helper2 as system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed all metavar var u end metavar indeed all metavar var v end metavar indeed not0 | metavar var x end metavar + - metavar var y end metavar | <= 1/ 1 + 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var x end metavar + - metavar var y end metavar | = 1/ 1 + 1 + 1 * metavar var v end metavar infer not0 | metavar var z end metavar + - metavar var u end metavar | <= 1/ 1 + 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var z end metavar + - metavar var u end metavar | = 1/ 1 + 1 + 1 * metavar var v end metavar infer metavar var v end metavar <= | metavar var y end metavar + - metavar var u end metavar | infer not0 1/ 1 + 1 + 1 * metavar var v end metavar <= | metavar var x end metavar + - metavar var z end metavar | imply not0 not0 1/ 1 + 1 + 1 * metavar var v end metavar = | metavar var x end metavar + - metavar var z end metavar | end define
define proof of lemma fromNotSameF(Strongest) helper2 as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var z end metavar indeed all metavar var u end metavar indeed all metavar var v end metavar indeed not0 | metavar var x end metavar + - metavar var y end metavar | <= 1/ 1 + 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var x end metavar + - metavar var y end metavar | = 1/ 1 + 1 + 1 * metavar var v end metavar infer not0 | metavar var z end metavar + - metavar var u end metavar | <= 1/ 1 + 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var z end metavar + - metavar var u end metavar | = 1/ 1 + 1 + 1 * metavar var v end metavar infer metavar var v end metavar <= | metavar var y end metavar + - metavar var u end metavar | infer lemma numericalDifference conclude | metavar var x end metavar + - metavar var y end metavar | = | metavar var y end metavar + - metavar var x end metavar | cut lemma subLessLeft modus ponens | metavar var x end metavar + - metavar var y end metavar | = | metavar var y end metavar + - metavar var x end metavar | modus ponens not0 | metavar var x end metavar + - metavar var y end metavar | <= 1/ 1 + 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var x end metavar + - metavar var y end metavar | = 1/ 1 + 1 + 1 * metavar var v end metavar conclude not0 | metavar var y end metavar + - metavar var x end metavar | <= 1/ 1 + 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var y end metavar + - metavar var x end metavar | = 1/ 1 + 1 + 1 * metavar var v end metavar cut lemma lessNegated modus ponens not0 | metavar var y end metavar + - metavar var x end metavar | <= 1/ 1 + 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var y end metavar + - metavar var x end metavar | = 1/ 1 + 1 + 1 * metavar var v end metavar conclude not0 - 1/ 1 + 1 + 1 * metavar var v end metavar <= - | metavar var y end metavar + - metavar var x end metavar | imply not0 not0 - 1/ 1 + 1 + 1 * metavar var v end metavar = - | metavar var y end metavar + - metavar var x end metavar | cut lemma lessNegated modus ponens not0 | metavar var z end metavar + - metavar var u end metavar | <= 1/ 1 + 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var z end metavar + - metavar var u end metavar | = 1/ 1 + 1 + 1 * metavar var v end metavar conclude not0 - 1/ 1 + 1 + 1 * metavar var v end metavar <= - | metavar var z end metavar + - metavar var u end metavar | imply not0 not0 - 1/ 1 + 1 + 1 * metavar var v end metavar = - | metavar var z end metavar + - metavar var u end metavar | cut lemma addEquations(LeqLess) modus ponens metavar var v end metavar <= | metavar var y end metavar + - metavar var u end metavar | modus ponens not0 - 1/ 1 + 1 + 1 * metavar var v end metavar <= - | metavar var y end metavar + - metavar var x end metavar | imply not0 not0 - 1/ 1 + 1 + 1 * metavar var v end metavar = - | metavar var y end metavar + - metavar var x end metavar | conclude not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar <= | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | imply not0 not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar = | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | cut lemma addEquations(Less) modus ponens not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar <= | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | imply not0 not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar = | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | modus ponens not0 - 1/ 1 + 1 + 1 * metavar var v end metavar <= - | metavar var z end metavar + - metavar var u end metavar | imply not0 not0 - 1/ 1 + 1 + 1 * metavar var v end metavar = - | metavar var z end metavar + - metavar var u end metavar | conclude not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar <= | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | + - | metavar var z end metavar + - metavar var u end metavar | imply not0 not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar = | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | + - | metavar var z end metavar + - metavar var u end metavar | cut lemma insertTwoMiddleTerms(Numerical) conclude | metavar var y end metavar + - metavar var u end metavar | <= | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | cut axiom plusAssociativity conclude | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | = | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | cut axiom plusCommutativity conclude | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | = | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | + | metavar var y end metavar + - metavar var x end metavar | cut lemma eqTransitivity modus ponens | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | = | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | modus ponens | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | = | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | + | metavar var y end metavar + - metavar var x end metavar | conclude | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | = | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | + | metavar var y end metavar + - metavar var x end metavar | cut lemma subLeqRight modus ponens | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | = | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | + | metavar var y end metavar + - metavar var x end metavar | modus ponens | metavar var y end metavar + - metavar var u end metavar | <= | metavar var y end metavar + - metavar var x end metavar | + | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | conclude | metavar var y end metavar + - metavar var u end metavar | <= | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | + | metavar var y end metavar + - metavar var x end metavar | cut lemma positiveToLeft(Leq) modus ponens | metavar var y end metavar + - metavar var u end metavar | <= | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | + | metavar var y end metavar + - metavar var x end metavar | conclude | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | <= | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | cut lemma positiveToLeft(Leq) modus ponens | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | <= | metavar var x end metavar + - metavar var z end metavar | + | metavar var z end metavar + - metavar var u end metavar | conclude | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | + - | metavar var z end metavar + - metavar var u end metavar | <= | metavar var x end metavar + - metavar var z end metavar | cut lemma lessLeqTransitivity modus ponens not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar <= | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | + - | metavar var z end metavar + - metavar var u end metavar | imply not0 not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar = | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | + - | metavar var z end metavar + - metavar var u end metavar | modus ponens | metavar var y end metavar + - metavar var u end metavar | + - | metavar var y end metavar + - metavar var x end metavar | + - | metavar var z end metavar + - metavar var u end metavar | <= | metavar var x end metavar + - metavar var z end metavar | conclude not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar <= | metavar var x end metavar + - metavar var z end metavar | imply not0 not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar = | metavar var x end metavar + - metavar var z end metavar | cut lemma (1/3)x+(1/3)x+(1/3)x=x conclude 1/ 1 + 1 + 1 * metavar var v end metavar + 1/ 1 + 1 + 1 * metavar var v end metavar + 1/ 1 + 1 + 1 * metavar var v end metavar = metavar var v end metavar cut lemma positiveToRight(Eq) modus ponens 1/ 1 + 1 + 1 * metavar var v end metavar + 1/ 1 + 1 + 1 * metavar var v end metavar + 1/ 1 + 1 + 1 * metavar var v end metavar = metavar var v end metavar conclude 1/ 1 + 1 + 1 * metavar var v end metavar + 1/ 1 + 1 + 1 * metavar var v end metavar = metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar cut lemma positiveToRight(Eq) modus ponens 1/ 1 + 1 + 1 * metavar var v end metavar + 1/ 1 + 1 + 1 * metavar var v end metavar = metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar conclude 1/ 1 + 1 + 1 * metavar var v end metavar = metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar cut lemma eqSymmetry modus ponens 1/ 1 + 1 + 1 * metavar var v end metavar = metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar conclude metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar = 1/ 1 + 1 + 1 * metavar var v end metavar cut lemma subLessLeft modus ponens metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar = 1/ 1 + 1 + 1 * metavar var v end metavar modus ponens not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar <= | metavar var x end metavar + - metavar var z end metavar | imply not0 not0 metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 + 1 * metavar var v end metavar = | metavar var x end metavar + - metavar var z end metavar | conclude not0 1/ 1 + 1 + 1 * metavar var v end metavar <= | metavar var x end metavar + - metavar var z end metavar | imply not0 not0 1/ 1 + 1 + 1 * metavar var v end metavar = | metavar var x end metavar + - metavar var z end metavar | end quote state proof state cache var c end expand end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,