...

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/FTC.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/FTC.mma
index 9412847b9e27df798d2bf551312c10fe9648ce68..b7381ac7691ef135486ba2925d8a9f97bf30ed4e 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/FTC.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/FTC.mma
@@ -49,21 +49,31 @@ and [a] be a point in [I].
 %\end{convention}%
 *)
 
-alias id "I" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Indefinite_Integral/I.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Indefinite_Integral/F.var
+*)
 
-alias id "contF" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Indefinite_Integral/contF.var
+*)
 
-alias id "a" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Indefinite_Integral/a.var
+*)
 
-alias id "Ha" = "cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Indefinite_Integral/Ha.var
+*)
 
-inline procedural "cic:/CoRN/ftc/FTC/prim_lemma.con".
+inline procedural "cic:/CoRN/ftc/FTC/prim_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/FTC/Fprim_strext.con".
+inline procedural "cic:/CoRN/ftc/FTC/Fprim_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/FTC/Fprim.con".
+inline procedural "cic:/CoRN/ftc/FTC/Fprim.con" as definition.
 
 (* UNEXPORTED
 End Indefinite_Integral
@@ -92,41 +102,57 @@ indefinite integral of [F] from [x0].
 %\end{convention}%
 *)
 
-alias id "J" = "cic:/CoRN/ftc/FTC/FTC/J.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/FTC/J.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/FTC/FTC/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/FTC/F.var
+*)
 
-alias id "contF" = "cic:/CoRN/ftc/FTC/FTC/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/FTC/contF.var
+*)
 
-alias id "x0" = "cic:/CoRN/ftc/FTC/FTC/x0.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/FTC/x0.var
+*)
 
-alias id "Hx0" = "cic:/CoRN/ftc/FTC/FTC/Hx0.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/FTC/Hx0.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/FTC/FTC/G.con" "FTC__".
+inline procedural "cic:/CoRN/ftc/FTC/FTC/G.con" "FTC__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/FTC/Continuous_prim.con".
+inline procedural "cic:/CoRN/ftc/FTC/Continuous_prim.con" as lemma.
 
 (*#*
 The derivative of [G] is simply [F].
 *)
 
-alias id "pJ" = "cic:/CoRN/ftc/FTC/FTC/pJ.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/FTC/pJ.var
+*)
 
-inline procedural "cic:/CoRN/ftc/FTC/FTC1.con".
+inline procedural "cic:/CoRN/ftc/FTC/FTC1.con" as theorem.
 
 (*#*
 Any other function [G0] with derivative [F] must differ from [G] by a constant.
 *)
 
-alias id "G0" = "cic:/CoRN/ftc/FTC/FTC/G0.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/FTC/G0.var
+*)
 
-alias id "derG0" = "cic:/CoRN/ftc/FTC/FTC/derG0.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/FTC/derG0.var
+*)
 
-inline procedural "cic:/CoRN/ftc/FTC/FTC2.con".
+inline procedural "cic:/CoRN/ftc/FTC/FTC2.con" as theorem.
 
 (*#*
 The following is another statement of the Fundamental Theorem of Calculus, also known as Barrow's rule.
@@ -134,7 +160,7 @@ The following is another statement of the Fundamental Theorem of Calculus, also
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/FTC/FTC/G0_inc.con" "FTC__".
+inline procedural "cic:/CoRN/ftc/FTC/FTC/G0_inc.con" "FTC__" as definition.
 
 (* end hide *)
 
@@ -142,7 +168,7 @@ inline procedural "cic:/CoRN/ftc/FTC/FTC/G0_inc.con" "FTC__".
 Opaque G.
 *)
 
-inline procedural "cic:/CoRN/ftc/FTC/Barrow.con".
+inline procedural "cic:/CoRN/ftc/FTC/Barrow.con" as theorem.
 
 (* end hide *)
 
@@ -178,15 +204,25 @@ then the sequence of their primitives also converges, and the limit
 commutes with the indefinite integral.
 *)
 
-alias id "J" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/J.var
+*)
 
-alias id "f" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/f.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/F.var
+*)
 
-alias id "contf" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contf.var
+*)
 
-alias id "contF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/contF.var
+*)
 
 (* UNEXPORTED
 Section Compact
@@ -202,45 +238,67 @@ continuous in [[a,b]], $x0\in[a,b]$#x0∈[a,b]#; denote by
 %\end{convention}%
 *)
 
-alias id "a" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hab.var
+*)
 
-alias id "contIf" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIf.var
+*)
 
