define pyk of lemma fromNotSameF(Strong) 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 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(Strong) helper2 as text unicode start of text unicode capital 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 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(Strong) 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 metavar var v end metavar <= | metavar var x end metavar + - metavar var z end metavar | infer not0 | metavar var x end metavar + - metavar var y end metavar | <= 1/ 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var x end metavar + - metavar var y end metavar | = 1/ 1 + 1 * metavar var v end metavar infer not0 | metavar var z end metavar + - metavar var u end metavar | <= 1/ 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var z end metavar + - metavar var u end metavar | = 1/ 1 + 1 * metavar var v end metavar infer not0 metavar var y end metavar = metavar var u end metavar end define
define proof of lemma fromNotSameF(Strong) 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 metavar var v end metavar <= | metavar var x end metavar + - metavar var z end metavar | infer not0 | metavar var x end metavar + - metavar var y end metavar | <= 1/ 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var x end metavar + - metavar var y end metavar | = 1/ 1 + 1 * metavar var v end metavar infer not0 | metavar var z end metavar + - metavar var u end metavar | <= 1/ 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var z end metavar + - metavar var u end metavar | = 1/ 1 + 1 * metavar var v end metavar infer lemma lessNegated modus ponens not0 | metavar var x end metavar + - metavar var y end metavar | <= 1/ 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var x end metavar + - metavar var y end metavar | = 1/ 1 + 1 * metavar var v end metavar conclude not0 - 1/ 1 + 1 * metavar var v end metavar <= - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 - 1/ 1 + 1 * metavar var v end metavar = - | metavar var x end metavar + - metavar var y end metavar | cut lemma numericalDifference conclude | metavar var z end metavar + - metavar var u end metavar | = | metavar var u end metavar + - metavar var z end metavar | cut lemma subLessLeft modus ponens | metavar var z end metavar + - metavar var u end metavar | = | metavar var u end metavar + - metavar var z end metavar | modus ponens not0 | metavar var z end metavar + - metavar var u end metavar | <= 1/ 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var z end metavar + - metavar var u end metavar | = 1/ 1 + 1 * metavar var v end metavar conclude not0 | metavar var u end metavar + - metavar var z end metavar | <= 1/ 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var u end metavar + - metavar var z end metavar | = 1/ 1 + 1 * metavar var v end metavar cut lemma lessNegated modus ponens not0 | metavar var u end metavar + - metavar var z end metavar | <= 1/ 1 + 1 * metavar var v end metavar imply not0 not0 | metavar var u end metavar + - metavar var z end metavar | = 1/ 1 + 1 * metavar var v end metavar conclude not0 - 1/ 1 + 1 * metavar var v end metavar <= - | metavar var u end metavar + - metavar var z end metavar | imply not0 not0 - 1/ 1 + 1 * metavar var v end metavar = - | metavar var u end metavar + - metavar var z end metavar | cut lemma addEquations(Less) modus ponens not0 - 1/ 1 + 1 * metavar var v end metavar <= - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 - 1/ 1 + 1 * metavar var v end metavar = - | metavar var x end metavar + - metavar var y end metavar | modus ponens not0 - 1/ 1 + 1 * metavar var v end metavar <= - | metavar var u end metavar + - metavar var z end metavar | imply not0 not0 - 1/ 1 + 1 * metavar var v end metavar = - | metavar var u end metavar + - metavar var z end metavar | conclude not0 - 1/ 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 * metavar var v end metavar <= - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | imply not0 not0 - 1/ 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 * metavar var v end metavar = - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | cut lemma (1/2)x+(1/2)x=x conclude 1/ 1 + 1 * metavar var v end metavar + 1/ 1 + 1 * metavar var v end metavar = metavar var v end metavar cut lemma eqNegated modus ponens 1/ 1 + 1 * metavar var v end metavar + 1/ 1 + 1 * metavar var v end metavar = metavar var v end metavar conclude - 1/ 1 + 1 * metavar var v end metavar + 1/ 1 + 1 * metavar var v end metavar = - metavar var v end metavar cut lemma -x-y=-(x+y) conclude - 1/ 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 * metavar var v end metavar = - 1/ 1 + 1 * metavar var v end metavar + 1/ 1 + 1 * metavar var v end metavar cut lemma eqTransitivity modus ponens - 1/ 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 * metavar var v end metavar = - 1/ 1 + 1 * metavar var v end metavar + 1/ 1 + 1 * metavar var v end metavar modus ponens - 1/ 1 + 1 * metavar var v end metavar + 1/ 1 + 1 * metavar var v end metavar = - metavar var v end metavar conclude - 1/ 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 * metavar var v end metavar = - metavar var v end metavar cut lemma subLessLeft modus ponens - 1/ 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 * metavar var v end metavar = - metavar var v end metavar modus ponens not0 - 1/ 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 * metavar var v end metavar <= - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | imply not0 not0 - 1/ 1 + 1 * metavar var v end metavar + - 1/ 1 + 1 * metavar var v end metavar = - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | conclude not0 - metavar var v end metavar <= - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | imply not0 not0 - metavar var v end metavar = - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | cut axiom plusCommutativity conclude - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | = - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | cut lemma subLessRight modus ponens - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | = - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | modus ponens not0 - metavar var v end metavar <= - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | imply not0 not0 - metavar var v end metavar = - | metavar var x end metavar + - metavar var y end metavar | + - | metavar var u end metavar + - metavar var z end metavar | conclude not0 - metavar var v end metavar <= - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 - metavar var v end metavar = - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | cut lemma addEquations(LeqLess) modus ponens metavar var v end metavar <= | metavar var x end metavar + - metavar var z end metavar | modus ponens not0 - metavar var v end metavar <= - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 - metavar var v end metavar = - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | conclude not0 metavar var v end metavar + - metavar var v end metavar <= | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 metavar var v end metavar + - metavar var v end metavar = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | cut axiom negative conclude metavar var v end metavar + - metavar var v end metavar = 0 cut lemma subLessLeft modus ponens metavar var v end metavar + - metavar var v end metavar = 0 modus ponens not0 metavar var v end metavar + - metavar var v end metavar <= | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 metavar var v end metavar + - metavar var v end metavar = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | conclude not0 0 <= | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 0 = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | cut axiom plusAssociativity conclude | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | cut lemma eqSymmetry modus ponens | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | conclude | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | cut lemma subLessRight modus ponens | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | modus ponens not0 0 <= | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 0 = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | conclude not0 0 <= | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 0 = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | cut lemma insertTwoMiddleTerms(Numerical) conclude | metavar var x end metavar + - metavar var z end metavar | <= | metavar var x end metavar + - metavar var y end metavar | + | metavar var y end metavar + - metavar var u end metavar | + | metavar var u end metavar + - metavar var z end metavar | cut lemma positiveToLeft(Leq) modus ponens | metavar var x end metavar + - metavar var z end metavar | <= | metavar var x end metavar + - metavar var y end metavar | + | metavar var y end metavar + - metavar var u end metavar | + | metavar var u end metavar + - metavar var z end metavar | conclude | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | <= | metavar var x end metavar + - metavar var y end metavar | + | metavar var y end metavar + - metavar var u end metavar | cut axiom plusCommutativity conclude | metavar var x end metavar + - metavar var y end metavar | + | metavar var y end metavar + - metavar var u end metavar | = | metavar var y end metavar + - metavar var u end metavar | + | metavar var x end metavar + - metavar var y end metavar | cut lemma subLeqRight modus ponens | metavar var x end metavar + - metavar var y end metavar | + | metavar var y end metavar + - metavar var u end metavar | = | metavar var y end metavar + - metavar var u end metavar | + | metavar var x end metavar + - metavar var y end metavar | modus ponens | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | <= | metavar var x end metavar + - metavar var y end metavar | + | metavar var y end metavar + - metavar var u end metavar | conclude | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | <= | metavar var y end metavar + - metavar var u end metavar | + | metavar var x end metavar + - metavar var y end metavar | cut lemma positiveToLeft(Leq) modus ponens | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | <= | metavar var y end metavar + - metavar var u end metavar | + | metavar var x end metavar + - metavar var y end metavar | conclude | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | <= | metavar var y end metavar + - metavar var u end metavar | cut lemma lessLeqTransitivity modus ponens not0 0 <= | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | imply not0 not0 0 = | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | modus ponens | metavar var x end metavar + - metavar var z end metavar | + - | metavar var u end metavar + - metavar var z end metavar | + - | metavar var x end metavar + - metavar var y end metavar | <= | metavar var y end metavar + - metavar var u end metavar | conclude not0 0 <= | metavar var y end metavar + - metavar var u end metavar | imply not0 not0 0 = | metavar var y end metavar + - metavar var u end metavar | cut lemma fromPositiveNumerical modus ponens not0 0 <= | metavar var y end metavar + - metavar var u end metavar | imply not0 not0 0 = | metavar var y end metavar + - metavar var u end metavar | conclude not0 metavar var y end metavar + - metavar var u end metavar = 0 cut lemma negativeToRight(Neq)(1 term) modus ponens not0 metavar var y end metavar + - metavar var u end metavar = 0 conclude not0 metavar var y end metavar = metavar var u end metavar end quote state proof state cache var c end expand end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,