define pyk of lemma exp(+1) 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 e unicode small x unicode small p unicode left parenthesis unicode plus sign unicode one unicode right parenthesis unicode end of text end unicode text end text end define
define tex of lemma exp(+1) as text unicode start of text unicode capital e unicode small x unicode small p unicode left parenthesis unicode plus sign unicode one unicode right parenthesis unicode end of text end unicode text end text end define
define statement of lemma exp(+1) as system Q infer all metavar var m end metavar indeed all metavar var x end metavar indeed metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar end define
define proof of lemma exp(+1) as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var m end metavar indeed all metavar var x end metavar indeed lemma +1IsPositive(N) conclude not0 0 <= metavar var m end metavar + 1 imply not0 not0 0 = metavar var m end metavar + 1 cut 1rule expPositive modus ponens not0 0 <= metavar var m end metavar + 1 imply not0 not0 0 = metavar var m end metavar + 1 conclude metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 cut lemma x=x+y-y conclude metavar var m end metavar = metavar var m end metavar + 1 + - 1 cut lemma sameExp modus ponens metavar var m end metavar = metavar var m end metavar + 1 + - 1 conclude metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 cut lemma eqMultiplicationLeft modus ponens metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 conclude metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 cut lemma eqSymmetry modus ponens metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 conclude metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar cut lemma eqTransitivity modus ponens metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 modus ponens metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar + 1 + - 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar conclude metavar var x end metavar ^ metavar var m end metavar + 1 = metavar var x end metavar * metavar var x end metavar ^ metavar var m end metavar end quote state proof state cache var c end expand end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,