Changeset 3492
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3491 r3492 891 891  @eqb_elim normalize nodelta 892 892 [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels 893 >(rewrite_in_dependent_map ??? []) 894 [ whd in ⊢ (???% → ?); #EQ destruct whd >act_neutral >act_neutral 895 lapply (instr_map_ok … good … prf …) 893 896 894 >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append ] 895 >rewrite_in_dependent_map [2: 896 @chop_append_singleton 897 whd in ⊢ (??%% → ?); whd in match (dependent_map ????); 898 899 >(act_neutral … a1) in H; 900 901 902 #H #H1 903 cases st2 in prf; st2 [3: #st2] #prf 904 lapply(instr_map_ok … good … prf … rel_fin) 905 906 lapply prf * 907 #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct 908 >act_neutral >act_neutral @(instr_map_ok … good … rel_fin) 909 910 911 @opt_safe_elim #k_init 912 #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct 913 >act_neutral whd in match (big_op ??); >act_op >act_neutral 914 915 916 #H >act_neutral whd in prf; 917 918 cases l in prf H1 H2; 919 [1,4: #f #lbl 2,5: * [2,4: #lbl] *: * [2,4: #lbl] ] #prf 920 ** [normalize in ⊢ (% → ?); 921 ⊢ (??%% → ?); 922 923 #st * #st3 * #t1 * #l * #prf * #ABS cases(tbase_tind_append … ABS) ] 924 cases st st [3: #x] * #H #_ whd in ⊢ (??%% → ?); @eqb_elim [2: * #ABS @⊥ @ABS %] 925 #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin_a1 926 #labels whd in ⊢ (???% → ?); #EQ destruct >act_neutral >act_neutral assumption 927  st1 st2 * [3: #st1] * [3,6,9: #st2] #st3 #l whd in ⊢ (% → ?); * 928 [ #no_final #Hstep #tl #IH whd in ⊢ (% → ?); 929 (* 930 #EQlabels 931 #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta 932 [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st 933 normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) 934 #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption 935  ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta 936 #H cases(bind_inversion ????? H) H * 937 [ #seq * [#lbl1] 938  #newpc 939  #cond #newpc #ltrue #lfalse 940  #lin #io #lout 941  #f 942  943 ] 944 * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate; 945 normalize nodelta >EQfetch >m_return_bind normalize nodelta 946 cases(asm_is_io ??) normalize nodelta 947 [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct 948 2,4,8,9,12,14: #H cases(bind_inversion ????? H) H #x * #_ 949 [3: cases x normalize nodelta 950 6: #H cases(bind_inversion ????? H) H #y * #_ 951 ] 952 ] 953 whd in ⊢ (??%% → ?); #EQ destruct 954 [4,8: cases H1 [1,3: * *: * #y #EQ destruct]] 955 >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct 956 #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r 957 >act_neutral 958 @(instr_map_ok … good … EQfetch … good_st_a1) /2/ 959 ]*) 960  st1 st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H 897 >(act_neutral ?? (act_abs ? abs_t) a1)) 898 change 899 with (get_costlabels_of_trace ??? (?@?)) 900 in match (get_costlabels_of_trace ????); 901 cases l 902 903 >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append skip]3:skip] 904 cases daemon 905  cases daemon ]] 906  st1 #st1 #st3 #st4 #l whd in ⊢ (% → ?); 907 908 * #H3 #H4 909 910 st1 st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H 961 911 #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????); 962 912 whd #costs >dependent_map_append
Note: See TracChangeset
for help on using the changeset viewer.