Changeset 3496
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3495 r3496 660 660 definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝ 661 661 λS,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3)) 662 ∧ ((is_costlabelled_act l ∨ is_labelled_ret_act l) ∧ 663 (is_call_act l → bool_to_Prop (is_call_post_label … s2))). 662 ∧ is_costlabelled_act l. 664 663 665 664 definition big_op: ∀M: monoid. list M → M ≝ … … 871 870 #S #st1 #st2 #st3 * // qed. 872 871 873 lemma actionlabel_ok : ∀l : ActionLabel.874 (is_costlabelled_act l ∨ is_labelled_ret_act l) → ∃c.actionlabel_to_costlabel l = [c].875 * /2 by refl, ex_intro/ 876 [ * /2/ ** #x #EQ destruct  * /2/ ** #x #EQ destruct] 872 lemma actionlabel_ok : 873 ∀l : ActionLabel. 874 is_costlabelled_act l → ∃c.actionlabel_to_costlabel l = [c]. 875 * /2/ * /2/ * 877 876 qed. 878 877 … … 901 900 ] 902 901 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * #l1 * #prf1 * #EQ destruct 903 * #Hlabelled 904 >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1)) 902 #Hlabelled >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1)) 905 903 [2: >get_cost_label_append >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled) 906 904 #c #EQc >EQc // 907 905 ] 908 906 lapply Hlabelled lapply prf1 prf1 lapply l1 l1 elim t1 st3 909 [ * [3: #st] #l #prf #H1 #H2 #k #_whd in ⊢ (??%? → ?);907 [ * [3: #st] #l #prf #H1 #H2 #k whd in ⊢ (??%? → ?); 910 908 [3: cases prf 911 909 2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?); … … 945 943 ] 946 944 ] 947 whd in ⊢ (??%% → ?); #EQ destruct 948 [4,8: cases H1 [1,3: * *: * #y #EQ destruct]] 945 whd in ⊢ (??%% → ?); #EQ destruct [4,8: cases H1 ] 949 946 >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct 950 947 #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ destruct >neutral_r … … 968 965 ] 969 966 ] 970 #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab # l1_lab1 #k #pre_meas whd in ⊢ (??%? → ?);967 #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #k #pre_meas whd in ⊢ (??%? → ?); 971 968 >rewrite_in_dependent_map [2,5: @get_cost_label_of_trace_tind 3,6: ] 972 969 >dependent_map_append
Note: See TracChangeset
for help on using the changeset viewer.