-alias id "contIF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contIF.var
+*)
 
 (* begin show *)
 
-alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/convF.var
+*)
 
 (* end show *)
 
-alias id "x0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/x0.var
+*)
 
-alias id "Hx0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0.var
+*)
 
-alias id "Hx0'" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/Hx0'.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/g.con" "Limit_of_Integral_Seq__Compact__".
+inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/g.con" "Limit_of_Integral_Seq__Compact__" as definition.
 
-inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/G.con" "Limit_of_Integral_Seq__Compact__".
+inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/G.con" "Limit_of_Integral_Seq__Compact__" as definition.
 
 (* end hide *)
 
 (* begin show *)
 
-alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contg.var
+*)
 
-alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/Compact/contG.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con".
+inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral.con" as lemma.
 
 (* UNEXPORTED
 End Compact
@@ -250,9 +308,9 @@ End Compact
 And now we can generalize it step by step.
 *)
 
-inline procedural "cic:/CoRN/ftc/FTC/limit_of_integral.con".
+inline procedural "cic:/CoRN/ftc/FTC/limit_of_integral.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/FTC/limit_of_Integral.con".
+inline procedural "cic:/CoRN/ftc/FTC/limit_of_Integral.con" as lemma.
 
 (* UNEXPORTED
 Section General
@@ -264,27 +322,37 @@ Finally, with [x0, g, G] as before,
 
 (* begin show *)
 
-alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/convF.var
+*)
 
 (* end show *)
 
-alias id "x0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/x0.var
+*)
 
-alias id "Hx0" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/Hx0.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/g.con" "Limit_of_Integral_Seq__General__".
+inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/g.con" "Limit_of_Integral_Seq__General__" as definition.
 
-inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/G.con" "Limit_of_Integral_Seq__General__".
+inline procedural "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/G.con" "Limit_of_Integral_Seq__General__" as definition.
 
 (* end hide *)
 
-alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contg.var
+*)
 
-alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Integral_Seq/General/contG.var
+*)
 
-inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con".
+inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_integral_IR.con" as lemma.
 
 (* UNEXPORTED
 End General
@@ -305,33 +373,59 @@ Similar results hold for the sequence of derivatives of a converging sequence; t
 %\end{convention}%
 *)
 
-alias id "J" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/J.var
+*)
 
-alias id "pJ" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/pJ.var
+*)
 
-alias id "f" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/f.var
+*)
 
-alias id "g" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/g.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/G.var
+*)
 
-alias id "contf" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contf.var
+*)
 
-alias id "contF" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contF.var
+*)
 
-alias id "convF" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convF.var
+*)
 
-alias id "contg" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contg.var
+*)
 
-alias id "contG" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/contG.var
+*)
 
-alias id "convG" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/convG.var
+*)
 
-alias id "derf" = "cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Limit_of_Derivative_Seq/derf.var
+*)
 
-inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con".
+inline procedural "cic:/CoRN/ftc/FTC/fun_lim_seq_derivative.con" as lemma.
 
 (* UNEXPORTED
 End Limit_of_Derivative_Seq
@@ -345,25 +439,39 @@ Section Derivative_Series
 As a very important case of this result, we get a rule for deriving series.
 *)
 
-alias id "J" = "cic:/CoRN/ftc/FTC/Derivative_Series/J.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Derivative_Series/J.var
+*)
 
-alias id "pJ" = "cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Derivative_Series/pJ.var
+*)
 
-alias id "f" = "cic:/CoRN/ftc/FTC/Derivative_Series/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Derivative_Series/f.var
+*)
 
-alias id "g" = "cic:/CoRN/ftc/FTC/Derivative_Series/g.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Derivative_Series/g.var
+*)
 
 (* begin show *)
 
-alias id "convF" = "cic:/CoRN/ftc/FTC/Derivative_Series/convF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Derivative_Series/convF.var
+*)
 
-alias id "convG" = "cic:/CoRN/ftc/FTC/Derivative_Series/convG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Derivative_Series/convG.var
+*)
 
 (* end show *)
 
-alias id "derF" = "cic:/CoRN/ftc/FTC/Derivative_Series/derF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/FTC/Derivative_Series/derF.var
+*)
 
-inline procedural "cic:/CoRN/ftc/FTC/Derivative_FSeries.con".
+inline procedural "cic:/CoRN/ftc/FTC/Derivative_FSeries.con" as lemma.
 
 (* UNEXPORTED
 End Derivative_Series