...

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/MoreFunctions.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/MoreFunctions.mma
index 23b99d713bfb8e112125c9be2b477df037bb598d..89c1d2e1dfe7dd9e32d32f9452b32869173d87c5 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/MoreFunctions.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/MoreFunctions.mma
@@ -42,38 +42,48 @@ arbitrary intervals.
 **Continuity
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var
+*)
 
 (*#*
 Trivial stuff.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con" as lemma.
 
 (*#*
 %\begin{convention}% Assume that [I] is compact and [F] is continuous in [I].
 %\end{convention}%
 *)
 
-alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var
+*)
 
-alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con" as lemma.
 
 (* begin show *)
 
-alias id "Hinc" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm.con" as definition.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con" as lemma.
 
 (* UNEXPORTED
 End Basic_Results
@@ -91,45 +101,55 @@ Section Other_Results
 The usual stuff.
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con" as lemma.
 
 (* begin show *)
 
-alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var
+*)
 
-alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con" as lemma.
 
 (* UNEXPORTED
 End Other_Results
@@ -149,21 +169,33 @@ Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous.
 Section Corollaries
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var
+*)
 
-alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var
+*)
 
-alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var
+*)
 
-alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con" as lemma.
 
 (* UNEXPORTED
 End Corollaries
@@ -177,22 +209,28 @@ Hint Resolve Continuous_div: continuous.
 Section Sums
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Sums/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Sums/I.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con" as lemma.
 
 (*#*
 %\begin{convention}% Assume [f] is a sequence of continuous functions.
 %\end{convention}%
 *)
 
-alias id "f" = "cic:/CoRN/ftc/MoreFunctions/Sums/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Sums/f.var
+*)
 
-alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Sums/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Sums/contF.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con" as lemma.
 
 (* UNEXPORTED
 End Sums
@@ -214,29 +252,39 @@ Derivative is not that much different.
 %\end{convention}%
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var
+*)
 
-alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var
+*)
 
-alias id "H" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con" as lemma.
 
 (* UNEXPORTED
 End Basic_Properties
@@ -255,48 +303,64 @@ Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous':
 Section More_Results
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Results/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Results/I.var
+*)
 
-alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Results/pI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Results/pI.var
+*)
 
 (*#*
 %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I].
 %\end{convention}%
 *)
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Results/F.var
+*)
 
-alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Results/G.var
+*)
 
-alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var
+*)
 
-alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var
+*)
 
-alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con" as lemma.
 
 (* UNEXPORTED
 End More_Results
@@ -306,29 +370,47 @@ End More_Results
 Section More_Corollaries
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var
+*)
 
-alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var
+*)
 
-alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var
+*)
 
-alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var
+*)
 
-alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var
+*)
 
-alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var
+*)
 
 (* begin show *)
 
-alias id "Gbnd" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con" as lemma.
 
 (* UNEXPORTED
 End More_Corollaries
@@ -338,25 +420,35 @@ End More_Corollaries
 Section More_Sums
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var
+*)
 
-alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con" as lemma.
 
 (* begin show *)
 
-alias id "f" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var
+*)
 
-alias id "f'" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var
+*)
 
-alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con" as lemma.
 
 (* UNEXPORTED
 End More_Sums
@@ -371,50 +463,62 @@ Section Diffble_Basic_Properties
 Mutatis mutandis for differentiability.
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var
+*)
 
-alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con" as lemma.
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var
+*)
 
-alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var
+*)
 
-alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var
+*)
 
 (*#*
 %\begin{convention}% Assume [F] and [G] are differentiable in [I].
 %\end{convention}%
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con" as lemma.
 
 (* UNEXPORTED
 End Diffble_Basic_Properties
@@ -428,25 +532,37 @@ Hint Immediate Diffble_imp_inc: included.
 Section Diffble_Corollaries
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var
+*)
 
-alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var
+*)
 
-alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var
+*)
 
-alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con" as lemma.
 
 (* UNEXPORTED
 End Diffble_Corollaries
@@ -461,9 +577,13 @@ Section Nth_Derivative
 Higher order derivatives pose more interesting problems.  It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval.
 *)
 
-alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var
+*)
 
-alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/pI.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/pI.var
+*)
 
 (* UNEXPORTED
 Section Definitions
@@ -474,24 +594,30 @@ Section Definitions
 %\end{convention}%
 *)
 
-alias id "n" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var
+*)
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var
+*)
 
-alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var
+*)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con" as definition.
 
 inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_char
- (* begin hide *).con".
+ (* begin hide *).con" as lemma.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con" as definition.
 
 (* UNEXPORTED
 End Definitions
@@ -505,39 +631,39 @@ Section Basic_Results
 All the usual results hold.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con" as lemma.
 
 (* UNEXPORTED
 End Basic_Results
@@ -551,21 +677,21 @@ Section More_Results
 Some new results hold, too:
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con" as lemma.
 
 (*#*
 Some useful characterization results.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con" as lemma.
 
 (* UNEXPORTED
 End More_Results
@@ -579,17 +705,21 @@ Section Derivating_Diffble
 As a special case we get a differentiation operator%\ldots%#...#
 *)
 
-alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var
+*)
 
 (* begin show *)
 
-alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var
+*)
 
 (* end show *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv.con" as definition.
 
 (* UNEXPORTED
 End Derivating_Diffble
@@ -603,19 +733,19 @@ Section Corollaries
 %\ldots%#...# for which the expected property also holds.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con" as lemma.
 
 (*#*
 Some more interesting properties.
 *)
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con" as lemma.
 
-inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con".
+inline procedural "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con" as lemma.
 
 (* UNEXPORTED
 End Corollaries