From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 31 Oct 2008 16:30:33 +0000 (+0000)
Subject: Environment simplified.
X-Git-Tag: make_still_working~4610
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=db1552c8344acc3de1f0596d999170046eb0c8fa;p=helm.git

Environment simplified.
---

diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
index 9f489b792..d8805d269 100755
--- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
+++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
@@ -384,10 +384,10 @@ definition env_to_flatEnv_inv ≝
  λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
   ∀str.
    check_desc_env d e str →
-   (((check_env_map_align d e d map)⊗(check_map_env_align d e map)) = true ∧
+    check_env_map_align d e d map = true ∧ check_map_env_align d e map = true ∧
     check_id_map d map str ∧
     check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
-    get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
+    get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
 
 lemma inv_to_checkdescflatenv :
  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
@@ -527,10 +527,20 @@ let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_ty
   ].
 
 (* avanzamento dell'invariante *)
-axiom env_map_flatEnv_enter_aux : 
+lemma env_map_flatEnv_enter_aux : 
  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
   env_to_flatEnv_inv d e map fe →
   env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
+ unfold env_to_flatEnv_inv;
+ intros;
+ split; [ split [ split [ split | ] | ] | ]
+  [ elim daemon
+  | elim daemon;
+  | elim daemon;
+  | elim daemon;
+  | elim daemon;
+  ]
+qed.
 
 axiom env_map_flatEnv_add_aux : 
  ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.