X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Falgebra%2FCSums.mma;h=57ece830d5a947667dbbb1a1342cb74a24816d96;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=5bb30914eb077b7d58f80969e255cb7a7c36bd8e;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Procedural/algebra/CSums.mma b/helm/software/matita/contribs/CoRN-Procedural/algebra/CSums.mma index 5bb30914e..57ece830d 100644 --- a/helm/software/matita/contribs/CoRN-Procedural/algebra/CSums.mma +++ b/helm/software/matita/contribs/CoRN-Procedural/algebra/CSums.mma @@ -44,9 +44,9 @@ alias id "G" = "cic:/CoRN/algebra/CSums/Sums/G.var". (* Sum1 and Sum use subtraction *) -inline procedural "cic:/CoRN/algebra/CSums/Sumlist.con". +inline procedural "cic:/CoRN/algebra/CSums/Sumlist.con" as definition. -inline procedural "cic:/CoRN/algebra/CSums/Sumx.con". +inline procedural "cic:/CoRN/algebra/CSums/Sumx.con" as definition. (*#* It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$ @@ -54,137 +54,137 @@ It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$ [Zero] when the input is greater than or equal to [i]. *) -inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun.con". +inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun.con" as definition. -inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con". +inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con". +inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con" as lemma. (*#* [Sum0] defines the sum for [i=0..(n-1)] *) -inline procedural "cic:/CoRN/algebra/CSums/Sum0.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum0.con" as definition. (*#* [Sum1] defines the sum for [i=m..(n-1)] *) -inline procedural "cic:/CoRN/algebra/CSums/Sum1.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum1.con" as definition. -inline procedural "cic:/CoRN/algebra/CSums/Sum.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum.con" as definition. (* Sum i=m..n *) (*#* [Sum2] is similar to [Sum1], but does not require the summand to be defined outside where it is being added. *) -inline procedural "cic:/CoRN/algebra/CSums/Sum2.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum2.con" as definition. -inline procedural "cic:/CoRN/algebra/CSums/Sum_one.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_one.con" as lemma. (* UNEXPORTED Hint Resolve Sum_one: algebra. *) -inline procedural "cic:/CoRN/algebra/CSums/Sum_empty.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_empty.con" as lemma. (* UNEXPORTED Hint Resolve Sum_empty: algebra. *) -inline procedural "cic:/CoRN/algebra/CSums/Sum_Sum.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_Sum.con" as lemma. (* UNEXPORTED Hint Resolve Sum_Sum: algebra. *) -inline procedural "cic:/CoRN/algebra/CSums/Sum_first.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_first.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_last.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_last.con" as lemma. (* UNEXPORTED Hint Resolve Sum_last: algebra. *) -inline procedural "cic:/CoRN/algebra/CSums/Sum_last'.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_last'.con" as lemma. (*#* We add some extensionality results which will be quite useful when working with integration. *) -inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_strext.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_strext.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sumx_strext.con". +inline procedural "cic:/CoRN/algebra/CSums/Sumx_strext.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext'.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext'.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_strext'.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_strext'.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum0_wd.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum0_wd.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_wd.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_wd.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sumx_wd.con". +inline procedural "cic:/CoRN/algebra/CSums/Sumx_wd.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_wd'.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_wd'.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum2_wd.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum2_wd.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con" as lemma. (* UNEXPORTED Hint Resolve Sum0_plus_Sum0: algebra. *) -inline procedural "cic:/CoRN/algebra/CSums/Sum_plus_Sum.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_plus_Sum.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con". +inline procedural "cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/inv_Sum0.con". +inline procedural "cic:/CoRN/algebra/CSums/inv_Sum0.con" as lemma. (* UNEXPORTED Hint Resolve inv_Sum0: algebra. *) -inline procedural "cic:/CoRN/algebra/CSums/inv_Sum.con". +inline procedural "cic:/CoRN/algebra/CSums/inv_Sum.con" as lemma. (* UNEXPORTED Hint Resolve inv_Sum: algebra. *) -inline procedural "cic:/CoRN/algebra/CSums/inv_Sumx.con". +inline procedural "cic:/CoRN/algebra/CSums/inv_Sumx.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/inv_Sum2.con". +inline procedural "cic:/CoRN/algebra/CSums/inv_Sum2.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_minus_Sum.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_minus_Sum.con" as lemma. (* UNEXPORTED Hint Resolve Sum_minus_Sum: algebra. *) -inline procedural "cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con". +inline procedural "cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_apzero.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_apzero.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_zero.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_zero.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_term.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_term.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum0_shift.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum0_shift.con" as lemma. (* UNEXPORTED Hint Resolve Sum0_shift: algebra. *) -inline procedural "cic:/CoRN/algebra/CSums/Sum_shift.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_shift.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sum_big_shift.con". +inline procedural "cic:/CoRN/algebra/CSums/Sum_big_shift.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sumx_Sum0.con". +inline procedural "cic:/CoRN/algebra/CSums/Sumx_Sum0.con" as lemma. (* UNEXPORTED End Sums @@ -219,13 +219,13 @@ Section More_Sums alias id "G" = "cic:/CoRN/algebra/CSums/More_Sums/G.var". -inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum.con". +inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con". +inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con". +inline procedural "cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con" as lemma. -inline procedural "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con". +inline procedural "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con" as lemma. (* UNEXPORTED End More_Sums