Logiweb aspects of lemma subLessRight(F) in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma subLessRight(F) 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 s unicode small u unicode small b unicode capital l unicode small e unicode small s unicode small s unicode capital r unicode small i unicode small g unicode small h unicode small t unicode left parenthesis unicode capital f unicode right parenthesis unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma subLessRight(F) as text unicode start of text unicode capital s unicode small u unicode small b unicode capital l unicode small e unicode small s unicode small s unicode capital r unicode small i unicode small g unicode small h unicode small t unicode left parenthesis unicode capital f unicode right parenthesis unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma subLessRight(F) as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = object var var ep end var infer not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var infer not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - object var var ep end var end define

The user defined "the proof aspect" aspect

define proof of lemma subLessRight(F) as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = object var var ep end var infer not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var infer 1rule repetition modus ponens for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = object var var ep end var conclude for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = object var var ep end var cut 1rule deduction modus ponens for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = object var var ep end var conclude for all objects object var var ep end var indeed not0 for all objects object var var n1 end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = object var var ep end var cut lemma a4 at 1/ 1 + 1 + 1 * object var var ep end var modus ponens for all objects object var var ep end var indeed not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply object var var n end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = object var var ep end var conclude not0 for all objects object var var n1 end var indeed not0 for all objects object var var m end var indeed not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var cut 1rule repetition modus ponens not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var conclude not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var cut 1rule deduction modus ponens not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var conclude not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n2 end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var cut all metavar var fx end metavar indeed all metavar var fx end metavar indeed all metavar var fz end metavar indeed for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var infer lemma a4 at object var var m end var modus ponens for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var conclude not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var cut prop lemma first conjunct modus ponens not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var conclude not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var cut lemma positiveDividedBy3 modus ponens not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var conclude not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var cut all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed for all objects object var var m end var indeed not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var infer for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var infer if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var infer lemma leqMax1 conclude object var var n1 end var <= if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) cut lemma leqTransitivity modus ponens object var var n1 end var <= if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) modus ponens if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var conclude object var var n1 end var <= object var var m end var cut lemma leqMax2 conclude object var var n2 end var <= if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) cut lemma leqTransitivity modus ponens object var var n2 end var <= if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) modus ponens if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var conclude object var var n2 end var <= object var var m end var cut lemma a4 at object var var m end var modus ponens for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var conclude not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var cut prop lemma first conjunct modus ponens not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var conclude not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var cut prop lemma second conjunct modus ponens not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var conclude object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var cut 1rule mp modus ponens object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var modus ponens object var var n2 end var <= object var var m end var conclude [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var cut lemma a4 at object var var m end var modus ponens for all objects object var var m end var indeed not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var conclude not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var cut lemma positiveDividedBy3 modus ponens not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var conclude not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var cut prop lemma mp2 modus ponens not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var modus ponens not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var modus ponens object var var n1 end var <= object var var m end var conclude not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var cut lemma closetogreaterIsGreater modus ponens [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var modus ponens not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var conclude [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var cut 1rule deduction modus ponens all metavar var fx end metavar indeed all metavar var fx end metavar indeed all metavar var fz end metavar indeed for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var infer not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var conclude for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var imply not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var cut pred lemma 2exist mp modus ponens for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var imply not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var modus ponens not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n2 end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var conclude not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var cut 1rule deduction modus ponens all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fz end metavar indeed for all objects object var var m end var indeed not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var infer for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var infer if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var infer [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var conclude for all objects object var var m end var indeed not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var imply for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var imply if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var cut pred lemma exist mp modus ponens for all objects object var var m end var indeed not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var imply for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var imply if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var modus ponens not0 for all objects object var var n1 end var indeed not0 for all objects object var var m end var indeed not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply object var var n1 end var <= object var var m end var imply not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 1/ 1 + 1 + 1 * object var var ep end var conclude for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var imply if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var cut pred lemma 2exist mp modus ponens for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var imply if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var modus ponens not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n2 end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n2 end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fx end metavar ; object var var m end var ] + - object var var ep end var conclude if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var cut prop lemma join conjuncts modus ponens not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var modus ponens if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var conclude not0 not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply not0 if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var cut 1rule gen modus ponens not0 not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply not0 if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var conclude for all objects object var var m end var indeed not0 not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply not0 if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var cut pred lemma intro exist at if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) modus ponens for all objects object var var m end var indeed not0 not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply not0 if( object var var n2 end var <= object var var n1 end var , object var var n1 end var , object var var n2 end var ) <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var conclude not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var cut pred lemma intro exist at 1/ 1 + 1 + 1 * object var var ep end var modus ponens not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= 1/ 1 + 1 + 1 * object var var ep end var imply not0 not0 0 = 1/ 1 + 1 + 1 * object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - 1/ 1 + 1 + 1 * object var var ep end var conclude not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - object var var ep end var cut 1rule repetition modus ponens not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - object var var ep end var conclude not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ metavar var fz end metavar ; object var var m end var ] <= [ metavar var fy end metavar ; object var var m end var ] + - object var var ep end var end quote state proof state cache var c end expand end define