define statement of axiom s nine as system s infer all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed sub zero quote metavar var b end metavar end quote is quote metavar var a end metavar end quote where quote metavar var x end metavar end quote is quote zero end quote end sub endorse sub zero quote metavar var c end metavar end quote is quote metavar var a end metavar end quote where quote metavar var x end metavar end quote is quote metavar var x end metavar suc end quote end sub endorse metavar var b end metavar infer metavar var a end metavar imply metavar var c end metavar infer metavar var a end metavar end define
define proof of axiom s nine as rule tactic end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,