define pyk of lemma sameTelescope second 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 s unicode small a unicode small m unicode small e unicode capital 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 s unicode small e unicode small c unicode small o unicode small n unicode small d unicode end of text end unicode text end text end define
define tex of lemma sameTelescope second as text unicode start of text unicode capital s unicode small a unicode small m unicode small e unicode capital 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 two unicode right parenthesis unicode end of text end unicode text end text end define
define statement of lemma sameTelescope second as system Q infer all metavar var m end metavar indeed all metavar var n1 end metavar indeed all metavar var n2 end metavar indeed metavar var n1 end metavar = metavar var n2 end metavar infer UStelescope( metavar var m end metavar , metavar var n1 end metavar ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) end define
define proof of lemma sameTelescope second 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 n1 end metavar indeed all metavar var n2 end metavar indeed metavar var n1 end metavar = metavar var n2 end metavar infer lemma sameTelescope second base conclude for all objects metavar var n2 end metavar indeed 0 = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , 0 ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) cut lemma sameTelescope second indu conclude for all objects metavar var n2 end metavar indeed metavar var n1 end metavar = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , metavar var n1 end metavar ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) imply for all objects metavar var n2 end metavar indeed metavar var n1 end metavar + 1 = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , metavar var n1 end metavar + 1 ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) cut lemma induction modus ponens for all objects metavar var n2 end metavar indeed 0 = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , 0 ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) modus ponens for all objects metavar var n2 end metavar indeed metavar var n1 end metavar = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , metavar var n1 end metavar ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) imply for all objects metavar var n2 end metavar indeed metavar var n1 end metavar + 1 = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , metavar var n1 end metavar + 1 ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) conclude for all objects metavar var n2 end metavar indeed metavar var n1 end metavar = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , metavar var n1 end metavar ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) cut lemma a4 at metavar var n2 end metavar modus ponens for all objects metavar var n2 end metavar indeed metavar var n1 end metavar = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , metavar var n1 end metavar ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) conclude metavar var n1 end metavar = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , metavar var n1 end metavar ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) cut 1rule mp modus ponens metavar var n1 end metavar = metavar var n2 end metavar imply UStelescope( metavar var m end metavar , metavar var n1 end metavar ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) modus ponens metavar var n1 end metavar = metavar var n2 end metavar conclude UStelescope( metavar var m end metavar , metavar var n1 end metavar ) = UStelescope( metavar var m end metavar , metavar var n2 end metavar ) end quote state proof state cache var c end expand end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,