Logiweb aspects of lemma equalsSameF in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma equalsSameF 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 q unicode small u unicode small a unicode small l unicode small s unicode capital 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 equalsSameF as text unicode start of text unicode capital e unicode small q unicode small u unicode small a unicode small l unicode small s unicode capital 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 equalsSameF as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed metavar var fx end metavar = metavar var fy 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 equalsSameF 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 metavar var fx end metavar = metavar var fy end metavar infer not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var infer 0 <= object var var m end var infer axiom natType conclude object var var m end var in0 N cut axiom seriesType conclude not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 metavar var fx end metavar imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 metavar var fx end metavar imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 metavar var fx end metavar imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 metavar var fx end metavar cut axiom seriesType conclude not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 metavar var fy end metavar imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 metavar var fy end metavar imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 metavar var fy end metavar imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 metavar var fy end metavar cut lemma eqReflexivity conclude object var var m end var = object var var m end var cut lemma sameSeries(Gen) modus ponens object var var m end var in0 N modus ponens object var var m end var in0 N modus ponens not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 metavar var fx end metavar imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 metavar var fx end metavar imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 metavar var fx end metavar imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 metavar var fx end metavar modus ponens not0 not0 for all objects object var var r1 end var indeed object var var r1 end var in0 metavar var fy end metavar imply not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 N imply not0 object var var op2 end var in0 Q imply not0 object var var r1 end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair imply not0 for all objects object var var f1 end var indeed for all objects object var var f2 end var indeed for all objects object var var f3 end var indeed for all objects object var var f4 end var indeed zermelo pair zermelo pair object var var f1 end var comma object var var f1 end var end pair comma zermelo pair object var var f1 end var comma object var var f2 end var end pair end pair in0 metavar var fy end metavar imply zermelo pair zermelo pair object var var f3 end var comma object var var f3 end var end pair comma zermelo pair object var var f3 end var comma object var var f4 end var end pair end pair in0 metavar var fy end metavar imply object var var f1 end var = object var var f3 end var imply object var var f2 end var = object var var f4 end var imply not0 for all objects object var var s1 end var indeed object var var s1 end var in0 N imply not0 for all objects object var var s2 end var indeed not0 zermelo pair zermelo pair object var var s1 end var comma object var var s1 end var end pair comma zermelo pair object var var s1 end var comma object var var s2 end var end pair end pair in0 metavar var fy end metavar modus ponens object var var m end var = object var var m end var modus ponens metavar var fx end metavar = metavar var fy end metavar conclude [ metavar var fx end metavar ; object var var m end var ] = [ metavar var fy end metavar ; object var var m end var ] cut lemma positiveToLeft(Eq)(1 term) modus ponens [ metavar var fx end metavar ; object var var m end var ] = [ metavar var fy end metavar ; object var var m end var ] conclude [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] = 0 cut lemma sameNumerical modus ponens [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] = 0 conclude | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = | 0 | cut lemma |0|=0 conclude | 0 | = 0 cut lemma eqTransitivity modus ponens | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = | 0 | modus ponens | 0 | = 0 conclude | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 0 cut lemma eqSymmetry modus ponens | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | = 0 conclude 0 = | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | cut lemma subLessLeft modus ponens 0 = | [ metavar var fx end metavar ; object var var m end var ] + - [ metavar var fy end metavar ; object var var m end var ] | modus ponens not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep 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 ] | <= 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 all metavar var fx end metavar indeed all metavar var fy end metavar indeed 1rule deduction modus ponens all metavar var fx end metavar indeed all metavar var fy end metavar indeed metavar var fx end metavar = metavar var fy end metavar infer not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var infer 0 <= object var var m end var infer 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 metavar var fx end metavar = metavar var fy end metavar imply not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply 0 <= 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 metavar var fx end metavar = metavar var fy end metavar infer 1rule mp modus ponens metavar var fx end metavar = metavar var fy end metavar imply not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply 0 <= 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 modus ponens metavar var fx end metavar = metavar var fy end metavar conclude not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply 0 <= 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 gen modus ponens not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply 0 <= 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 m end var indeed not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply 0 <= 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 pred lemma intro exist at 0 modus ponens 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 0 <= 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 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 gen 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 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 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