define pyk of axiom three 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 t unicode small h unicode small r unicode small e unicode small e unicode end of text end unicode text end text end define
define tex of axiom three as text unicode start of text unicode capital a unicode three unicode end of text end unicode text end text end define
define statement of axiom three as prop theory infer ( ( ( not metavar var c end metavar ) imply not metavar var b end metavar ) imply ( ( ( not metavar var c end metavar ) imply metavar var b end metavar ) imply metavar var c end metavar ) ) end define
define proof of axiom three as rule tactic end define
The pyk compiler, version 0.grue.20050502 by Klaus Grue,