define pyk of lemma a four as text unicode start of text unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode small a unicode space unicode small f unicode small o unicode small u unicode small r unicode end of text end unicode text end text end define
define tex of lemma a four as text unicode start of text unicode newline unicode capital a unicode four unicode apostrophe unicode end of text end unicode text end text end define
define statement of lemma a four as system s infer for all objects object var var x end var indeed for all objects object var var y end var indeed object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var imply two plus three equal three plus two end define
define proof of lemma a four as lambda var c dot lambda var x dot proof expand quote system s infer object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var infer repetition modus ponens object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var conclude object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var cut deduction modus ponens object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var infer object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var conclude for all objects object var var x end var indeed for all objects object var var y end var indeed object var var x end var plus object var var y end var equal object var var y end var plus object var var x end var imply two plus three equal three plus two end quote state proof state cache var c end expand end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,