define pyk of lemma sameBase(1/2)Sum 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 b unicode small a unicode small s unicode small e unicode left parenthesis unicode one unicode slash unicode two unicode right parenthesis unicode capital s unicode small u unicode small m 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 sameBase(1/2)Sum second as text unicode start of text unicode capital s unicode small a unicode small m unicode small e unicode capital b unicode capital s unicode left parenthesis unicode two unicode right parenthesis unicode end of text end unicode text end text end define
define statement of lemma sameBase(1/2)Sum 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 base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar ) = base(1/2)Sum( metavar var m end metavar , metavar var n2 end metavar ) end define
define proof of lemma sameBase(1/2)Sum 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 sameBase(1/2)Sum second base conclude for all objects metavar var n2 end metavar indeed 0 = metavar var n2 end metavar imply base(1/2)Sum( metavar var m end metavar , 0 ) = base(1/2)Sum( metavar var m end metavar , metavar var n2 end metavar ) cut lemma sameBase(1/2)Sum second indu conclude for all objects metavar var n2 end metavar indeed metavar var n1 end metavar = metavar var n2 end metavar imply base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar ) = base(1/2)Sum( 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 base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar + 1 ) = base(1/2)Sum( 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 base(1/2)Sum( metavar var m end metavar , 0 ) = base(1/2)Sum( 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 base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar ) = base(1/2)Sum( 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 base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar + 1 ) = base(1/2)Sum( 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 base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar ) = base(1/2)Sum( 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 base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar ) = base(1/2)Sum( metavar var m end metavar , metavar var n2 end metavar ) conclude metavar var n1 end metavar = metavar var n2 end metavar imply base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar ) = base(1/2)Sum( 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 base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar ) = base(1/2)Sum( metavar var m end metavar , metavar var n2 end metavar ) modus ponens metavar var n1 end metavar = metavar var n2 end metavar conclude base(1/2)Sum( metavar var m end metavar , metavar var n1 end metavar ) = base(1/2)Sum( 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,