define pyk of lemma sameSeries(NumDiff) 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 s unicode small e unicode small r unicode small i unicode small e unicode small s unicode left parenthesis unicode capital n unicode small u unicode small m unicode capital d unicode small i unicode small f unicode small f unicode right parenthesis unicode end of text end unicode text end text end define
define tex of lemma sameSeries(NumDiff) as text unicode start of text unicode capital s unicode small a unicode small m unicode small e unicode capital s unicode small e unicode small r unicode small i unicode small e unicode small s unicode left parenthesis unicode capital n unicode small u unicode small m unicode capital d unicode small i unicode small f unicode small f unicode right parenthesis unicode end of text end unicode text end text end define
define statement of lemma sameSeries(NumDiff) as system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var o end metavar indeed all metavar var p end metavar indeed all metavar var n1 end metavar indeed all metavar var n2 end metavar indeed metavar var o end metavar = metavar var p end metavar infer metavar var n1 end metavar = metavar var n2 end metavar infer | [ metavar var fx end metavar ; metavar var o end metavar ] + - [ metavar var fy end metavar ; metavar var n1 end metavar ] | = | [ metavar var fx end metavar ; metavar var p end metavar ] + - [ metavar var fy end metavar ; metavar var n2 end metavar ] | end define
define proof of lemma sameSeries(NumDiff) as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var fx end metavar indeed all metavar var fy end metavar indeed all metavar var o end metavar indeed all metavar var p end metavar indeed all metavar var n1 end metavar indeed all metavar var n2 end metavar indeed metavar var o end metavar = metavar var p end metavar infer metavar var n1 end metavar = metavar var n2 end metavar infer lemma sameSeries modus ponens metavar var o end metavar = metavar var p end metavar conclude [ metavar var fx end metavar ; metavar var o end metavar ] = [ metavar var fx end metavar ; metavar var p end metavar ] cut lemma sameSeries modus ponens metavar var n1 end metavar = metavar var n2 end metavar conclude [ metavar var fy end metavar ; metavar var n1 end metavar ] = [ metavar var fy end metavar ; metavar var n2 end metavar ] cut lemma eqNegated modus ponens [ metavar var fy end metavar ; metavar var n1 end metavar ] = [ metavar var fy end metavar ; metavar var n2 end metavar ] conclude - [ metavar var fy end metavar ; metavar var n1 end metavar ] = - [ metavar var fy end metavar ; metavar var n2 end metavar ] cut lemma addEquations modus ponens [ metavar var fx end metavar ; metavar var o end metavar ] = [ metavar var fx end metavar ; metavar var p end metavar ] modus ponens - [ metavar var fy end metavar ; metavar var n1 end metavar ] = - [ metavar var fy end metavar ; metavar var n2 end metavar ] conclude [ metavar var fx end metavar ; metavar var o end metavar ] + - [ metavar var fy end metavar ; metavar var n1 end metavar ] = [ metavar var fx end metavar ; metavar var p end metavar ] + - [ metavar var fy end metavar ; metavar var n2 end metavar ] cut lemma sameNumerical modus ponens [ metavar var fx end metavar ; metavar var o end metavar ] + - [ metavar var fy end metavar ; metavar var n1 end metavar ] = [ metavar var fx end metavar ; metavar var p end metavar ] + - [ metavar var fy end metavar ; metavar var n2 end metavar ] conclude | [ metavar var fx end metavar ; metavar var o end metavar ] + - [ metavar var fy end metavar ; metavar var n1 end metavar ] | = | [ metavar var fx end metavar ; metavar var p end metavar ] + - [ metavar var fy 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,