Changeset 3494

Timestamp:

Sep 25, 2014, 1:43:33 PM (5 years ago)

Author:

piccolo

Message:

 

File:

• LTS/Vm.ma (modified) (2 diffs)

LTS/Vm.ma

@@ -1014 +1014 @@
     #EQ >(rewrite_in_dependent_map … EQ) %
   ]
-    >(rewrite_in_dependent_map ??? [])
-    [ whd in ⊢ (???% → ?); #EQ destruct whd >act_neutral >act_neutral
-      lapply (instr_map_ok … good … prf …)
     
     >rewrite_in_dependent_map [2: @eq_f [2: @eq_f2 [3: % |4: @get_cost_label_append |*:] |*:] |3:]
@@ -1089 +1086 @@
          ⊢ (??%% → ?);
 
- * #H3 #H4
-
-  -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
+ #st * #st3 * #t1 * #l * #prf * #ABS cases(tbase_tind_append … ABS) ] 
+  cases st -st [3: #x] * #H #_ whd in ⊢ (??%% → ?); @eqb_elim [2: * #ABS @⊥ @ABS %]
+   #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin_a1
+   #labels whd in ⊢ (???% → ?); #EQ destruct >act_neutral >act_neutral assumption
+| -st1 -st2 * [3: #st1] * [3,6,9: #st2] #st3 #l whd in ⊢ (% → ?); *
+  [ #no_final #Hstep #tl #IH whd in ⊢ (% → ?);
+   (*
+    #EQlabels
+  #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
+  [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
+    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
+    #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption 
+  | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta
+    #H cases(bind_inversion ????? H) -H *
+    [ #seq * [|#lbl1]
+    | #newpc
+    | #cond #newpc #ltrue #lfalse
+    | #lin #io #lout
+    | #f
+    |
+    ] 
+    * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
+    normalize nodelta >EQfetch >m_return_bind normalize nodelta
+    cases(asm_is_io ??) normalize nodelta 
+    [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
+    |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
+      [3: cases x normalize nodelta
+      |6: #H cases(bind_inversion ????? H) -H #y * #_
+      ]
+    ]
+    whd in ⊢ (??%% → ?); #EQ destruct 
+    [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
+    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
+    #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r
+    >act_neutral
+    @(instr_map_ok … good … EQfetch … good_st_a1) /2/
+  ]*)
+| -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
   #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
   whd #costs >dependent_map_append