define pyk of lemma UStelescope zero exact as text unicode start of text unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode capital u unicode capital s unicode small t unicode small e unicode small l unicode small e unicode small s unicode small c unicode small o unicode small p unicode small e unicode space unicode small z unicode small e unicode small r unicode small o unicode space unicode small e unicode small x unicode small a unicode small c unicode small t unicode end of text end unicode text end text end define
define tex of lemma UStelescope zero exact as text unicode start of text unicode capital u unicode capital s unicode small t unicode small e unicode small l unicode small e unicode small s unicode small c unicode small o unicode small p unicode small e unicode left parenthesis unicode capital z unicode small e unicode small r unicode small o unicode right parenthesis unicode left parenthesis unicode capital e unicode small x unicode small a unicode small c unicode small t unicode right parenthesis unicode end of text end unicode text end text end define
define statement of lemma UStelescope zero exact as system Q infer all metavar var m end metavar indeed UStelescope( metavar var m end metavar , 0 ) = | [ us ; metavar var m end metavar ] + - [ us ; metavar var m end metavar + 1 ] | end define
define proof of lemma UStelescope zero exact as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var m end metavar indeed lemma eqReflexivity conclude 0 = 0 cut 1rule UStelescope zero modus ponens 0 = 0 conclude UStelescope( metavar var m end metavar , 0 ) = | [ us ; metavar var m end metavar ] + - [ us ; metavar var m end metavar + 1 ] | end quote state proof state cache var c end expand end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,