define pyk of 1rule to==XX 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 equal sign unicode equal sign unicode capital x unicode capital x unicode end of text end unicode text end text end define
define tex of 1rule to==XX as text unicode start of text unicode capital t unicode small o unicode equal sign unicode equal sign unicode capital x unicode capital x unicode end of text end unicode text end text end define
define statement of 1rule to==XX as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var rx end metavar indeed all metavar var ry end metavar indeed metavar var fx end metavar in0 metavar var rx end metavar imply metavar var fy end metavar in0 metavar var ry end metavar imply metavar var fx end metavar sameF metavar var fy end metavar infer metavar var rx end metavar == metavar var ry end metavar end define
define proof of 1rule to==XX as rule tactic end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,