- new library/logic/coimplication.ma uses new decompose tactic

[helm.git] / helm / software / matita / contribs / CoRN-Decl / ftc / TaylorLemma.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma
index 0fc55435693aa1bf35bf4473bf809ce3efd82d03..29affb739515d7d80cd8e5b025bb50021df82984 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma
@@ -16,18 +16,18 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/ftc/TaylorLemma".
 
+include "CoRN.ma".
+
 (* $Id: TaylorLemma.v,v 1.8 2004/04/23 10:01:01 lcf Exp $ *)
 
-(* INCLUDE
-Rolle
-*)
+include "ftc/Rolle.ma".
 
 (* UNEXPORTED
 Opaque Min.
 *)
 
 (* UNEXPORTED
-Section Taylor_Defs.
+Section Taylor_Defs
 *)
 
 (*#* *Taylor's Theorem
@@ -44,31 +44,31 @@ define the nth order derivative of [F] in the interval
 [[Min(a,b),Max(a,b)]].
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/a.var.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/a.var" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/b.var.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/b.var" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/Hap.var.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hap.var" "Taylor_Defs__".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Hab'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab'.con" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/Hab.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hab.con" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/I.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/I.con" "Taylor_Defs__".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/F.var.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/F.var" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/Ha.var.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Ha.var" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/Hb.var.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Hb.var" "Taylor_Defs__".
 
 (* begin show *)
 
-inline cic:/CoRN/ftc/TaylorLemma/fi.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/fi.con" "Taylor_Defs__".
 
 (* end show *)
 
@@ -79,7 +79,7 @@ $f_i=f^{(i)}$#f<sub>i</sub>=f<sup>(i)</sup>#.
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma1.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma1.con".
 
 (* end hide *)
 
@@ -94,41 +94,49 @@ corresponding to [a] and [b].
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_compact_a.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_a.con" "Taylor_Defs__".
+
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/TL_compact_b.con" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_compact_b.con.
+(* NOTATION
+Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
+*)
+
+(* NOTATION
+Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
+*)
 
 (* end hide *)
 
 (* begin show *)
 
-inline cic:/CoRN/ftc/TaylorLemma/funct_i.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i.con" "Taylor_Defs__".
 
 (* end show *)
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/funct_i'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_i'.con" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_a_i.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_a_i.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_b_i.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_b_i.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_x_i.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_x_i.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_a_i'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_a_i'.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_b_i'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_b_i'.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_x_i'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_x_i'.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma2'.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma3'.con".
 
 (* end hide *)
 
@@ -137,13 +145,13 @@ Adding the previous expressions up to a given bound [n] gives us the
 Taylor sum of order [n].
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_seq'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_seq'.con".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_seq'_aux.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/Taylor_seq'_aux.con" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a.con".
 
 (* end hide *)
 
@@ -151,21 +159,21 @@ inline 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 cic:/CoRN/ftc/TaylorLemma/TL_lemma_b.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b.con".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_lemma_a'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_a'.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/TL_lemma_b'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TL_lemma_b'.con".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_rem.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_rem.con".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/g.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g.con" "Taylor_Defs__".
 
 (* UNEXPORTED
 Opaque Taylor_seq'_aux Taylor_rem.
@@ -191,7 +199,7 @@ Opaque funct_i'.
 Opaque funct_i.
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma4.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma4.con".
 
 (* UNEXPORTED
 Transparent funct_i funct_i'.
@@ -213,15 +221,15 @@ Opaque FSumx.
 Opaque funct_i'.
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma5.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma5.con".
 
 (* UNEXPORTED
 Transparent funct_i' FSumx.
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/funct_aux.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/funct_aux.con" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma6.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma6.con".
 
 (* UNEXPORTED
 Ltac Lazy_Included :=
@@ -245,9 +253,9 @@ Ltac Lazy_Eq :=
    | apply csf_wd_unfolded ]; Algebra.
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma7.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma7.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma8.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma8.con".
 
 (* UNEXPORTED
 Opaque funct_aux.
@@ -257,15 +265,15 @@ Opaque funct_aux.
 Transparent funct_aux.
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma9.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma9.con".
 
-inline cic:/CoRN/ftc/TaylorLemma/g'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/g'.con" "Taylor_Defs__".
 
 (* UNEXPORTED
 Opaque Taylor_rem funct_aux.
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma10.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma10.con".
 
 (* UNEXPORTED
 Transparent Taylor_rem funct_aux.
@@ -280,25 +288,25 @@ Now Taylor's theorem.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/e.var.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/e.var" "Taylor_Defs__".
 
-inline cic:/CoRN/ftc/TaylorLemma/He.var.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/He.var" "Taylor_Defs__".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma11.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma11.con".
 
 (* end hide *)
 
 (* begin show *)
 
-inline cic:/CoRN/ftc/TaylorLemma/deriv_Sn'.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_Defs/deriv_Sn'.con" "Taylor_Defs__".
 
 (* end show *)
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/TaylorLemma/TLH.con.
+inline "cic:/CoRN/ftc/TaylorLemma/TLH.con".
 
 (* end hide *)
 
@@ -314,9 +322,9 @@ Opaque Taylor_rem.
 Transparent Taylor_rem funct_aux.
 *)
 
-inline cic:/CoRN/ftc/TaylorLemma/Taylor_lemma.con.
+inline "cic:/CoRN/ftc/TaylorLemma/Taylor_lemma.con".
 
 (* UNEXPORTED
-End Taylor_Defs.
+End Taylor_Defs
 *)