Logiweb aspects of lemma sameExp indu in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma sameExp indu 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 a unicode small m unicode small e unicode capital e unicode small x unicode small p unicode space unicode small i unicode small n unicode small d unicode small u unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma sameExp indu as text unicode start of text unicode capital s unicode small a unicode small m unicode small e unicode capital e unicode small x unicode small p unicode left parenthesis unicode capital i unicode small n unicode small d unicode small u 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 sameExp indu as system Q infer all metavar var m end metavar indeed all metavar var n end metavar indeed all metavar var x end metavar indeed for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar imply for all objects metavar var n end metavar indeed metavar var m end metavar + 1 = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar end define

The user defined "the proof aspect" aspect

define proof of lemma sameExp indu as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var m end metavar indeed all metavar var n end metavar indeed all metavar var x end metavar indeed all metavar var m end metavar indeed all metavar var n end metavar indeed all metavar var x end metavar indeed for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar infer metavar var m end metavar + 1 = metavar var n end metavar infer lemma +1IsPositive(N) conclude not0 0 <= metavar var m end metavar + 1 imply not0 not0 0 = metavar var m end metavar + 1 cut 1rule expPositive modus ponens not0 0 <= metavar var m end metavar + 1 imply not0 not0 0 = metavar var m end metavar + 1 conclude metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 cut lemma x=x+y-y conclude metavar var m end metavar = metavar var m end metavar + 1 + - 1 cut lemma a4 at metavar var m end metavar + 1 + - 1 modus ponens for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar conclude metavar var m end metavar = metavar var m end metavar + 1 + - 1 imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 cut 1rule mp modus ponens metavar var m end metavar = metavar var m end metavar + 1 + - 1 imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 modus ponens metavar var m end metavar = metavar var m end metavar + 1 + - 1 conclude metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 cut lemma eqSymmetry modus ponens metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 conclude metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 = metavar var x end metavar ^ metavar var m end metavar cut lemma eqMultiplicationLeft modus ponens metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 = metavar var x end metavar ^ metavar var m end metavar conclude metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar cut lemma a4 at metavar var n end metavar + - 1 modus ponens for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar conclude metavar var m end metavar = metavar var n end metavar + - 1 imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar + - 1 cut lemma positiveToRight(Eq) modus ponens metavar var m end metavar + 1 = metavar var n end metavar conclude metavar var m end metavar = metavar var n end metavar + - 1 cut 1rule mp modus ponens metavar var m end metavar = metavar var n end metavar + - 1 imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar + - 1 modus ponens metavar var m end metavar = metavar var n end metavar + - 1 conclude metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar + - 1 cut lemma eqMultiplicationLeft modus ponens metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar + - 1 conclude metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar * metavar var x end metavar ^ metavar var n end metavar + - 1 cut lemma subLessRight modus ponens metavar var m end metavar + 1 = metavar var n end metavar modus ponens not0 0 <= metavar var m end metavar + 1 imply not0 not0 0 = metavar var m end metavar + 1 conclude not0 0 <= metavar var n end metavar imply not0 not0 0 = metavar var n end metavar cut 1rule expPositive modus ponens not0 0 <= metavar var n end metavar imply not0 not0 0 = metavar var n end metavar conclude metavar var x end metavar ^ metavar var n end metavar = metavar var x end metavar * metavar var x end metavar ^ metavar var n end metavar + - 1 cut lemma eqSymmetry modus ponens metavar var x end metavar ^ metavar var n end metavar = metavar var x end metavar * metavar var x end metavar ^ metavar var n end metavar + - 1 conclude metavar var x end metavar * metavar var x end metavar ^ metavar var n end metavar + - 1 = metavar var x end metavar ^ metavar var n end metavar cut lemma eqTransitivity5 modus ponens metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 modus ponens metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar modus ponens metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar * metavar var x end metavar ^ metavar var n end metavar + - 1 modus ponens metavar var x end metavar * metavar var x end metavar ^ metavar var n end metavar + - 1 = metavar var x end metavar ^ metavar var n end metavar conclude metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar cut 1rule deduction modus ponens all metavar var m end metavar indeed all metavar var n end metavar indeed all metavar var x end metavar indeed for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar infer metavar var m end metavar + 1 = metavar var n end metavar infer metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar conclude for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar imply metavar var m end metavar + 1 = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar cut for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar infer 1rule mp modus ponens for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar imply metavar var m end metavar + 1 = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar modus ponens for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar conclude metavar var m end metavar + 1 = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar cut 1rule gen modus ponens metavar var m end metavar + 1 = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar conclude for all objects metavar var n end metavar indeed metavar var m end metavar + 1 = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar cut all metavar var m end metavar indeed all metavar var n end metavar indeed all metavar var x end metavar indeed 1rule deduction modus ponens all metavar var m end metavar indeed all metavar var n end metavar indeed all metavar var x end metavar indeed for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar infer for all objects metavar var n end metavar indeed metavar var m end metavar + 1 = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar conclude for all objects metavar var n end metavar indeed metavar var m end metavar = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var n end metavar imply for all objects metavar var n end metavar indeed metavar var m end metavar + 1 = metavar var n end metavar imply metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar ^ metavar var n end metavar end quote state proof state cache var c end expand end define