...

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/Composition.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/Composition.mma
index 2d2ebfbabbecc99b2ce9653ffc81896c399359c5..68fda7511f37ea71c0acca8785fd890975628385 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/Composition.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/Composition.mma
@@ -51,49 +51,69 @@ mapped into another compact interval.  We define this concept for
 partial functions, and prove some trivial results.
 *)
 
-alias id "F" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/G.var
+*)
 
-alias id "a" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hab.var
+*)
 
-alias id "c" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/c.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/c.var
+*)
 
-alias id "d" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/d.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/d.var
+*)
 
-alias id "Hcd" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hcd.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hcd.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/I.con" "Maps_into_Compacts__Part_Funct__".
+inline procedural "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/I.con" "Maps_into_Compacts__Part_Funct__" as definition.
 
 (* end hide *)
 
 (* begin show *)
 
-alias id "Hf" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hf.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hf.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_into_compacts.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_into_compacts.con" as definition.
 
 (* begin show *)
 
-alias id "maps" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/maps.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/maps.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_lemma'.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_lemma'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_lemma.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_less.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_less.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_inc.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_lemma_inc.con" as lemma.
 
 (* UNEXPORTED
 End Part_Funct
@@ -112,33 +132,55 @@ As was the case for division of partial functions, this condition
 completely characterizes the domain of the composite function.
 *)
 
-alias id "F" = "cic:/CoRN/ftc/Composition/Mapping/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/Composition/Mapping/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/G.var
+*)
 
-alias id "a" = "cic:/CoRN/ftc/Composition/Mapping/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/Composition/Mapping/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/Composition/Mapping/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/Hab.var
+*)
 
-alias id "c" = "cic:/CoRN/ftc/Composition/Mapping/c.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/c.var
+*)
 
-alias id "d" = "cic:/CoRN/ftc/Composition/Mapping/d.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/d.var
+*)
 
-alias id "Hcd" = "cic:/CoRN/ftc/Composition/Mapping/Hcd.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/Hcd.var
+*)
 
 (* begin show *)
 
-alias id "Hf" = "cic:/CoRN/ftc/Composition/Mapping/Hf.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/Hf.var
+*)
 
-alias id "Hg" = "cic:/CoRN/ftc/Composition/Mapping/Hg.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/Hg.var
+*)
 
-alias id "maps" = "cic:/CoRN/ftc/Composition/Mapping/maps.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Mapping/maps.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/included_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/included_comp.con" as lemma.
 
 (* UNEXPORTED
 End Mapping
@@ -153,39 +195,61 @@ Section Interval_Continuity
 We now prove that the composition of two continuous partial functions is continuous.
 *)
 
-alias id "a" = "cic:/CoRN/ftc/Composition/Interval_Continuity/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/Composition/Interval_Continuity/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/Hab.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__".
+inline procedural "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__" as definition.
 
 (* end hide *)
 
-alias id "c" = "cic:/CoRN/ftc/Composition/Interval_Continuity/c.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/c.var
+*)
 
-alias id "d" = "cic:/CoRN/ftc/Composition/Interval_Continuity/d.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/d.var
+*)
 
-alias id "Hcd" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hcd.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/Hcd.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/Composition/Interval_Continuity/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/Composition/Interval_Continuity/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/G.var
+*)
 
 (* begin show *)
 
-alias id "contF" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/contF.var
+*)
 
-alias id "contG" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/contG.var
+*)
 
-alias id "Hmap" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hmap.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Interval_Continuity/Hmap.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Continuous_I_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Continuous_I_comp.con" as lemma.
 
 (* UNEXPORTED
 End Interval_Continuity
@@ -200,57 +264,83 @@ Section Derivative
 We now work with the derivative relation and prove the chain rule for partial functions.
 *)
 
-alias id "F" = "cic:/CoRN/ftc/Composition/Derivative/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/F.var
+*)
 
-alias id "F'" = "cic:/CoRN/ftc/Composition/Derivative/F'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/F'.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/Composition/Derivative/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/G.var
+*)
 
-alias id "G'" = "cic:/CoRN/ftc/Composition/Derivative/G'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/G'.var
+*)
 
-alias id "a" = "cic:/CoRN/ftc/Composition/Derivative/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/Composition/Derivative/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/b.var
+*)
 
-alias id "Hab'" = "cic:/CoRN/ftc/Composition/Derivative/Hab'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/Hab'.var
+*)
 
-alias id "c" = "cic:/CoRN/ftc/Composition/Derivative/c.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/c.var
+*)
 
-alias id "d" = "cic:/CoRN/ftc/Composition/Derivative/d.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/d.var
+*)
 
-alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Derivative/Hcd'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/Hcd'.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hab.con" "Derivative__".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hab.con" "Derivative__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hcd.con" "Derivative__".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative/Hcd.con" "Derivative__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative/I.con" "Derivative__".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative/I.con" "Derivative__" as definition.
 
 (* end hide *)
 
 (* begin show *)
 
