...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / fta / FTAreg.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/fta/FTAreg.mma b/helm/software/matita/contribs/CoRN-Procedural/fta/FTAreg.mma
index 58c776f63445af06cf2b67c0a66fb0c0f7718bfc..8c6d3cbc9352c756fc775b809122230af85afb7b 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/fta/FTAreg.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/fta/FTAreg.mma
@@ -34,9 +34,13 @@ include "fta/CPoly_Contin1.ma".
 Section Seq_Exists
 *)
 
-alias id "n" = "cic:/CoRN/fta/FTAreg/Seq_Exists/n.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/n.var
+*)
 
-alias id "lt0n" = "cic:/CoRN/fta/FTAreg/Seq_Exists/lt0n.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/lt0n.var
+*)
 
 (*#*
 %\begin{convention}% Let [qK] be a real between 0 and 1, with
@@ -53,21 +57,37 @@ Let [p] be a monic polynomial over the complex numbers with degree
 Section Kneser_Sequence
 *)
 
-alias id "qK" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qK.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qK.var
+*)
 
-alias id "zltq" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/zltq.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/zltq.var
+*)
 
-alias id "qlt1" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qlt1.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qlt1.var
+*)
 
-alias id "q_prop" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/q_prop.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/q_prop.var
+*)
 
-alias id "p" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p.var
+*)
 
-alias id "mp" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/mp.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/mp.var
+*)
 
-alias id "c0" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/c0.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/c0.var
+*)
 
-alias id "p0ltc0" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p0ltc0.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p0ltc0.var
+*)
 
 inline procedural "cic:/CoRN/fta/FTAreg/Knes_tup.ind".
 
@@ -81,21 +101,21 @@ inline procedural "cic:/CoRN/fta/FTAreg/Knes_tupp.ind".
 cic:/matita/CoRN-Procedural/fta/FTAreg/Kntup.con
 *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun.con".
+inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun.con" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun_it.con".
+inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun_it.con" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK.con" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_c.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_c.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_c0.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_c0.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_prop1.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_prop1.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_it.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_it.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/sK_prop2.con".
+inline procedural "cic:/CoRN/fta/FTAreg/sK_prop2.con" as lemma.
 
 (* UNEXPORTED
 End Kneser_Sequence
@@ -108,7 +128,7 @@ Section Seq_Exists_Main
 (*#* **Main results
 *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/seq_exists.con".
+inline procedural "cic:/CoRN/fta/FTAreg/seq_exists.con" as lemma.
 
 (* UNEXPORTED
 End Seq_Exists_Main
@@ -122,31 +142,49 @@ End Seq_Exists
 Section N_Exists
 *)
 
-alias id "n" = "cic:/CoRN/fta/FTAreg/N_Exists/n.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/N_Exists/n.var
+*)
 
-alias id "lt0n" = "cic:/CoRN/fta/FTAreg/N_Exists/lt0n.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/N_Exists/lt0n.var
+*)
 
-alias id "q" = "cic:/CoRN/fta/FTAreg/N_Exists/q.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/N_Exists/q.var
+*)
 
-alias id "zleq" = "cic:/CoRN/fta/FTAreg/N_Exists/zleq.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/N_Exists/zleq.var
+*)
 
-alias id "qlt1" = "cic:/CoRN/fta/FTAreg/N_Exists/qlt1.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/N_Exists/qlt1.var
+*)
 
-alias id "c" = "cic:/CoRN/fta/FTAreg/N_Exists/c.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/N_Exists/c.var
+*)
 
-alias id "zltc" = "cic:/CoRN/fta/FTAreg/N_Exists/zltc.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/N_Exists/zltc.var
+*)
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/N_Exists/q_.con" "N_Exists__".
+inline procedural "cic:/CoRN/fta/FTAreg/N_Exists/q_.con" "N_Exists__" as definition.
 
 (* end hide *)
 
-alias id "e" = "cic:/CoRN/fta/FTAreg/N_Exists/e.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/N_Exists/e.var
+*)
 
-alias id "zlte" = "cic:/CoRN/fta/FTAreg/N_Exists/zlte.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/N_Exists/zlte.var
+*)
 
-inline procedural "cic:/CoRN/fta/FTAreg/N_exists.con".
+inline procedural "cic:/CoRN/fta/FTAreg/N_exists.con" as lemma.
 
 (* UNEXPORTED
 End N_Exists
@@ -158,19 +196,33 @@ Section Seq_is_CC_CAuchy
 
 (*#* ** The Kneser sequence is Cauchy in [CC] *)
 
-alias id "n" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/n.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/n.var
+*)
 
-alias id "lt0n" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/lt0n.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/lt0n.var
+*)
 
-alias id "q" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q.var
+*)
 
-alias id "zleq" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zleq.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zleq.var
+*)
 
-alias id "qlt1" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/qlt1.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/qlt1.var
+*)
 
-alias id "c" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/c.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/c.var
+*)
 
-alias id "zltc" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zltc.var".
+(* UNEXPORTED
+cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zltc.var
+*)
 
 (*#* %\begin{convention}% Let:
  - [q_] prove [q[-]One [#] Zero]
@@ -183,39 +235,39 @@ alias id "zltc" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zltc.var".
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q_.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q_.con" "Seq_is_CC_CAuchy__" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq.con" "Seq_is_CC_CAuchy__" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtc.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtc.con" "Seq_is_CC_CAuchy__" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtqlt1.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtqlt1.con" "Seq_is_CC_CAuchy__" as definition.
 
-inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq_.con" "Seq_is_CC_CAuchy__".
+inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq_.con" "Seq_is_CC_CAuchy__" as definition.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtq.con".
+inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtq.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtc.con".
+inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtc.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/nrt_pow.con".
+inline procedural "cic:/CoRN/fta/FTAreg/nrt_pow.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltRe.con".
+inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltRe.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltIm.con".
+inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltIm.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/SublemmaRe.con".
+inline procedural "cic:/CoRN/fta/FTAreg/SublemmaRe.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/SublemmaIm.con".
+inline procedural "cic:/CoRN/fta/FTAreg/SublemmaIm.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/seq_is_CC_Cauchy.con".
+inline procedural "cic:/CoRN/fta/FTAreg/seq_is_CC_Cauchy.con" as lemma.
 
 (* UNEXPORTED
 End Seq_is_CC_CAuchy
 *)
 
-inline procedural "cic:/CoRN/fta/FTAreg/FTA_monic.con".
+inline procedural "cic:/CoRN/fta/FTAreg/FTA_monic.con" as lemma.
 
-inline procedural "cic:/CoRN/fta/FTAreg/FTA_reg.con".
+inline procedural "cic:/CoRN/fta/FTAreg/FTA_reg.con" as lemma.