Logiweb aspects of axiom prime a four in pyk

Up Help

The user defined "the statement aspect" aspect

define statement of axiom prime a four as system prime 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 prime a four as rule tactic end define