-alias id "derF" = "cic:/CoRN/ftc/Composition/Derivative/derF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/derF.var
+*)
 
-alias id "derG" = "cic:/CoRN/ftc/Composition/Derivative/derG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/derG.var
+*)
 
-alias id "Hmap" = "cic:/CoRN/ftc/Composition/Derivative/Hmap.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Derivative/Hmap.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/included_comp'.con".
+inline procedural "cic:/CoRN/ftc/Composition/included_comp'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/maps'.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative_I_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative_I_comp.con" as lemma.
 
 (*#*
 The next lemma will be useful when we move on to differentiability.
 *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con".
+inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con" as lemma.
 
 (* UNEXPORTED
 End Derivative
@@ -265,43 +355,65 @@ Section Differentiability
 Finally, we move on to differentiability.
 *)
 
-alias id "F" = "cic:/CoRN/ftc/Composition/Differentiability/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/Composition/Differentiability/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/G.var
+*)
 
-alias id "a" = "cic:/CoRN/ftc/Composition/Differentiability/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/Composition/Differentiability/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/b.var
+*)
 
-alias id "Hab'" = "cic:/CoRN/ftc/Composition/Differentiability/Hab'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/Hab'.var
+*)
 
-alias id "c" = "cic:/CoRN/ftc/Composition/Differentiability/c.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/c.var
+*)
 
-alias id "d" = "cic:/CoRN/ftc/Composition/Differentiability/d.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/d.var
+*)
 
-alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Differentiability/Hcd'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/Hcd'.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hab.con" "Differentiability__".
+inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hab.con" "Differentiability__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hcd.con" "Differentiability__".
+inline procedural "cic:/CoRN/ftc/Composition/Differentiability/Hcd.con" "Differentiability__" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/Differentiability/I.con" "Differentiability__".
+inline procedural "cic:/CoRN/ftc/Composition/Differentiability/I.con" "Differentiability__" as definition.
 
 (* end hide *)
 
 (* begin show *)
 
-alias id "diffF" = "cic:/CoRN/ftc/Composition/Differentiability/diffF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/diffF.var
+*)
 
-alias id "diffG" = "cic:/CoRN/ftc/Composition/Differentiability/diffG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/diffG.var
+*)
 
-alias id "Hmap" = "cic:/CoRN/ftc/Composition/Differentiability/Hmap.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Differentiability/Hmap.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Diffble_I_comp.con" as lemma.
 
 (* UNEXPORTED
 End Differentiability
@@ -319,45 +431,65 @@ We now generalize this results to arbitrary intervals.  We begin by generalizing
 %\end{convention}%
 *)
 
-alias id "I" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/I.var
+*)
 
-alias id "J" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/J.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/J.var
+*)
 
-alias id "pI" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/pI.var
+*)
 
-alias id "pJ" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pJ.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/pJ.var
+*)
 
-inline procedural "cic:/CoRN/ftc/Composition/maps_compacts_into.con".
+inline procedural "cic:/CoRN/ftc/Composition/maps_compacts_into.con" as definition.
 
 (*#*
 Now everything comes naturally:
 *)
 
-inline procedural "cic:/CoRN/ftc/Composition/comp_inc_lemma.con".
+inline procedural "cic:/CoRN/ftc/Composition/comp_inc_lemma.con" as lemma.
 
-alias id "F" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/F.var
+*)
 
-alias id "F'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/F'.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/G.var
+*)
 
-alias id "G'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/G'.var
+*)
 
 (* begin show *)
 
-alias id "Hmap" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Continuous_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Continuous_comp.con" as lemma.
 
 (* begin show *)
 
-alias id "Hmap'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap'.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Derivative_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Derivative_comp.con" as lemma.
 
 (* UNEXPORTED
 End Generalized_Intervals
@@ -371,21 +503,21 @@ Section Corollaries
 Finally, some criteria to prove that a function with a specific domain maps compacts into compacts:
 *)
 
-inline procedural "cic:/CoRN/ftc/Composition/positive_fun.con".
+inline procedural "cic:/CoRN/ftc/Composition/positive_fun.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/negative_fun.con".
+inline procedural "cic:/CoRN/ftc/Composition/negative_fun.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con".
+inline procedural "cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con".
+inline procedural "cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con".
+inline procedural "cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con" as lemma.
 
 (*#*
 As a corollary, we get the generalization of differentiability property.
 *)
 
-inline procedural "cic:/CoRN/ftc/Composition/Diffble_comp.con".
+inline procedural "cic:/CoRN/ftc/Composition/Diffble_comp.con" as lemma.
 
 (* UNEXPORTED
 End Corollaries