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
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
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
define proof of 1rule toSameF as rule tactic end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,