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

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

diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma
index 5d764a8828e0e1d6415466df0a7f7f394f61ede3..6e373299c3ca4e02b7a0d8c9df9fd4e9a625dde1 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FTC.ma
@@ -31,7 +31,7 @@ Opaque Min.
 *)
 
 (* UNEXPORTED
-Section Indefinite_Integral.
+Section Indefinite_Integral
 *)
 
 (*#* *The Fundamental Theorem of Calculus
@@ -51,15 +51,15 @@ and [a] be a point in [I].
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/FTC/I.var".
+inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var" "Indefinite_Integral__".
 
-inline "cic:/CoRN/ftc/FTC/F.var".
+inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var" "Indefinite_Integral__".
 
-inline "cic:/CoRN/ftc/FTC/contF.var".
+inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var" "Indefinite_Integral__".
 
-inline "cic:/CoRN/ftc/FTC/a.var".
+inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var" "Indefinite_Integral__".
 
-inline "cic:/CoRN/ftc/FTC/Ha.var".
+inline "cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var" "Indefinite_Integral__".
 
 inline "cic:/CoRN/ftc/FTC/prim_lemma.con".
 
@@ -68,7 +68,7 @@ inline "cic:/CoRN/ftc/FTC/Fprim_strext.con".
 inline "cic:/CoRN/ftc/FTC/Fprim.con".
 
 (* UNEXPORTED
-End Indefinite_Integral.
+End Indefinite_Integral
 *)
 
 (* UNEXPORTED
@@ -80,7 +80,7 @@ Notation "[-S-] F" := (Fprim F) (at level 20).
 *)
 
 (* UNEXPORTED
-Section FTC.
+Section FTC
 *)
 
 (*#* **The FTC
@@ -94,19 +94,19 @@ indefinite integral of [F] from [x0].
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/FTC/J.var".
+inline "cic:/CoRN/ftc/FTC/FTC/J.var" "FTC__".
 
-inline "cic:/CoRN/ftc/FTC/F.var".
+inline "cic:/CoRN/ftc/FTC/FTC/F.var" "FTC__".
 
-inline "cic:/CoRN/ftc/FTC/contF.var".
+inline "cic:/CoRN/ftc/FTC/FTC/contF.var" "FTC__".
 
-inline "cic:/CoRN/ftc/FTC/x0.var".
+inline "cic:/CoRN/ftc/FTC/FTC/x0.var" "FTC__".
 
-inline "cic:/CoRN/ftc/FTC/Hx0.var".
+inline "cic:/CoRN/ftc/FTC/FTC/Hx0.var" "FTC__".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/FTC/G.con".
+inline "cic:/CoRN/ftc/FTC/FTC/G.con" "FTC__".
 
 (* end hide *)
 
@@ -116,7 +116,7 @@ inline "cic:/CoRN/ftc/FTC/Continuous_prim.con".
 The derivative of [G] is simply [F].
 *)
 
-inline "cic:/CoRN/ftc/FTC/pJ.var".
+inline "cic:/CoRN/ftc/FTC/FTC/pJ.var" "FTC__".
 
 inline "cic:/CoRN/ftc/FTC/FTC1.con".
 
@@ -124,9 +124,9 @@ inline "cic:/CoRN/ftc/FTC/FTC1.con".
 Any other function [G0] with derivative [F] must differ from [G] by a constant.
 *)
 
-inline "cic:/CoRN/ftc/FTC/G0.var".
+inline "cic:/CoRN/ftc/FTC/FTC/G0.var" "FTC__".
 
-inline "cic:/CoRN/ftc/FTC/derG0.var".
+inline "cic:/CoRN/ftc/FTC/FTC/derG0.var" "FTC__".
 
 inline "cic:/CoRN/ftc/FTC/FTC2.con".
 
@@ -136,7 +136,7 @@ The following is another statement of the Fundamental Theorem of Calculus, also
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/FTC/G0_inc.con".
+inline "cic:/CoRN/ftc/FTC/FTC/G0_inc.con" "FTC__".
 
 (* end hide *)
 
@@ -149,7 +149,7 @@ inline "cic:/CoRN/ftc/FTC/Barrow.con".
 (* end hide *)
 
 (* UNEXPORTED
-End FTC.
+End FTC
 *)
 
 (* UNEXPORTED
@@ -161,7 +161,7 @@ Hint Resolve FTC1: derivate.
 *)
 
 (* UNEXPORTED
-Section Limit_of_Integral_Seq.
+Section Limit_of_Integral_Seq
 *)
 
 (*#* **Corollaries
@@ -180,18 +180,18 @@ then the sequence of their primitives also converges, and the limit
 commutes with the indefinite integral.
 *)
 
