helm/software/matita/contribs/procedural/CoRN/ftc/RefSeparated.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: RefSeparated.v,v 1.8 2004/04/23 10:01:00 lcf Exp $ *)
  20
  21 (* begin hide *)
  22
  23 include "ftc/COrdLemmas.ma".
  24
  25 include "ftc/Partitions.ma".
  26
  27 (* UNEXPORTED
  28 Section Separating__Separated
  29 *)
  30
  31 (* UNEXPORTED
  32 cic:/CoRN/ftc/RefSeparated/Separating__Separated/a.var
  33 *)
  34
  35 (* UNEXPORTED
  36 cic:/CoRN/ftc/RefSeparated/Separating__Separated/b.var
  37 *)
  38
  39 (* UNEXPORTED
  40 cic:/CoRN/ftc/RefSeparated/Separating__Separated/Hab.var
  41 *)
  42
  43 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/I.con" "Separating__Separated__" as definition.
  44
  45 (* UNEXPORTED
  46 cic:/CoRN/ftc/RefSeparated/Separating__Separated/F.var
  47 *)
  48
  49 (* UNEXPORTED
  50 cic:/CoRN/ftc/RefSeparated/Separating__Separated/contF.var
  51 *)
  52
  53 (* UNEXPORTED
  54 cic:/CoRN/ftc/RefSeparated/Separating__Separated/incF.var
  55 *)
  56
  57 (* UNEXPORTED
  58 cic:/CoRN/ftc/RefSeparated/Separating__Separated/Hab'.var
  59 *)
  60
  61 (* UNEXPORTED
  62 cic:/CoRN/ftc/RefSeparated/Separating__Separated/m.var
  63 *)
  64
  65 (* UNEXPORTED
  66 cic:/CoRN/ftc/RefSeparated/Separating__Separated/n.var
  67 *)
  68
  69 (* UNEXPORTED
  70 cic:/CoRN/ftc/RefSeparated/Separating__Separated/P.var
  71 *)
  72
  73 (* UNEXPORTED
  74 cic:/CoRN/ftc/RefSeparated/Separating__Separated/R.var
  75 *)
  76
  77 (* UNEXPORTED
  78 cic:/CoRN/ftc/RefSeparated/Separating__Separated/HP.var
  79 *)
  80
  81 (* UNEXPORTED
  82 cic:/CoRN/ftc/RefSeparated/Separating__Separated/HR.var
  83 *)
  84
  85 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_pos_n.con" as lemma.
  86
  87 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_pos_m.con" as lemma.
  88
  89 (* UNEXPORTED
  90 cic:/CoRN/ftc/RefSeparated/Separating__Separated/alpha.var
  91 *)
  92
  93 (* UNEXPORTED
  94 cic:/CoRN/ftc/RefSeparated/Separating__Separated/Halpha.var
  95 *)
  96
  97 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/e.con" "Separating__Separated__" as definition.
  98
  99 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_He.con" as lemma.
 100
 101 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/contF'.con" "Separating__Separated__" as definition.
 102
 103 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/d.con" "Separating__Separated__" as definition.
 104
 105 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_Hd.con" as lemma.
 106
 107 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_Hd'.con" as lemma.
 108
 109 (* UNEXPORTED
 110 cic:/CoRN/ftc/RefSeparated/Separating__Separated/csi.var
 111 *)
 112
 113 (* UNEXPORTED
 114 cic:/CoRN/ftc/RefSeparated/Separating__Separated/Hcsi.var
 115 *)
 116
 117 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/M.con" "Separating__Separated__" as definition.
 118
 119 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/deltaP.con" "Separating__Separated__" as definition.
 120
 121 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/deltaR.con" "Separating__Separated__" as definition.
 122
 123 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/delta.con" "Separating__Separated__" as definition.
 124
 125 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_delta_deltaP.con" as lemma.
 126
 127 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_delta_deltaR.con" as lemma.
 128
 129 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_delta_csi.con" as lemma.
 130
 131 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_delta_d.con" as lemma.
 132
 133 inline procedural "cic:/CoRN/ftc/RefSeparated/RS_delta_pos.con" as lemma.
 134
 135 (* UNEXPORTED
 136 Section Defining_ai'
 137 *)
 138
 139 (* UNEXPORTED
 140 cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/i.var
 141 *)
 142
 143 (* UNEXPORTED
 144 cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/Hi.var
 145 *)
 146
 147 inline procedural "cic:/CoRN/ftc/RefSeparated/separation_conseq.con" as lemma.
 148
 149 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/pred1.con" "Separating__Separated__Defining_ai'__" as definition.
 150
 151 inline procedural "cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/pred2.con" "Separating__Separated__Defining_ai'__" as definition.
 152
 153 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_aux_lemma.con" as lemma.
 154
 155 (* UNEXPORTED
 156 cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/Hi0.var
 157 *)
 158
 159 (* UNEXPORTED
 160 cic:/CoRN/ftc/RefSeparated/Separating__Separated/Defining_ai'/Hin.var
 161 *)
 162
 163 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i.con" as definition.
 164
 165 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_leEq.con" as lemma.
 166
 167 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_less.con" as lemma.
 168
 169 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_ap.con" as lemma.
 170
 171 (* UNEXPORTED
 172 End Defining_ai'
 173 *)
 174
 175 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_fun.con" as definition.
 176
 177 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_delta.con" as lemma.
 178
 179 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_delta.con" as lemma.
 180
 181 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_mon_i.con" as lemma.
 182
 183 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_mon.con" as lemma.
 184
 185 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_i_wd.con" as lemma.
 186
 187 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_fun_wd.con" as lemma.
 188
 189 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_part.con" as definition.
 190
 191 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_lemma.con" as lemma.
 192
 193 (* UNEXPORTED
 194 cic:/CoRN/ftc/RefSeparated/Separating__Separated/g.var
 195 *)
 196
 197 (* UNEXPORTED
 198 cic:/CoRN/ftc/RefSeparated/Separating__Separated/gP.var
 199 *)
 200
 201 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_points.con" as definition.
 202
 203 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_points_lemma.con" as lemma.
 204
 205 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_aux.con" as lemma.
 206
 207 (* NOTATION
 208 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
 209 *)
 210
 211 (* NOTATION
 212 Notation just2 :=
 213   (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)).
 214 *)
 215
 216 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_Sum.con" as lemma.
 217
 218 inline procedural "cic:/CoRN/ftc/RefSeparated/sep__sep_Mesh.con" as lemma.
 219
 220 (* UNEXPORTED
 221 End Separating__Separated
 222 *)
 223
 224 (* end hide *)
 225