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/RefSeparating".
21 (* $Id: RefSeparating.v,v 1.7 2004/04/23 10:01:01 lcf Exp $ *)
25 include "ftc/COrdLemmas.ma".
27 include "ftc/Partitions.ma".
30 Section Separating_Partition.
33 inline "cic:/CoRN/ftc/RefSeparating/a.var".
35 inline "cic:/CoRN/ftc/RefSeparating/b.var".
37 inline "cic:/CoRN/ftc/RefSeparating/Hab.var".
39 inline "cic:/CoRN/ftc/RefSeparating/I.con".
41 inline "cic:/CoRN/ftc/RefSeparating/F.var".
43 inline "cic:/CoRN/ftc/RefSeparating/contF.var".
45 inline "cic:/CoRN/ftc/RefSeparating/incF.var".
47 inline "cic:/CoRN/ftc/RefSeparating/Hab'.var".
49 inline "cic:/CoRN/ftc/RefSeparating/n.var".
51 inline "cic:/CoRN/ftc/RefSeparating/P.var".
53 inline "cic:/CoRN/ftc/RefSeparating/alpha.var".
55 inline "cic:/CoRN/ftc/RefSeparating/Halpha.var".
57 inline "cic:/CoRN/ftc/RefSeparating/csi.var".
59 inline "cic:/CoRN/ftc/RefSeparating/Hcsi.var".
61 inline "cic:/CoRN/ftc/RefSeparating/M.con".
63 inline "cic:/CoRN/ftc/RefSeparating/RS'_pos_n.con".
65 inline "cic:/CoRN/ftc/RefSeparating/SPap_n.con".
67 inline "cic:/CoRN/ftc/RefSeparating/delta.con".
69 inline "cic:/CoRN/ftc/RefSeparating/RS'_delta_pos.con".
71 inline "cic:/CoRN/ftc/RefSeparating/RS'_delta_csi.con".
73 inline "cic:/CoRN/ftc/RefSeparating/Hab''.var".
75 inline "cic:/CoRN/ftc/RefSeparating/sep__part_lemma.con".
77 inline "cic:/CoRN/ftc/RefSeparating/sep__part_h.con".
79 inline "cic:/CoRN/ftc/RefSeparating/sep__part_h_bnd.con".
81 inline "cic:/CoRN/ftc/RefSeparating/sep__part_h_mon_1.con".
83 inline "cic:/CoRN/ftc/RefSeparating/sep__part_h_mon_2.con".
85 inline "cic:/CoRN/ftc/RefSeparating/sep__part_h_mon_3.con".
87 inline "cic:/CoRN/ftc/RefSeparating/sep__part_app_n.con".
89 inline "cic:/CoRN/ftc/RefSeparating/sep__part_h_lemma.con".
91 inline "cic:/CoRN/ftc/RefSeparating/sep__part_h_lemma2.con".
93 inline "cic:/CoRN/ftc/RefSeparating/sep__part_h_lemma3.con".
95 inline "cic:/CoRN/ftc/RefSeparating/RS'_delta2_delta4.con".
97 inline "cic:/CoRN/ftc/RefSeparating/RS'_m1.con".
99 inline "cic:/CoRN/ftc/RefSeparating/RS'_m.con".
101 inline "cic:/CoRN/ftc/RefSeparating/sep__part_length.con".
103 inline "cic:/CoRN/ftc/RefSeparating/RS'_m_m1.con".
105 inline "cic:/CoRN/ftc/RefSeparating/RS'_pos_m.con".
107 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun.con".
109 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun_bnd.con".
111 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun_0.con".
113 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun_i.con".
115 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun_m.con".
117 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun_i'.con".
119 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun_bnd'.con".
121 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun_wd.con".
123 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun_mon.con".
125 inline "cic:/CoRN/ftc/RefSeparating/sep__part.con".
127 inline "cic:/CoRN/ftc/RefSeparating/sep__part_fun_mon_pts.con".
129 inline "cic:/CoRN/ftc/RefSeparating/sep__part_mon.con".
131 inline "cic:/CoRN/ftc/RefSeparating/sep__part_mon_Mesh.con".
133 inline "cic:/CoRN/ftc/RefSeparating/g.var".
135 inline "cic:/CoRN/ftc/RefSeparating/gP.var".
137 inline "cic:/CoRN/ftc/RefSeparating/gP'.var".
139 inline "cic:/CoRN/ftc/RefSeparating/sep__part_pts.con".
141 inline "cic:/CoRN/ftc/RefSeparating/sep__part_pts_lemma.con".
143 inline "cic:/CoRN/ftc/RefSeparating/sep__part_pts_in_Partition.con".
145 inline "cic:/CoRN/ftc/RefSeparating/RS'_Hsep_S.con".
147 inline "cic:/CoRN/ftc/RefSeparating/RS'_Hsep.con".
149 inline "cic:/CoRN/ftc/RefSeparating/RS'_h.con".
151 inline "cic:/CoRN/ftc/RefSeparating/sep__part_suRS'_m1.con".
153 inline "cic:/CoRN/ftc/RefSeparating/sep__part_Sum2.con".
155 inline "cic:/CoRN/ftc/RefSeparating/sep__part_Sum3.con".
157 inline "cic:/CoRN/ftc/RefSeparating/sep__part_Sum4.con".
159 inline "cic:/CoRN/ftc/RefSeparating/sep__part_aux.con".
161 inline "cic:/CoRN/ftc/RefSeparating/sep__part_Sum.con".
164 End Separating_Partition.