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.