...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / ftc / TaylorLemma.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/TaylorLemma.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/TaylorLemma.mma
index 8b016e4f289a64676ddbd8f62b56148df5e33d36..6f2e563519fe435cea64e40c2a1d770485c3eced 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/TaylorLemma.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/TaylorLemma.mma
@@ -42,31 +42,43 @@ define the nth order derivative of [F] in the interval
 [[Min(a,b),Max(a,b)]].
 *)
 
-alias id "a" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/b.var
+*)
 
-alias id "Hap" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hap.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hap.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab'.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab'.con" "Taylor_Defs__" as definition.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab.con" "Taylor_Defs__" as definition.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/I.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/I.con" "Taylor_Defs__" as definition.
 
 (* end hide *)
 
-alias id "F" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/F.var
+*)
 
-alias id "Ha" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Ha.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Ha.var
+*)
 
-alias id "Hb" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hb.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hb.var
+*)
 
 (* begin show *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/fi.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/fi.con" "Taylor_Defs__" as definition.
 
 (* end show *)
 
@@ -77,7 +89,7 @@ $f_i=f^{(i)}$#f<sub>i</sub>=f<sup>(i)</sup>#.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma1.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma1.con" as lemma.
 
 (* end hide *)
 
@@ -92,9 +104,9 @@ corresponding to [a] and [b].
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_a.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_a.con" "Taylor_Defs__" as definition.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_b.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_b.con" "Taylor_Defs__" as definition.
 
 (* NOTATION
 Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
@@ -108,33 +120,33 @@ Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
 
 (* begin show *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i.con" "Taylor_Defs__" as definition.
 
 (* end show *)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i'.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i'.con" "Taylor_Defs__" as definition.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i'.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_a_i'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i'.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_b_i'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i'.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_x_i'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2'.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3'.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3'.con" as lemma.
 
 (* end hide *)
 
@@ -143,13 +155,13 @@ Adding the previous expressions up to a given bound [n] gives us the
 Taylor sum of order [n].
 *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'.con" as definition.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Taylor_seq'_aux.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Taylor_seq'_aux.con" "Taylor_Defs__" as definition.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con" as lemma.
 
 (* end hide *)
 
@@ -157,21 +169,21 @@ inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con".
 It is easy to show that [b] is in the domain of this series, which allows us to write down the Taylor remainder around [b].
 *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b.con" as lemma.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a'.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b'.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b'.con" as lemma.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_rem.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_rem.con" as definition.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g.con" "Taylor_Defs__" as definition.
 
 (* UNEXPORTED
 Opaque Taylor_seq'_aux Taylor_rem.
@@ -197,7 +209,7 @@ Opaque funct_i'.
 Opaque funct_i.
 *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma4.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma4.con" as lemma.
 
 (* UNEXPORTED
 Transparent funct_i funct_i'.
@@ -219,15 +231,15 @@ Opaque FSumx.
 Opaque funct_i'.
 *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma5.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma5.con" as lemma.
 
 (* UNEXPORTED
 Transparent funct_i' FSumx.
 *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_aux.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_aux.con" "Taylor_Defs__" as definition.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma6.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma6.con" as lemma.
 
 (* UNEXPORTED
 Ltac Lazy_Included :=
@@ -251,9 +263,9 @@ Ltac Lazy_Eq :=
    | apply csf_wd_unfolded ]; Algebra.
 *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma7.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma7.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma8.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma8.con" as lemma.
 
 (* UNEXPORTED
 Opaque funct_aux.
@@ -263,15 +275,15 @@ Opaque funct_aux.
 Transparent funct_aux.
 *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma9.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma9.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g'.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g'.con" "Taylor_Defs__" as definition.
 
 (* UNEXPORTED
 Opaque Taylor_rem funct_aux.
 *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma10.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma10.con" as lemma.
 
 (* UNEXPORTED
 Transparent Taylor_rem funct_aux.
@@ -286,25 +298,29 @@ Now Taylor's theorem.
 %\end{convention}%
 *)
 
-alias id "e" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/e.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/e.var
+*)
 
-alias id "He" = "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/He.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/He.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma11.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma11.con" as lemma.
 
 (* end hide *)
 
 (* begin show *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/deriv_Sn'.con" "Taylor_Defs__".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/deriv_Sn'.con" "Taylor_Defs__" as definition.
 
 (* end show *)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/TLH.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/TLH.con" as lemma.
 
 (* end hide *)
 
@@ -320,7 +336,7 @@ Opaque Taylor_rem.
 Transparent Taylor_rem funct_aux.
 *)
 
-inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma.con".
+inline procedural "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma.con" as lemma.
 
 (* UNEXPORTED
 End Taylor_Defs