Logiweb aspects of lemma fpart-Bounded indu helper in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma fpart-Bounded indu helper 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 f unicode small p unicode small a unicode small r unicode small t unicode hyphen unicode capital b unicode small o unicode small u unicode small n unicode small d unicode small e unicode small d unicode space unicode small i unicode small n unicode small d unicode small u unicode space unicode small h unicode small e unicode small l unicode small p unicode small e unicode small r unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma fpart-Bounded indu helper as text unicode start of text unicode capital f unicode small p unicode small a unicode small r unicode small t unicode hyphen unicode capital b unicode small o unicode small u unicode small n unicode small d unicode small e unicode small d unicode left parenthesis unicode capital i unicode small n unicode small d unicode small u unicode capital h unicode small e unicode small l unicode small p unicode small e unicode small r unicode right parenthesis unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma fpart-Bounded indu helper as system Q infer all metavar var v1 end metavar indeed all metavar var v2n end metavar indeed all metavar var n end metavar indeed all metavar var fx end metavar indeed metavar var v2n end metavar <= metavar var n end metavar imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar infer metavar var v2n end metavar <= metavar var n end metavar + 1 infer not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) end define

The user defined "the proof aspect" aspect

define proof of lemma fpart-Bounded indu helper as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var v1 end metavar indeed all metavar var v2n end metavar indeed all metavar var n end metavar indeed all metavar var fx end metavar indeed metavar var v2n end metavar <= metavar var n end metavar imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar infer metavar var v2n end metavar <= metavar var n end metavar + 1 infer lemma leqLessEq modus ponens metavar var v2n end metavar <= metavar var n end metavar + 1 conclude not0 not0 metavar var v2n end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var v2n end metavar = metavar var n end metavar + 1 imply metavar var v2n end metavar = metavar var n end metavar + 1 cut all metavar var v1 end metavar indeed all metavar var v2n end metavar indeed all metavar var n end metavar indeed all metavar var fx end metavar indeed metavar var v2n end metavar <= metavar var n end metavar imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar infer not0 metavar var v2n end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var v2n end metavar = metavar var n end metavar + 1 infer 1rule lessMinus1(N) modus ponens not0 metavar var v2n end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var v2n end metavar = metavar var n end metavar + 1 conclude metavar var v2n end metavar <= metavar var n end metavar cut 1rule mp modus ponens metavar var v2n end metavar <= metavar var n end metavar imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar modus ponens metavar var v2n end metavar <= metavar var n end metavar conclude not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar cut lemma leqMax1 conclude metavar var v1 end metavar <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) cut lemma lessLeqTransitivity modus ponens not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar modus ponens metavar var v1 end metavar <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) conclude not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) cut all metavar var v1 end metavar indeed all metavar var v2n end metavar indeed all metavar var n end metavar indeed all metavar var fx end metavar indeed metavar var v2n end metavar = metavar var n end metavar + 1 infer lemma sameSeries modus ponens metavar var v2n end metavar = metavar var n end metavar + 1 conclude [ metavar var fx end metavar ; metavar var v2n end metavar ] = [ metavar var fx end metavar ; metavar var n end metavar + 1 ] cut lemma sameNumerical modus ponens [ metavar var fx end metavar ; metavar var v2n end metavar ] = [ metavar var fx end metavar ; metavar var n end metavar + 1 ] conclude | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | cut lemma eqLeq modus ponens | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | conclude | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | cut lemma leqPlus1 modus ponens | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | conclude not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 cut lemma leqMax2 conclude | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) cut lemma lessLeqTransitivity modus ponens not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 modus ponens | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) conclude not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) cut 1rule deduction modus ponens all metavar var v1 end metavar indeed all metavar var v2n end metavar indeed all metavar var n end metavar indeed all metavar var fx end metavar indeed metavar var v2n end metavar <= metavar var n end metavar imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar infer not0 metavar var v2n end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var v2n end metavar = metavar var n end metavar + 1 infer not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) conclude metavar var v2n end metavar <= metavar var n end metavar imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar imply not0 metavar var v2n end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var v2n end metavar = metavar var n end metavar + 1 imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) cut 1rule mp modus ponens metavar var v2n end metavar <= metavar var n end metavar imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar imply not0 metavar var v2n end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var v2n end metavar = metavar var n end metavar + 1 imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) modus ponens metavar var v2n end metavar <= metavar var n end metavar imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= metavar var v1 end metavar imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = metavar var v1 end metavar conclude not0 metavar var v2n end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var v2n end metavar = metavar var n end metavar + 1 imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) cut 1rule deduction modus ponens all metavar var v1 end metavar indeed all metavar var v2n end metavar indeed all metavar var n end metavar indeed all metavar var fx end metavar indeed metavar var v2n end metavar = metavar var n end metavar + 1 infer not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) conclude metavar var v2n end metavar = metavar var n end metavar + 1 imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) cut prop lemma from disjuncts modus ponens not0 not0 metavar var v2n end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var v2n end metavar = metavar var n end metavar + 1 imply metavar var v2n end metavar = metavar var n end metavar + 1 modus ponens not0 metavar var v2n end metavar <= metavar var n end metavar + 1 imply not0 not0 metavar var v2n end metavar = metavar var n end metavar + 1 imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) modus ponens metavar var v2n end metavar = metavar var n end metavar + 1 imply not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) conclude not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | <= if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) imply not0 not0 | [ metavar var fx end metavar ; metavar var v2n end metavar ] | = if( | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 <= metavar var v1 end metavar , metavar var v1 end metavar , | [ metavar var fx end metavar ; metavar var n end metavar + 1 ] | + 1 ) end quote state proof state cache var c end expand end define