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 (* $Id: RefSeparated.v,v 1.8 2004/04/23 10:01:00 lcf Exp $ *)
32 Section Separating__Separated.
35 inline cic:/CoRN/ftc/RefSeparated/a.var.
37 inline cic:/CoRN/ftc/RefSeparated/b.var.
39 inline cic:/CoRN/ftc/RefSeparated/Hab.var.
41 inline cic:/CoRN/ftc/RefSeparated/I.con.
43 inline cic:/CoRN/ftc/RefSeparated/F.var.
45 inline cic:/CoRN/ftc/RefSeparated/contF.var.
47 inline cic:/CoRN/ftc/RefSeparated/incF.var.
49 inline cic:/CoRN/ftc/RefSeparated/Hab'.var.
51 inline cic:/CoRN/ftc/RefSeparated/m.var.
53 inline cic:/CoRN/ftc/RefSeparated/n.var.
55 inline cic:/CoRN/ftc/RefSeparated/P.var.
57 inline cic:/CoRN/ftc/RefSeparated/R.var.
59 inline cic:/CoRN/ftc/RefSeparated/HP.var.
61 inline cic:/CoRN/ftc/RefSeparated/HR.var.
63 inline cic:/CoRN/ftc/RefSeparated/RS_pos_n.con.
65 inline cic:/CoRN/ftc/RefSeparated/RS_pos_m.con.
67 inline cic:/CoRN/ftc/RefSeparated/alpha.var.
69 inline cic:/CoRN/ftc/RefSeparated/Halpha.var.
71 inline cic:/CoRN/ftc/RefSeparated/e.con.
73 inline cic:/CoRN/ftc/RefSeparated/RS_He.con.
75 inline cic:/CoRN/ftc/RefSeparated/contF'.con.
77 inline cic:/CoRN/ftc/RefSeparated/d.con.
79 inline cic:/CoRN/ftc/RefSeparated/RS_Hd.con.
81 inline cic:/CoRN/ftc/RefSeparated/RS_Hd'.con.
83 inline cic:/CoRN/ftc/RefSeparated/csi.var.
85 inline cic:/CoRN/ftc/RefSeparated/Hcsi.var.
87 inline cic:/CoRN/ftc/RefSeparated/M.con.
89 inline cic:/CoRN/ftc/RefSeparated/deltaP.con.
91 inline cic:/CoRN/ftc/RefSeparated/deltaR.con.
93 inline cic:/CoRN/ftc/RefSeparated/delta.con.
95 inline cic:/CoRN/ftc/RefSeparated/RS_delta_deltaP.con.
97 inline cic:/CoRN/ftc/RefSeparated/RS_delta_deltaR.con.
99 inline cic:/CoRN/ftc/RefSeparated/RS_delta_csi.con.
101 inline cic:/CoRN/ftc/RefSeparated/RS_delta_d.con.
103 inline cic:/CoRN/ftc/RefSeparated/RS_delta_pos.con.
106 Section Defining_ai'.
109 inline cic:/CoRN/ftc/RefSeparated/i.var.
111 inline cic:/CoRN/ftc/RefSeparated/Hi.var.
113 inline cic:/CoRN/ftc/RefSeparated/separation_conseq.con.
115 inline cic:/CoRN/ftc/RefSeparated/pred1.con.
117 inline cic:/CoRN/ftc/RefSeparated/pred2.con.
119 inline cic:/CoRN/ftc/RefSeparated/sep__sep_aux_lemma.con.
121 inline cic:/CoRN/ftc/RefSeparated/Hi0.var.
123 inline cic:/CoRN/ftc/RefSeparated/Hin.var.
125 inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i.con.
127 inline cic:/CoRN/ftc/RefSeparated/sep__sep_leEq.con.
129 inline cic:/CoRN/ftc/RefSeparated/sep__sep_less.con.
131 inline cic:/CoRN/ftc/RefSeparated/sep__sep_ap.con.
137 inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun.con.
139 inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_delta.con.
141 inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_delta.con.
143 inline cic:/CoRN/ftc/RefSeparated/sep__sep_mon_i.con.
145 inline cic:/CoRN/ftc/RefSeparated/sep__sep_mon.con.
147 inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_wd.con.
149 inline cic:/CoRN/ftc/RefSeparated/sep__sep_fun_wd.con.
151 inline cic:/CoRN/ftc/RefSeparated/sep__sep_part.con.
153 inline cic:/CoRN/ftc/RefSeparated/sep__sep_lemma.con.
155 inline cic:/CoRN/ftc/RefSeparated/g.var.
157 inline cic:/CoRN/ftc/RefSeparated/gP.var.
159 inline cic:/CoRN/ftc/RefSeparated/sep__sep_points.con.
161 inline cic:/CoRN/ftc/RefSeparated/sep__sep_points_lemma.con.
163 inline cic:/CoRN/ftc/RefSeparated/sep__sep_aux.con.
165 inline cic:/CoRN/ftc/RefSeparated/sep__sep_Sum.con.
167 inline cic:/CoRN/ftc/RefSeparated/sep__sep_Mesh.con.
170 End Separating__Separated.