1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/RefSeparated".
19 include "CoRN_notation.ma".
21 (* $Id: RefSeparated.v,v 1.8 2004/04/23 10:01:00 lcf Exp $ *)
25 include "ftc/COrdLemmas.ma".
27 include "ftc/Partitions.ma".
30 Section Separating__Separated.
33 inline "cic:/CoRN/ftc/RefSeparated/a.var".
35 inline "cic:/CoRN/ftc/RefSeparated/b.var".
37 inline "cic:/CoRN/ftc/RefSeparated/Hab.var".
39 inline "cic:/CoRN/ftc/RefSeparated/I.con".
41 inline "cic:/CoRN/ftc/RefSeparated/F.var".
43 inline "cic:/CoRN/ftc/RefSeparated/contF.var".
45 inline "cic:/CoRN/ftc/RefSeparated/incF.var".
47 inline "cic:/CoRN/ftc/RefSeparated/Hab'.var".
49 inline "cic:/CoRN/ftc/RefSeparated/m.var".
51 inline "cic:/CoRN/ftc/RefSeparated/n.var".
53 inline "cic:/CoRN/ftc/RefSeparated/P.var".
55 inline "cic:/CoRN/ftc/RefSeparated/R.var".
57 inline "cic:/CoRN/ftc/RefSeparated/HP.var".
59 inline "cic:/CoRN/ftc/RefSeparated/HR.var".
61 inline "cic:/CoRN/ftc/RefSeparated/RS_pos_n.con".
63 inline "cic:/CoRN/ftc/RefSeparated/RS_pos_m.con".
65 inline "cic:/CoRN/ftc/RefSeparated/alpha.var".
67 inline "cic:/CoRN/ftc/RefSeparated/Halpha.var".
69 inline "cic:/CoRN/ftc/RefSeparated/e.con".
71 inline "cic:/CoRN/ftc/RefSeparated/RS_He.con".
73 inline "cic:/CoRN/ftc/RefSeparated/contF'.con".
75 inline "cic:/CoRN/ftc/RefSeparated/d.con".
77 inline "cic:/CoRN/ftc/RefSeparated/RS_Hd.con".
79 inline "cic:/CoRN/ftc/RefSeparated/RS_Hd'.con".
81 inline "cic:/CoRN/ftc/RefSeparated/csi.var".
83 inline "cic:/CoRN/ftc/RefSeparated/Hcsi.var".
85 inline "cic:/CoRN/ftc/RefSeparated/M.con".
87 inline "cic:/CoRN/ftc/RefSeparated/deltaP.con".
89 inline "cic:/CoRN/ftc/RefSeparated/deltaR.con".
91 inline "cic:/CoRN/ftc/RefSeparated/delta.con".
93 inline "cic:/CoRN/ftc/RefSeparated/RS_delta_deltaP.con".
95 inline "cic:/CoRN/ftc/RefSeparated/RS_delta_deltaR.con".
97 inline "cic:/CoRN/ftc/RefSeparated/RS_delta_csi.con".
99 inline "cic:/CoRN/ftc/RefSeparated/RS_delta_d.con".
101 inline "cic:/CoRN/ftc/RefSeparated/RS_delta_pos.con".
104 Section Defining_ai'.
107 inline "cic:/CoRN/ftc/RefSeparated/i.var".
109 inline "cic:/CoRN/ftc/RefSeparated/Hi.var".
111 inline "cic:/CoRN/ftc/RefSeparated/separation_conseq.con".
113 inline "cic:/CoRN/ftc/RefSeparated/pred1.con".
115 inline "cic:/CoRN/ftc/RefSeparated/pred2.con".
117 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_aux_lemma.con".
119 inline "cic:/CoRN/ftc/RefSeparated/Hi0.var".
121 inline "cic:/CoRN/ftc/RefSeparated/Hin.var".
123 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i.con".
125 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_leEq.con".
127 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_less.con".
129 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_ap.con".
135 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun.con".
137 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_delta.con".
139 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_delta.con".
141 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_mon_i.con".
143 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_mon.con".
145 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_wd.con".
147 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_wd.con".
149 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_part.con".
151 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_lemma.con".
153 inline "cic:/CoRN/ftc/RefSeparated/g.var".
155 inline "cic:/CoRN/ftc/RefSeparated/gP.var".
157 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_points.con".
159 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_points_lemma.con".
161 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_aux.con".
163 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Sum.con".
165 inline "cic:/CoRN/ftc/RefSeparated/sep__sep_Mesh.con".
168 End Separating__Separated.