Logiweb aspects of lemma eventually=f to sameF in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma eventually=f to sameF 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 e unicode small v unicode small e unicode small n unicode small t unicode small u unicode small a unicode small l unicode small l unicode small y unicode equal sign unicode small f unicode space unicode small t unicode small o unicode space unicode small s unicode small a unicode small m unicode small e unicode capital f unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma eventually=f to sameF as text unicode start of text unicode left parenthesis unicode capital e unicode small v unicode small e unicode small n unicode small t unicode small u unicode small a unicode small l unicode small l unicode small y unicode equal sign unicode small f unicode right parenthesis unicode two unicode small s unicode small a unicode small m unicode small e unicode capital f unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma eventually=f to sameF as system Q infer all metavar var m end metavar indeed all metavar var n end metavar indeed all metavar var fx end metavar indeed all metavar var fy end metavar indeed not0 for all objects metavar var n end metavar indeed not0 for all objects metavar var m end metavar indeed metavar var n end metavar <= metavar var m end metavar imply [ metavar var fx end metavar ; metavar var m end metavar ] = [ metavar var fy end metavar ; metavar var m end metavar ] infer 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 end define

The user defined "the proof aspect" aspect

define proof of lemma eventually=f to sameF 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 fx end metavar indeed all metavar var fy end metavar indeed not0 for all objects metavar var n end metavar indeed not0 for all objects metavar var m end metavar indeed metavar var n end metavar <= metavar var m end metavar imply [ metavar var fx end metavar ; metavar var m end metavar ] = [ metavar var fy end metavar ; metavar var m end metavar ] infer lemma eventually=f to sameF helper conclude for all objects metavar var m end metavar indeed metavar var n end metavar <= metavar var m end metavar imply [ metavar var fx end metavar ; metavar var m end metavar ] = [ metavar var fy end metavar ; metavar var m end metavar ] imply not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar cut pred lemma exist mp modus ponens for all objects metavar var m end metavar indeed metavar var n end metavar <= metavar var m end metavar imply [ metavar var fx end metavar ; metavar var m end metavar ] = [ metavar var fy end metavar ; metavar var m end metavar ] imply not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar modus ponens not0 for all objects metavar var n end metavar indeed not0 for all objects metavar var m end metavar indeed metavar var n end metavar <= metavar var m end metavar imply [ metavar var fx end metavar ; metavar var m end metavar ] = [ metavar var fy end metavar ; metavar var m end metavar ] conclude not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar cut 1rule gen modus ponens not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar conclude for all objects metavar var m end metavar indeed not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar cut pred lemma intro exist at metavar var n end metavar modus ponens for all objects metavar var m end metavar indeed not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar conclude not0 for all objects metavar var n end metavar indeed not0 for all objects metavar var m end metavar indeed not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar cut 1rule gen modus ponens not0 for all objects metavar var n end metavar indeed not0 for all objects metavar var m end metavar indeed not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar conclude for all objects metavar var ep end metavar indeed not0 for all objects metavar var n end metavar indeed not0 for all objects metavar var m end metavar indeed not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar cut 1rule deduction modus ponens for all objects metavar var ep end metavar indeed not0 for all objects metavar var n end metavar indeed not0 for all objects metavar var m end metavar indeed not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply metavar var n end metavar <= metavar var m end metavar imply not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | <= metavar var ep end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] | = metavar var ep end metavar 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 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 end quote state proof state cache var c end expand end define