Changeset 3494
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3493 r3494 1014 1014 #EQ >(rewrite_in_dependent_map … EQ) % 1015 1015 ] 1016 >(rewrite_in_dependent_map ??? [])1017 [ whd in ⊢ (???% → ?); #EQ destruct whd >act_neutral >act_neutral1018 lapply (instr_map_ok … good … prf …)1019 1016 1020 1017 >rewrite_in_dependent_map [2: @eq_f [2: @eq_f2 [3: % 4: @get_cost_label_append *:] *:] 3:] … … 1089 1086 ⊢ (??%% → ?); 1090 1087 1091 * #H3 #H4 1092 1093 st1 st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H 1088 #st * #st3 * #t1 * #l * #prf * #ABS cases(tbase_tind_append … ABS) ] 1089 cases st st [3: #x] * #H #_ whd in ⊢ (??%% → ?); @eqb_elim [2: * #ABS @⊥ @ABS %] 1090 #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin_a1 1091 #labels whd in ⊢ (???% → ?); #EQ destruct >act_neutral >act_neutral assumption 1092  st1 st2 * [3: #st1] * [3,6,9: #st2] #st3 #l whd in ⊢ (% → ?); * 1093 [ #no_final #Hstep #tl #IH whd in ⊢ (% → ?); 1094 (* 1095 #EQlabels 1096 #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta 1097 [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st 1098 normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1099 #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption 1100  ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta 1101 #H cases(bind_inversion ????? H) H * 1102 [ #seq * [#lbl1] 1103  #newpc 1104  #cond #newpc #ltrue #lfalse 1105  #lin #io #lout 1106  #f 1107  1108 ] 1109 * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate; 1110 normalize nodelta >EQfetch >m_return_bind normalize nodelta 1111 cases(asm_is_io ??) normalize nodelta 1112 [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct 1113 2,4,8,9,12,14: #H cases(bind_inversion ????? H) H #x * #_ 1114 [3: cases x normalize nodelta 1115 6: #H cases(bind_inversion ????? H) H #y * #_ 1116 ] 1117 ] 1118 whd in ⊢ (??%% → ?); #EQ destruct 1119 [4,8: cases H1 [1,3: * *: * #y #EQ destruct]] 1120 >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct 1121 #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r 1122 >act_neutral 1123 @(instr_map_ok … good … EQfetch … good_st_a1) /2/ 1124 ]*) 1125  st1 st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H 1094 1126 #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????); 1095 1127 whd #costs >dependent_map_append
Note: See TracChangeset
for help on using the changeset viewer.