-inline "cic:/CoRN/ftc/FTC/J.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var" "Limit_of_Integral_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/f.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var" "Limit_of_Integral_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/F.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var" "Limit_of_Integral_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/contf.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var" "Limit_of_Integral_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/contF.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contF.var" "Limit_of_Integral_Seq__".
 
 (* UNEXPORTED
-Section Compact.
+Section Compact
 *)
 
 (*#*
@@ -204,48 +204,48 @@ continuous in [[a,b]], $x0\in[a,b]$#x0∈[a,b]#; denote by
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/FTC/a.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var" "Limit_of_Integral_Seq__Compact__".
 
-inline "cic:/CoRN/ftc/FTC/b.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var" "Limit_of_Integral_Seq__Compact__".
 
-inline "cic:/CoRN/ftc/FTC/Hab.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var" "Limit_of_Integral_Seq__Compact__".
 
-inline "cic:/CoRN/ftc/FTC/contIf.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var" "Limit_of_Integral_Seq__Compact__".
 
-inline "cic:/CoRN/ftc/FTC/contIF.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var" "Limit_of_Integral_Seq__Compact__".
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/FTC/convF.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var" "Limit_of_Integral_Seq__Compact__".
 
 (* end show *)
 
-inline "cic:/CoRN/ftc/FTC/x0.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var" "Limit_of_Integral_Seq__Compact__".
 
-inline "cic:/CoRN/ftc/FTC/Hx0.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var" "Limit_of_Integral_Seq__Compact__".
 
-inline "cic:/CoRN/ftc/FTC/Hx0'.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var" "Limit_of_Integral_Seq__Compact__".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/FTC/g.con".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/g.con" "Limit_of_Integral_Seq__Compact__".
 
-inline "cic:/CoRN/ftc/FTC/G.con".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/G.con" "Limit_of_Integral_Seq__Compact__".
 
 (* end hide *)
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/FTC/contg.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var" "Limit_of_Integral_Seq__Compact__".
 
-inline "cic:/CoRN/ftc/FTC/contG.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var" "Limit_of_Integral_Seq__Compact__".
 
 (* end show *)
 
 inline "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con".
 
 (* UNEXPORTED
-End Compact.
+End Compact
 *)
 
 (*#*
@@ -257,7 +257,7 @@ inline "cic:/CoRN/ftc/FTC/limit_of_integral.con".
 inline "cic:/CoRN/ftc/FTC/limit_of_Integral.con".
 
 (* UNEXPORTED
-Section General.
+Section General
 *)
 
 (*#*
@@ -266,38 +266,38 @@ Finally, with [x0, g, G] as before,
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/FTC/convF.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var" "Limit_of_Integral_Seq__General__".
 
 (* end show *)
 
-inline "cic:/CoRN/ftc/FTC/x0.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var" "Limit_of_Integral_Seq__General__".
 
-inline "cic:/CoRN/ftc/FTC/Hx0.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var" "Limit_of_Integral_Seq__General__".
 
 (* begin hide *)
 
-inline "cic:/CoRN/ftc/FTC/g.con".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/g.con" "Limit_of_Integral_Seq__General__".
 
-inline "cic:/CoRN/ftc/FTC/G.con".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/G.con" "Limit_of_Integral_Seq__General__".
 
 (* end hide *)
 
-inline "cic:/CoRN/ftc/FTC/contg.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var" "Limit_of_Integral_Seq__General__".
 
-inline "cic:/CoRN/ftc/FTC/contG.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var" "Limit_of_Integral_Seq__General__".
 
 inline "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con".
 
 (* UNEXPORTED
-End General.
+End General
 *)
 
 (* UNEXPORTED
-End Limit_of_Integral_Seq.
+End Limit_of_Integral_Seq
 *)
 
 (* UNEXPORTED
-Section Limit_of_Derivative_Seq.
+Section Limit_of_Derivative_Seq
 *)
 
 (*#*
@@ -307,67 +307,67 @@ Similar results hold for the sequence of derivatives of a converging sequence; t
 %\end{convention}%
 *)
 
-inline "cic:/CoRN/ftc/FTC/J.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/pJ.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/f.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/g.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/F.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/G.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/contf.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/contF.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/convF.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/contg.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/contG.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/convG.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var" "Limit_of_Derivative_Seq__".
 
-inline "cic:/CoRN/ftc/FTC/derf.var".
+inline "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var" "Limit_of_Derivative_Seq__".
 
 inline "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con".
 
 (* UNEXPORTED
-End Limit_of_Derivative_Seq.
+End Limit_of_Derivative_Seq
 *)
 
 (* UNEXPORTED
-Section Derivative_Series.
+Section Derivative_Series
 *)
 
 (*#*
 As a very important case of this result, we get a rule for deriving series.
 *)
 
-inline "cic:/CoRN/ftc/FTC/J.var".
+inline "cic:/CoRN/ftc/FTC/Derivative_Series/J.var" "Derivative_Series__".
 
-inline "cic:/CoRN/ftc/FTC/pJ.var".
+inline "cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var" "Derivative_Series__".
 
-inline "cic:/CoRN/ftc/FTC/f.var".
+inline "cic:/CoRN/ftc/FTC/Derivative_Series/f.var" "Derivative_Series__".
 
-inline "cic:/CoRN/ftc/FTC/g.var".
+inline "cic:/CoRN/ftc/FTC/Derivative_Series/g.var" "Derivative_Series__".
 
 (* begin show *)
 
-inline "cic:/CoRN/ftc/FTC/convF.var".
+inline "cic:/CoRN/ftc/FTC/Derivative_Series/convF.var" "Derivative_Series__".
 
-inline "cic:/CoRN/ftc/FTC/convG.var".
+inline "cic:/CoRN/ftc/FTC/Derivative_Series/convG.var" "Derivative_Series__".
 
 (* end show *)
 
-inline "cic:/CoRN/ftc/FTC/derF.var".
+inline "cic:/CoRN/ftc/FTC/Derivative_Series/derF.var" "Derivative_Series__".
 
 inline "cic:/CoRN/ftc/FTC/Derivative_FSeries.con".
 
 (* UNEXPORTED
-End Derivative_Series.
+End Derivative_Series
 *)