define pyk of 1rule fromSameF as text unicode start of text unicode one unicode small r unicode small u unicode small l unicode small e unicode space unicode small f unicode small r unicode small o unicode small m 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 fromSameF as text unicode start of text unicode capital f unicode small r unicode small o unicode small m unicode capital s unicode capital f unicode end of text end unicode text end text end define
define statement of 1rule fromSameF 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 metavar var fx end metavar sameF metavar var fy end metavar infer not0 0 <= metavar var ep end metavar imply not0 not0 0 = metavar var ep end metavar infer 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 end define
define proof of 1rule fromSameF as rule tactic end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,