Logiweb aspects of 1rule toSameF in pyk

Up Help

The predefined "pyk" aspect

define pyk of 1rule toSameF as text unicode start of text unicode one unicode small r unicode small u unicode small l unicode small e unicode space unicode small t unicode small o 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 1rule toSameF as text unicode start of text unicode capital t unicode small o unicode capital s unicode capital f unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of 1rule toSameF as system Q infer all metavar var m end metavar indeed all metavar var ep end metavar indeed all metavar var fx end metavar indeed all metavar var fy end metavar indeed not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar imply existential var var c end var <= metavar var m end metavar imply not0 if( 0 <= [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] , [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] , - [ 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 if( 0 <= [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] , [ metavar var fx end metavar ; metavar var m end metavar ] + - [ metavar var fy end metavar ; metavar var m end metavar ] , - [ 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 infer metavar var fx end metavar sameF metavar var fy end metavar end define

The user defined "the proof aspect" aspect

define proof of 1rule toSameF as rule tactic end define