define pyk of propositional theory as text unicode start of text unicode small p unicode small r unicode small o unicode small p unicode small o unicode small s unicode small i unicode small t unicode small i unicode small o unicode small n unicode small a unicode small l unicode space unicode small t unicode small h unicode small e unicode small o unicode small r unicode small y unicode end of text end unicode text end text end define
define tex of propositional theory as text unicode start of text unicode capital t unicode underscore unicode left brace unicode capital p unicode capital c unicode right brace unicode end of text end unicode text end text end define
define statement of propositional theory as ( all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed ( ( metavar var b end metavar imply ( metavar var c end metavar imply metavar var d end metavar ) ) imply ( ( metavar var b end metavar imply metavar var c end metavar ) imply ( metavar var b end metavar imply metavar var d end metavar ) ) ) ) rule plus ( ( all metavar var b end metavar indeed all metavar var c end metavar indeed ( metavar var b end metavar infer ( ( metavar var b end metavar imply metavar var c end metavar ) infer metavar var c end metavar ) ) ) rule plus ( ( all metavar var b end metavar indeed all metavar var c end metavar indeed ( metavar var b end metavar imply ( metavar var c end metavar imply metavar var b end metavar ) ) ) rule plus all metavar var b end metavar indeed all metavar var c end metavar indeed ( ( ( 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
The pyk compiler, version 0.grue.20050603 by Klaus Grue,