X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCSums.ma;h=3930cbf9febd05b374bad1b227d8fee8c85f6638;hb=f2d9db85559c7a8db11aae1153495fae4a258d54;hp=0177138c73ca71f48d8378048b4fa3e102f01ed3;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma index 0177138c7..3930cbf9f 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma @@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums". +include "CoRN.ma". + (* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *) (*#* printing Sum0 %\ensuremath{\sum_0}% #∑0# *) @@ -28,13 +30,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums". (*#* printing Sumx %\ensuremath{\sum'}% #∑'&*) -(* INCLUDE -CAbGroups -*) - -(* INCLUDE -Peano_dec -*) +include "algebra/CAbGroups.ma". (*#* * Sums @@ -43,16 +39,16 @@ Peano_dec *) (* UNEXPORTED -Section Sums. +Section Sums *) -inline cic:/CoRN/algebra/CSums/G.var. +alias id "G" = "cic:/CoRN/algebra/CSums/Sums/G.var". (* Sum1 and Sum use subtraction *) -inline cic:/CoRN/algebra/CSums/Sumlist.con. +inline "cic:/CoRN/algebra/CSums/Sumlist.con". -inline cic:/CoRN/algebra/CSums/Sumx.con. +inline "cic:/CoRN/algebra/CSums/Sumx.con". (*#* It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$ @@ -60,140 +56,140 @@ 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 cic:/CoRN/algebra/CSums/part_tot_nat_fun.con. +inline "cic:/CoRN/algebra/CSums/part_tot_nat_fun.con". -inline cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con. +inline "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con". -inline cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con. +inline "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con". (*#* [Sum0] defines the sum for [i=0..(n-1)] *) -inline cic:/CoRN/algebra/CSums/Sum0.con. +inline "cic:/CoRN/algebra/CSums/Sum0.con". (*#* [Sum1] defines the sum for [i=m..(n-1)] *) -inline cic:/CoRN/algebra/CSums/Sum1.con. +inline "cic:/CoRN/algebra/CSums/Sum1.con". -inline cic:/CoRN/algebra/CSums/Sum.con. +inline "cic:/CoRN/algebra/CSums/Sum.con". (* 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 cic:/CoRN/algebra/CSums/Sum2.con. +inline "cic:/CoRN/algebra/CSums/Sum2.con". -inline cic:/CoRN/algebra/CSums/Sum_one.con. +inline "cic:/CoRN/algebra/CSums/Sum_one.con". (* UNEXPORTED Hint Resolve Sum_one: algebra. *) -inline cic:/CoRN/algebra/CSums/Sum_empty.con. +inline "cic:/CoRN/algebra/CSums/Sum_empty.con". (* UNEXPORTED Hint Resolve Sum_empty: algebra. *) -inline cic:/CoRN/algebra/CSums/Sum_Sum.con. +inline "cic:/CoRN/algebra/CSums/Sum_Sum.con". (* UNEXPORTED Hint Resolve Sum_Sum: algebra. *) -inline cic:/CoRN/algebra/CSums/Sum_first.con. +inline "cic:/CoRN/algebra/CSums/Sum_first.con". -inline cic:/CoRN/algebra/CSums/Sum_last.con. +inline "cic:/CoRN/algebra/CSums/Sum_last.con". (* UNEXPORTED Hint Resolve Sum_last: algebra. *) -inline cic:/CoRN/algebra/CSums/Sum_last'.con. +inline "cic:/CoRN/algebra/CSums/Sum_last'.con". (*#* We add some extensionality results which will be quite useful when working with integration. *) -inline cic:/CoRN/algebra/CSums/Sum0_strext.con. +inline "cic:/CoRN/algebra/CSums/Sum0_strext.con". -inline cic:/CoRN/algebra/CSums/Sum_strext.con. +inline "cic:/CoRN/algebra/CSums/Sum_strext.con". -inline cic:/CoRN/algebra/CSums/Sumx_strext.con. +inline "cic:/CoRN/algebra/CSums/Sumx_strext.con". -inline cic:/CoRN/algebra/CSums/Sum0_strext'.con. +inline "cic:/CoRN/algebra/CSums/Sum0_strext'.con". -inline cic:/CoRN/algebra/CSums/Sum_strext'.con. +inline "cic:/CoRN/algebra/CSums/Sum_strext'.con". -inline cic:/CoRN/algebra/CSums/Sum0_wd.con. +inline "cic:/CoRN/algebra/CSums/Sum0_wd.con". -inline cic:/CoRN/algebra/CSums/Sum_wd.con. +inline "cic:/CoRN/algebra/CSums/Sum_wd.con". -inline cic:/CoRN/algebra/CSums/Sumx_wd.con. +inline "cic:/CoRN/algebra/CSums/Sumx_wd.con". -inline cic:/CoRN/algebra/CSums/Sum_wd'.con. +inline "cic:/CoRN/algebra/CSums/Sum_wd'.con". -inline cic:/CoRN/algebra/CSums/Sum2_wd.con. +inline "cic:/CoRN/algebra/CSums/Sum2_wd.con". -inline cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con. +inline "cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con". (* UNEXPORTED Hint Resolve Sum0_plus_Sum0: algebra. *) -inline cic:/CoRN/algebra/CSums/Sum_plus_Sum.con. +inline "cic:/CoRN/algebra/CSums/Sum_plus_Sum.con". -inline cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con. +inline "cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con". -inline cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con. +inline "cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con". -inline cic:/CoRN/algebra/CSums/inv_Sum0.con. +inline "cic:/CoRN/algebra/CSums/inv_Sum0.con". (* UNEXPORTED Hint Resolve inv_Sum0: algebra. *) -inline cic:/CoRN/algebra/CSums/inv_Sum.con. +inline "cic:/CoRN/algebra/CSums/inv_Sum.con". (* UNEXPORTED Hint Resolve inv_Sum: algebra. *) -inline cic:/CoRN/algebra/CSums/inv_Sumx.con. +inline "cic:/CoRN/algebra/CSums/inv_Sumx.con". -inline cic:/CoRN/algebra/CSums/inv_Sum2.con. +inline "cic:/CoRN/algebra/CSums/inv_Sum2.con". -inline cic:/CoRN/algebra/CSums/Sum_minus_Sum.con. +inline "cic:/CoRN/algebra/CSums/Sum_minus_Sum.con". (* UNEXPORTED Hint Resolve Sum_minus_Sum: algebra. *) -inline cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con. +inline "cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con". -inline cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con. +inline "cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con". -inline cic:/CoRN/algebra/CSums/Sum_apzero.con. +inline "cic:/CoRN/algebra/CSums/Sum_apzero.con". -inline cic:/CoRN/algebra/CSums/Sum_zero.con. +inline "cic:/CoRN/algebra/CSums/Sum_zero.con". -inline cic:/CoRN/algebra/CSums/Sum_term.con. +inline "cic:/CoRN/algebra/CSums/Sum_term.con". -inline cic:/CoRN/algebra/CSums/Sum0_shift.con. +inline "cic:/CoRN/algebra/CSums/Sum0_shift.con". (* UNEXPORTED Hint Resolve Sum0_shift: algebra. *) -inline cic:/CoRN/algebra/CSums/Sum_shift.con. +inline "cic:/CoRN/algebra/CSums/Sum_shift.con". -inline cic:/CoRN/algebra/CSums/Sum_big_shift.con. +inline "cic:/CoRN/algebra/CSums/Sum_big_shift.con". -inline cic:/CoRN/algebra/CSums/Sumx_Sum0.con. +inline "cic:/CoRN/algebra/CSums/Sumx_Sum0.con". (* UNEXPORTED -End Sums. +End Sums *) (* UNEXPORTED @@ -220,21 +216,21 @@ often referred to as ``Mengolli Sums''. *) (* UNEXPORTED -Section More_Sums. +Section More_Sums *) -inline cic:/CoRN/algebra/CSums/G.var. +alias id "G" = "cic:/CoRN/algebra/CSums/More_Sums/G.var". -inline cic:/CoRN/algebra/CSums/Mengolli_Sum.con. +inline "cic:/CoRN/algebra/CSums/Mengolli_Sum.con". -inline cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con. +inline "cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con". -inline cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con. +inline "cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con". -inline cic:/CoRN/algebra/CSums/Sumx_to_Sum.con. +inline "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con". (* UNEXPORTED -End More_Sums. +End More_Sums *) (* UNEXPORTED