]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/ftc/RefSeparating.mma
ground_2 released and permanently renamed as ground
[helm.git] / helm / software / matita / contribs / procedural / CoRN / ftc / RefSeparating.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "CoRN.ma".
18
19 (* $Id: RefSeparating.v,v 1.7 2004/04/23 10:01:01 lcf Exp $ *)
20
21 (* begin hide *)
22
23 include "ftc/COrdLemmas.ma".
24
25 include "ftc/Partitions.ma".
26
27 (* UNEXPORTED
28 Section Separating_Partition
29 *)
30
31 (* UNEXPORTED
32 cic:/CoRN/ftc/RefSeparating/Separating_Partition/a.var
33 *)
34
35 (* UNEXPORTED
36 cic:/CoRN/ftc/RefSeparating/Separating_Partition/b.var
37 *)
38
39 (* UNEXPORTED
40 cic:/CoRN/ftc/RefSeparating/Separating_Partition/Hab.var
41 *)
42
43 inline procedural "cic:/CoRN/ftc/RefSeparating/Separating_Partition/I.con" "Separating_Partition__" as definition.
44
45 (* UNEXPORTED
46 cic:/CoRN/ftc/RefSeparating/Separating_Partition/F.var
47 *)
48
49 (* UNEXPORTED
50 cic:/CoRN/ftc/RefSeparating/Separating_Partition/contF.var
51 *)
52
53 (* UNEXPORTED
54 cic:/CoRN/ftc/RefSeparating/Separating_Partition/incF.var
55 *)
56
57 (* UNEXPORTED
58 cic:/CoRN/ftc/RefSeparating/Separating_Partition/Hab'.var
59 *)
60
61 (* UNEXPORTED
62 cic:/CoRN/ftc/RefSeparating/Separating_Partition/n.var
63 *)
64
65 (* UNEXPORTED
66 cic:/CoRN/ftc/RefSeparating/Separating_Partition/P.var
67 *)
68
69 (* UNEXPORTED
70 cic:/CoRN/ftc/RefSeparating/Separating_Partition/alpha.var
71 *)
72
73 (* UNEXPORTED
74 cic:/CoRN/ftc/RefSeparating/Separating_Partition/Halpha.var
75 *)
76
77 (* UNEXPORTED
78 cic:/CoRN/ftc/RefSeparating/Separating_Partition/csi.var
79 *)
80
81 (* UNEXPORTED
82 cic:/CoRN/ftc/RefSeparating/Separating_Partition/Hcsi.var
83 *)
84
85 inline procedural "cic:/CoRN/ftc/RefSeparating/Separating_Partition/M.con" "Separating_Partition__" as definition.
86
87 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_pos_n.con" as lemma.
88
89 inline procedural "cic:/CoRN/ftc/RefSeparating/SPap_n.con" as lemma.
90
91 inline procedural "cic:/CoRN/ftc/RefSeparating/Separating_Partition/delta.con" "Separating_Partition__" as definition.
92
93 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_delta_pos.con" as lemma.
94
95 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_delta_csi.con" as lemma.
96
97 (* UNEXPORTED
98 cic:/CoRN/ftc/RefSeparating/Separating_Partition/Hab''.var
99 *)
100
101 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_lemma.con" as lemma.
102
103 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_h.con" as definition.
104
105 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_h_bnd.con" as lemma.
106
107 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_h_mon_1.con" as lemma.
108
109 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_h_mon_2.con" as lemma.
110
111 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_h_mon_3.con" as lemma.
112
113 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_app_n.con" as lemma.
114
115 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_h_lemma.con" as lemma.
116
117 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_h_lemma2.con" as lemma.
118
119 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_h_lemma3.con" as lemma.
120
121 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_delta2_delta4.con" as lemma.
122
123 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_m1.con" as definition.
124
125 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_m.con" as definition.
126
127 (* NOTATION
128 Notation m := RS'_m.
129 *)
130
131 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_length.con" as definition.
132
133 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_m_m1.con" as lemma.
134
135 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_pos_m.con" as lemma.
136
137 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun.con" as definition.
138
139 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun_bnd.con" as lemma.
140
141 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun_0.con" as lemma.
142
143 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun_i.con" as lemma.
144
145 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun_m.con" as lemma.
146
147 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun_i'.con" as lemma.
148
149 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun_bnd'.con" as lemma.
150
151 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun_wd.con" as lemma.
152
153 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun_mon.con" as lemma.
154
155 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part.con" as definition.
156
157 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_fun_mon_pts.con" as lemma.
158
159 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_mon.con" as lemma.
160
161 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_mon_Mesh.con" as lemma.
162
163 (* UNEXPORTED
164 cic:/CoRN/ftc/RefSeparating/Separating_Partition/g.var
165 *)
166
167 (* UNEXPORTED
168 cic:/CoRN/ftc/RefSeparating/Separating_Partition/gP.var
169 *)
170
171 (* UNEXPORTED
172 cic:/CoRN/ftc/RefSeparating/Separating_Partition/gP'.var
173 *)
174
175 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_pts.con" as definition.
176
177 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_pts_lemma.con" as lemma.
178
179 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_pts_in_Partition.con" as lemma.
180
181 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_Hsep_S.con" as lemma.
182
183 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_Hsep.con" as lemma.
184
185 inline procedural "cic:/CoRN/ftc/RefSeparating/RS'_h.con" as definition.
186
187 (* NOTATION
188 Notation h := RS'_h.
189 *)
190
191 (* NOTATION
192 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
193 *)
194
195 (* NOTATION
196 Notation just2 :=
197   (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)).
198 *)
199
200 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_suRS'_m1.con" as lemma.
201
202 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_Sum2.con" as lemma.
203
204 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_Sum3.con" as lemma.
205
206 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_Sum4.con" as lemma.
207
208 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_aux.con" as lemma.
209
210 inline procedural "cic:/CoRN/ftc/RefSeparating/sep__part_Sum.con" as lemma.
211
212 (* UNEXPORTED
213 End Separating_Partition
214 *)
215
216 (* end hide *)
217