X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FFunctSums.ma;h=aeed9200cd628be08d26e015b0ff7aac0b3226cd;hb=ee9a771a3cf2124ef65906ae75eb0ba7e2e4303b;hp=5006a55f98b7ba36b8222f3768ea11b864043c31;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git
diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
index 5006a55f9..aeed9200c 100644
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
@@ -16,6 +16,8 @@
set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSums".
+include "CoRN.ma".
+
(* $Id: FunctSums.v,v 1.5 2004/04/23 10:00:59 lcf Exp $ *)
(*#* printing FSum0 %\ensuremath{\sum_0}% #∑0# *)
@@ -24,13 +26,9 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSums".
(*#* printing FSumx %\ensuremath{\sum'}% #∑'&*)
-(* INCLUDE
-CSumsReals
-*)
+include "reals/CSumsReals.ma".
-(* INCLUDE
-PartFunEquality
-*)
+include "ftc/PartFunEquality.ma".
(*#* *Sums of Functions
@@ -48,9 +46,9 @@ $\sum_{i=m}^nf_i$#the sum of fm through fn#
( [FSum]).
*)
-inline cic:/CoRN/ftc/FunctSums/FSum0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0.con".
-inline cic:/CoRN/ftc/FunctSums/FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum.con".
(*#*
Although [FSum] is here defined directly, it has the same relationship
@@ -62,37 +60,37 @@ mentioned, their forming too big a type makes it impossible to use
those results.
*)
-inline cic:/CoRN/ftc/FunctSums/FSum_FSum0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0.con".
-inline cic:/CoRN/ftc/FunctSums/FSum0_wd.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0_wd.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_one.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_one.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_first.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_first.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_last.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_last.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_last'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_last'.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_wd.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_wd.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_plus_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_plus_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/inv_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/inv_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_minus_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_minus_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_wd'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_wd'.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_resp_less.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_resp_less.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_resp_leEq.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_resp_leEq.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_comm_scal.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_comm_scal'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal'.con".
(*#*
Also important is the case when we have a finite family
@@ -100,15 +98,15 @@ $\{f_i\}_{i=0}^{n-1}$ of #exactly n# functions; in this case we need
to use the [FSumx] operator.
*)
-inline cic:/CoRN/ftc/FunctSums/FSumx.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx.con".
(*#*
This operator is well defined, as expected.
*)
-inline cic:/CoRN/ftc/FunctSums/FSumx_wd.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_wd.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_wd'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_wd'.con".
(*#*
As was already the case for [Sumx], in many cases we will need to
@@ -117,9 +115,9 @@ explicitly assume that $f_i$#f1# is independent of the proof that
function $f_i$#fi#.
*)
-inline cic:/CoRN/ftc/FunctSums/ext_fun_seq.con.
+inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq.con".
-inline cic:/CoRN/ftc/FunctSums/ext_fun_seq'.con.
+inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq'.con".
(* UNEXPORTED
Implicit Arguments ext_fun_seq [n].
@@ -133,35 +131,35 @@ Implicit Arguments ext_fun_seq' [n].
Under these assumptions, we can characterize the domain and the value of the sum function from the domains and values of the summands:
*)
-inline cic:/CoRN/ftc/FunctSums/FSumx_pred.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_pred.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_pred'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_pred'.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_char.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_char.con".
(*#*
As we did for arbitrary groups, it is often useful to rewrite this sums as ordinary sums.
*)
-inline cic:/CoRN/ftc/FunctSums/FSumx_to_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_to_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_lt.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_lt.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_le.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_le.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_FSumx_to_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSumx_to_FSum.con".
(*#*
Some useful lemmas follow.
*)
-inline cic:/CoRN/ftc/FunctSums/FSum0_0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0_0.con".
-inline cic:/CoRN/ftc/FunctSums/FSum0_S.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0_S.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_0.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_S.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_S.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_FSum0'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0'.con".