define pyk of hypothesize plus plus as text unicode start of text unicode small h unicode small y unicode small p unicode small o unicode small t unicode small h unicode small e unicode small s unicode small i unicode small z unicode small e unicode space unicode small p unicode small l unicode small u unicode small s unicode space unicode small p unicode small l unicode small u unicode small s unicode end of text end unicode text end text end define
define tex of hypothesize plus plus as text unicode start of text unicode newline unicode capital t unicode small i unicode small l unicode small f unicode backslash unicode small o unicode space unicode small j unicode space unicode space unicode small h unicode small y unicode small p unicode small o unicode small t unicode small e unicode small s unicode small e unicode underscore unicode plus sign unicode end of text end unicode text end text end define
define statement of hypothesize plus plus as system prime s infer all metavar var i end metavar indeed all metavar var h end metavar indeed all metavar var a end metavar indeed ( metavar var a end metavar infer ( metavar var i end metavar peano imply ( metavar var h end metavar peano imply metavar var a end metavar ) ) ) end define
define proof of hypothesize plus plus as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var i end metavar indeed all metavar var h end metavar indeed all metavar var a end metavar indeed ( metavar var a end metavar infer ( ( ( hypothesize modus ponens metavar var a end metavar ) conclude ( metavar var h end metavar peano imply metavar var a end metavar ) ) cut ( ( hypothesize modus ponens ( metavar var h end metavar peano imply metavar var a end metavar ) ) conclude ( metavar var i end metavar peano imply ( metavar var h end metavar peano imply metavar var a end metavar ) ) ) ) ) end quote state proof state cache var c end expand end define
The pyk compiler, version 0.grue.20050603 by Klaus Grue,