helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma

   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 (* ********************************************************************** *)
  16 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "compiler/environment.ma".
  23
  24 (* ********************** *)
  25 (* GESTIONE AMBIENTE FLAT *)
  26 (* ********************** *)
  27
  28 (* ambiente flat *)
  29 inductive var_flatElem : Type ≝
  30 VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem.
  31
  32 definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
  33 definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
  34
  35 definition aux_flatEnv_type ≝ list var_flatElem.
  36
  37 definition empty_flatEnv ≝ nil var_flatElem.
  38
  39 (* mappa: nome + max + cur *)
  40 inductive n_list : nat → Type ≝
  41   n_nil: n_list O
  42 | n_cons: ∀n.option nat → n_list n → n_list (S n).
  43
  44 definition defined_nList ≝
  45 λd.λl:n_list d.match l with [ n_nil ⇒ False | n_cons _ _ _ ⇒ True ].
  46
  47 definition cut_first_nList : Πd.n_list d → ? → n_list (pred d) ≝
  48 λd.λl:n_list d.λp:defined_nList ? l.
  49  let value ≝
  50   match l
  51    return λX.λY:n_list X.defined_nList X Y → n_list (pred X)
  52   with
  53    [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p
  54    | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).t
  55    ] p in value.
  56
  57 definition get_first_nList : Πd.n_list d → ? → option nat ≝
  58 λd.λl:n_list d.λp:defined_nList ? l.
  59  let value ≝
  60   match l
  61    return λX.λY:n_list X.defined_nList X Y → option nat
  62   with
  63    [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p
  64    | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).h
  65    ] p in value.
  66
  67 inductive map_elem (d:nat) : Type ≝
  68 MAP_ELEM: aux_str_type → nat → n_list (S d) → map_elem d.
  69
  70 definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ].
  71 definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ].
  72 definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ].
  73
  74 definition aux_map_type ≝ λd.list (map_elem d).
  75
  76 definition empty_map ≝ nil (map_elem O).
  77
  78 axiom defined_nList_S_to_true :
  79 ∀d.∀l:n_list (S d).defined_nList (S d) l = True.
  80
  81 lemma defined_get_id :
  82  ∀d.∀h:map_elem d.True → defined_nList (S d) (get_cur_mapElem d h).
  83  intros 3;
  84  rewrite > (defined_nList_S_to_true ? (get_cur_mapElem d h));
  85  apply H.
  86 qed.
  87
  88 (* get_id *)
  89 let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
  90  match map with
  91   [ nil ⇒ None ?
  92   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
  93                 [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ?? I)
  94                 | false ⇒ get_id_map_aux d t name
  95                 ]
  96   ].
  97
  98 definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
  99  match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
 100
 101 (* get_max *)
 102 let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
 103  match map with
 104   [ nil ⇒ None ?
 105   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
 106                 [ true ⇒ Some ? (get_max_mapElem d h)
 107                 | false ⇒ get_max_map_aux d t name
 108                 ]
 109   ].
 110
 111 definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 112  match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
 113
 114 (* check_id *)
 115 definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 116  match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ].
 117
 118 definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 119  match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
 120
 121 lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name.
 122  unfold checkb_id_map;
 123  unfold check_id_map;
 124  intros 3;
 125  elim (get_id_map_aux d map name) 0;
 126  [ simplify; intro; destruct H
 127  | simplify; intros; apply I
 128  ].
 129 qed.
 130
 131 definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 132  match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ].
 133
 134 definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
 135  match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ].
 136
 137 lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name.
 138  unfold checknotb_id_map;
 139  unfold checknot_id_map;
 140  intros 3;
 141  elim (get_id_map_aux d map name) 0;
 142  [ simplify; intro; apply I
 143  | simplify; intros; destruct H
 144  ].
 145 qed.
 146
 147 (* get_desc *)
 148 let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
 149  match fe with
 150   [ nil ⇒ None ?
 151   | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with
 152                [ true ⇒ Some ? (get_desc_flatVar h)
 153                | false ⇒ get_desc_flatEnv_aux t name
 154                ]
 155   ].
 156
 157 definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 158  match get_desc_flatEnv_aux fe str with
 159   [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
 160
 161 definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 162  match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ].
 163
 164 definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 165  match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ].
 166
 167 lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
 168  unfold checkb_desc_flatEnv;
 169  unfold check_desc_flatEnv;
 170  intros 2;
 171  elim (get_desc_flatEnv_aux fe str) 0;
 172  [ simplify; intro; destruct H
 173  | simplify; intros; apply I
 174  ].
 175 qed.
 176
 177 definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 178  match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ].
 179
 180 definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
 181  match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ].
 182
 183 lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
 184  unfold checknotb_desc_flatEnv;
 185  unfold checknot_desc_flatEnv;
 186  intros 2;
 187  elim (get_desc_flatEnv_aux fe str) 0;
 188  [ simplify; intro; apply I
 189  | simplify; intros; destruct H
 190  ].
 191 qed.
 192
 193 (* fe <= fe' *)
 194 definition eq_flatEnv_elem ≝
 195 λe1,e2.match e1 with
 196  [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
 197   [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
 198
 199 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
 200  intros 3;
 201  rewrite < H;
 202  elim e1;
 203  simplify;
 204  rewrite > (eq_to_eqstrid a a (refl_eq ??));
 205  rewrite > (eq_to_eqdescelem d d (refl_eq ??));
 206  reflexivity.
 207 qed.
 208
 209 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
 210  intros 2;
 211  elim e1 0;
 212  elim e2 0;
 213  intros 4;
 214  simplify;
 215  intro;
 216  rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
 217  rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
 218  reflexivity.
 219 qed.
 220
 221 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
 222 match fe with
 223   [ nil ⇒ true
 224   | cons h tl ⇒ match fe' with
 225    [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
 226   ].
 227
 228 lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
 229  intros 3;
 230  rewrite < H;
 231  elim e1;
 232  [ reflexivity
 233  | simplify;
 234    rewrite > (eq_to_eqflatenv a a (refl_eq ??));
 235    rewrite > H1;
 236    reflexivity
 237  ].
 238 qed.
 239
 240 lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
 241  intro;
 242  elim fe 0;
 243  [ intros; exists; [ apply fe' | reflexivity ]
 244  | intros 4; elim fe';
 245    [ simplify in H1:(%); destruct H1
 246    | simplify in H2:(%);
 247      rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
 248      cases (H l1 (andb_true_true_r ?? H2));
 249      simplify;
 250      rewrite < H3;
 251      exists; [ apply x | reflexivity ]
 252    ]
 253  ].
 254 qed.
 255
 256 lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
 257  intros;
 258  elim fe;
 259  [ simplify;
 260    reflexivity
 261  | simplify;
 262    rewrite > (eq_to_eqflatenv a a (refl_eq ??));
 263    rewrite > H;
 264    reflexivity
 265  ].
 266 qed.
 267
 268 lemma leflatenv_to_check : ∀fe,fe',str.
 269  (le_flatEnv fe fe' = true) →
 270  (check_desc_flatEnv fe str) →
 271  (check_desc_flatEnv fe' str).
 272  intros 4;
 273  cases (leflatEnv_to_le fe fe' H);
 274  rewrite < H1;
 275  elim fe 0;
 276  [ intro; simplify in H2:(%); elim H2;
 277  | intros 3;
 278    simplify;
 279    cases (eqStrId_str str (get_name_flatVar a));
 280    [ simplify; intro; apply H3
 281    | simplify; apply H2
 282    ]
 283  ].
 284 qed.
 285
 286 lemma leflatenv_to_get : ∀fe,fe',str.
 287  (le_flatEnv fe fe' = true) →
 288  (check_desc_flatEnv fe str) →
 289  (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
 290  intros 4;
 291  cases (leflatEnv_to_le fe fe' H);
 292  rewrite < H1;
 293  elim fe 0;
 294  [ intro;
 295    simplify in H2:(%);
 296    elim H2
 297  | simplify;
 298    intros 2;
 299    cases (eqStrId_str str (get_name_flatVar a));
 300    [ simplify;
 301      intros;
 302      reflexivity
 303    | simplify;
 304      unfold check_desc_flatEnv;
 305      unfold get_desc_flatEnv;
 306      cases (get_desc_flatEnv_aux l str);
 307      [ simplify; intros; elim H3
 308      | simplify; intros; rewrite < (H2 H3); reflexivity
 309      ]
 310    ]
 311  ].
 312 qed.
 313
 314 (* invariante *)
 315 definition env_to_flatEnv_inv ≝
 316  λd.λe:aux_env_type.λmap:aux_map_type d.λfe:aux_flatEnv_type.
 317   ∀str.
 318    check_desc_env e str →
 319    (check_id_map d map str ∧
 320     check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
 321     get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
 322
 323 lemma inv_to_checkdescflatenv :
 324  ∀d.∀e.∀map:aux_map_type d.∀fe.
 325  env_to_flatEnv_inv d e map fe →
 326  (∀str.check_desc_env e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
 327  intros 7;
 328  unfold env_to_flatEnv_inv in H:(%);
 329  lapply (H str H1);
 330  apply (proj2 ?? (proj1 ?? Hletin));
 331 qed.
 332
 333 lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
 334  unfold env_to_flatEnv_inv;
 335  unfold empty_env;
 336  unfold empty_map;
 337  unfold empty_flatEnv;
 338  simplify;
 339  intros;
 340  split;
 341  [ split; apply H | reflexivity ].
 342 qed.
 343
 344 lemma leflatenv_to_inv :
 345  ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
 346   le_flatEnv fe fe' = true →
 347   env_to_flatEnv_inv d e map fe →
 348   env_to_flatEnv_inv d e map fe'.
 349  intros 6;
 350  unfold env_to_flatEnv_inv;
 351  intros;
 352  split;
 353  [ split;
 354    [ lapply (H1 str H2);
 355      apply (proj1 ?? (proj1 ?? Hletin))
 356    | lapply (H1 str H2);
 357      apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
 358    ]
 359  | lapply (H1 str H2);
 360    rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
 361    apply (proj2 ?? Hletin)
 362  ].
 363 qed.
 364
 365 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
 366 let rec enter_map d (map:aux_map_type d) on map ≝
 367  match map with
 368   [ nil ⇒ []
 369   | cons h t ⇒
 370    (MAP_ELEM (S d)
 371              (get_name_mapElem d h)
 372              (get_max_mapElem d h)
 373              (n_cons (S d)
 374                      (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ?? I))
 375                      (get_cur_mapElem d h))
 376    )::(enter_map d t)
 377   ].
 378
 379 lemma getidmap_to_enter :
 380  ∀d.∀m:aux_map_type d.∀str.
 381   get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
 382  intros;
 383  elim m;
 384  [ simplify; reflexivity
 385  | simplify; rewrite > H; reflexivity
 386  ]
 387 qed.
 388
 389 lemma env_map_flatEnv_enter_aux :
 390  ∀d.∀e.∀map:aux_map_type d.∀fe.
 391   env_to_flatEnv_inv d e map fe → env_to_flatEnv_inv (S d) (enter_env e) (enter_map d map) fe.
 392  intros 3;
 393  unfold enter_env;
 394  unfold empty_env;
 395  unfold env_to_flatEnv_inv;
 396  simplify;
 397  elim e 0;
 398  [ elim map 0;
 399    [ simplify; intros; split;
 400      [ apply (proj1 ?? (H str H1)) | apply (proj2 ?? (H str H1)); ]
 401    | simplify; intros; split;
 402      [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H1 str H2))
 403      | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H1 str H2))
 404      ]
 405    ]
 406  | elim map 0;
 407    [ simplify; intros; split;
 408      [ apply (proj1 ?? (H1 str H2)) | apply (proj2 ?? (H1 str H2)) ]
 409    | simplify; intros; split;
 410      [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H2 str H3))
 411      | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H2 str H3))
 412      ]
 413    ]
 414  ].
 415 qed.
 416
 417 (* leave: elimina la testa (il "cur" corrente) *)
 418 let rec leave_map d (map:aux_map_type (S d)) on map ≝
 419  match map with
 420   [ nil ⇒ []
 421   | cons h t ⇒
 422    (MAP_ELEM d
 423              (get_name_mapElem (S d) h)
 424              (get_max_mapElem (S d) h)
 425              (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ?? I))
 426    )::(leave_map d t)
 427   ].
 428
 429 (* aggiungi descrittore *)
 430 let rec new_map_elem_from_depth_aux (d:nat) on d ≝
 431  match d
 432   return λd.n_list d
 433  with
 434   [ O ⇒ n_nil
 435   | S n ⇒ n_cons n (None ?) (new_map_elem_from_depth_aux n)
 436   ].
 437
 438 let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
 439  match map with
 440   [ nil ⇒ []
 441   | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
 442                 [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ?? I)))
 443                 | false ⇒ h
 444                 ]::(new_max_map_aux d t name max)
 445   ].
 446
 447 definition add_desc_env_flatEnv_map ≝
 448 λd.λmap:aux_map_type d.λstr.
 449  match get_max_map_aux d map str with
 450   [ None ⇒ map@[ MAP_ELEM d str O (n_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
 451   | Some x ⇒ new_max_map_aux d map str (S x)
 452   ].
 453
 454 definition add_desc_env_flatEnv_fe ≝
 455 λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
 456  fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
 457                     (DESC_ELEM c desc) ].
 458
 459 let rec build_trasfEnv_env (trsf:list (Prod3T aux_str_type bool ast_type)) e on trsf ≝
 460  match trsf with
 461   [ nil ⇒ e
 462   | cons h t ⇒ build_trasfEnv_env t (add_desc_env e (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))
 463   ].
 464
 465 let rec build_trasfEnv_mapFe (trasf:list ?) d (mfe:Prod (aux_map_type d) aux_flatEnv_type) on trasf ≝
 466  match trasf with
 467   [ nil ⇒ mfe
 468   | cons h t ⇒
 469    build_trasfEnv_mapFe t d (pair ?? (add_desc_env_flatEnv_map d (fst ?? mfe) (fst3T ??? h))
 470                                      (add_desc_env_flatEnv_fe d (fst ?? mfe) (snd ?? mfe) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
 471   ].
 472
 473 (* avanzamento delle dimostrazioni *)
 474 axiom env_map_flatEnv_add_aux :
 475  ∀d.∀e.∀map:aux_map_type d.∀fe.∀trsf.
 476   env_to_flatEnv_inv d e map fe →
 477   env_to_flatEnv_inv d
 478                      (build_trasfEnv_env trsf e)
 479                      (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe)))
 480                      (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))).
 481
 482 axiom env_map_flatEnv_add_aux_fe :
 483  ∀d.∀map:aux_map_type d.∀fe,trsf.
 484   ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))).
 485
 486 lemma buildtrasfenvadd_to_le :
 487  ∀d.∀m:aux_map_type d.∀fe,trsf.
 488   le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true.
 489  intros 4;
 490   cases (env_map_flatEnv_add_aux_fe d m fe trsf);
 491  rewrite < H;
 492  rewrite > (le_to_leflatenv fe x);
 493  reflexivity.
 494 qed.
 495
 496 axiom env_map_flatEnv_leave_aux :
 497  ∀d.∀e.∀map:aux_map_type (S d).∀fe.
 498   env_to_flatEnv_inv (S d) e map fe →
 499   env_to_flatEnv_inv d
 500                      (leave_env e)
 501                      (leave_map d map)
 502                      fe.
 503
 504 (* avanzamento congiunto oggetti + dimostrazioni *)
 505 inductive env_map_flatEnv :
 506      Πd.Πe.Πm:aux_map_type d.Πfe,fe'.
 507      env_to_flatEnv_inv d e m fe' →
 508      le_flatEnv fe fe' = true → Type ≝
 509   ENV_MAP_FLATENV_EMPTY: env_map_flatEnv O
 510                                          empty_env
 511                                          empty_map
 512                                          empty_flatEnv
 513                                          empty_flatEnv
 514                                          env_map_flatEnv_empty_aux
 515                                          (eq_to_leflatenv ?? (refl_eq ??))
 516 | ENV_MAP_FLATENV_ENTER: ∀d,e.∀m:aux_map_type d.∀fe,fe'.
 517                       ∀dimInv:env_to_flatEnv_inv d e m fe'.
 518                       ∀dimLe:le_flatEnv fe fe' = true.
 519                          env_map_flatEnv d e m fe fe' dimInv dimLe →
 520                          env_map_flatEnv (S d)
 521                                          (enter_env e)
 522                                          (enter_map d m)
 523                                          fe'
 524                                          fe'
 525                                          (env_map_flatEnv_enter_aux d e m fe' dimInv)
 526                                          (eq_to_leflatenv ?? (refl_eq ??))
 527 | ENV_MAP_FLATENV_ADD: ∀d,e.∀m:aux_map_type d.∀fe,fe'.
 528                     ∀dimInv:env_to_flatEnv_inv d e m fe'.
 529                     ∀dimLe:le_flatEnv fe fe' = true.∀trsf.
 530                        env_map_flatEnv d e m fe fe' dimInv dimLe →
 531                        env_map_flatEnv d
 532                                        (build_trasfEnv_env trsf e)
 533                                        (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe')))
 534                                        fe'
 535                                        (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe')))
 536                                        (env_map_flatEnv_add_aux d e m fe' trsf dimInv)
 537                                        (buildtrasfenvadd_to_le d m fe' trsf)
 538 | ENV_MAP_FLATENV_LEAVE: ∀d,e.∀m:aux_map_type (S d).∀fe,fe'.
 539                       ∀dimInv:env_to_flatEnv_inv (S d) e m fe'.
 540                       ∀dimLe:le_flatEnv fe fe' = true.
 541                          env_map_flatEnv (S d) e m fe fe' dimInv dimLe →
 542                          env_map_flatEnv d
 543                                          (leave_env e)
 544                                          (leave_map d m)
 545                                          fe'
 546                                          fe'
 547                                          (env_map_flatEnv_leave_aux d e m fe' dimInv)
 548                                          (eq_to_leflatenv ?? (refl_eq ??)).