define pyk of 1rule fromLeq(Advanced)(N) 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 l unicode small e unicode small q unicode left parenthesis unicode capital a unicode small d unicode small v unicode small a unicode small n unicode small c unicode small e unicode small d unicode right parenthesis unicode left parenthesis unicode capital n unicode right parenthesis unicode end of text end unicode text end text end define
define tex of 1rule fromLeq(Advanced)(N) as text unicode start of text unicode capital f unicode small r unicode small o unicode small m unicode capital l unicode small e unicode small q unicode left parenthesis unicode capital a unicode small d unicode small v unicode small a unicode small n unicode small c unicode small e unicode small d unicode right parenthesis unicode left parenthesis unicode capital n unicode right parenthesis unicode end of text end unicode text end text end define
define statement of 1rule fromLeq(Advanced)(N) as system Q infer all metavar var m end metavar indeed all metavar var m1 end metavar indeed all metavar var n end metavar indeed metavar var m end metavar <= metavar var n end metavar infer not0 for all objects metavar var m1 end metavar indeed not0 metavar var m end metavar + metavar var m1 end metavar = metavar var n end metavar end define
define proof of 1rule fromLeq(Advanced)(N) as rule tactic end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,