Logiweb aspects of 1rule fromUpperBound in pyk

Up Help

The predefined "pyk" aspect

define pyk of 1rule fromUpperBound 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 u unicode small p unicode small p unicode small e unicode small r unicode capital b unicode small o unicode small u unicode small n unicode small d unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of 1rule fromUpperBound as text unicode start of text unicode capital f unicode small r unicode small o unicode small m unicode capital u unicode small p unicode small p unicode small e unicode small r unicode capital b unicode small o unicode small u unicode small n unicode small d unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of 1rule fromUpperBound as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var fxs end metavar indeed upperBound( metavar var fy end metavar , metavar var fxs end metavar ) infer metavar var fx end metavar in0 metavar var fxs end metavar infer not0 not0 for all objects object var var ep end var indeed not0 not0 for all objects object var var n end var indeed not0 for all objects object var var m end var indeed not0 not0 0 <= object var var ep end var imply not0 not0 0 = object var var ep end var imply not0 object var var n end var <= object var var m end var imply [ var x ; object var var m end var ] <= [ var y ; object var var m end var ] + - object var var ep end var imply metavar var fx end metavar = metavar var fy end metavar end define

The user defined "the proof aspect" aspect

define proof of 1rule fromUpperBound as rule tactic end define