Changeset 3494 for LTS


Ignore:
Timestamp:
Sep 25, 2014, 1:43:33 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3493 r3494  
    10141014    #EQ >(rewrite_in_dependent_map … EQ) %
    10151015  ]
    1016     >(rewrite_in_dependent_map ??? [])
    1017     [ whd in ⊢ (???% → ?); #EQ destruct whd >act_neutral >act_neutral
    1018       lapply (instr_map_ok … good … prf …)
    10191016   
    10201017    >rewrite_in_dependent_map [2: @eq_f [2: @eq_f2 [3: % |4: @get_cost_label_append |*:] |*:] |3:]
     
    10891086         ⊢ (??%% → ?);
    10901087
    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
    10941126  #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
    10951127  whd #costs >dependent_map_append
Note: See TracChangeset for help on using the changeset viewer.