Logiweb aspects of axiom a four in pyk

Up Help

The predefined "pyk" aspect

define pyk of axiom a four as text unicode start of text unicode small a unicode small x unicode small i unicode small o unicode small m unicode space unicode small a unicode space unicode small f unicode small o unicode small u unicode small r unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of axiom a four as text unicode start of text unicode newline unicode capital a unicode four unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of axiom a four as system s infer all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed ( peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse ( ( peano all metavar var x end metavar indeed metavar var b end metavar ) peano imply metavar var a end metavar ) ) end define

The user defined "the proof aspect" aspect

define proof of axiom a four as rule tactic end define