Changeset 3390 for LTS/Traces.ma
- Timestamp:
- Oct 10, 2013, 2:53:31 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Traces.ma
r3388 r3390 198 198 | silent_empty : ∀st : S.pre_silent_trace … (t_base S st) 199 199 | silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2. 200 ∀tl : raw_trace S st2 st3. as_classify … st2 = cl_other→ pre_silent_trace … tl →200 ∀tl : raw_trace S st2 st3. as_classify … st2 ≠ cl_io → pre_silent_trace … tl → 201 201 pre_silent_trace … (t_ind … prf … tl). 202 202 … … 208 208 [ #st' #EQ1 #EQ2 destruct #EQ destruct] 209 209 #st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct 210 #EQ destruct #_ #Hclass' @IH [ assumption ] >Hclass % #EQ destruct210 #EQ destruct #_ #Hclass' @IH [ assumption ] assumption 211 211 qed. 212 212 … … 217 217 definition silent_trace : ∀S : abstract_status.∀st1,st2 : S. 218 218 raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧ 219 (is_trace_non_empty … t → as_classify … st1 = cl_other). 219 (is_trace_non_empty … t → as_classify … st1 ≠ cl_io) ∧ 220 well_formed_trace … t. 220 221 221 222 lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S. 222 223 ∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t. 223 #S #st1 #st2 #t elim t -t 224 #S #st1 #st2 #t * // 225 qed. 226 (* elim t -t 224 227 [ #st #_ %] 225 228 #st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2 … … 228 231 #st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_ 229 232 % [ assumption | #_ assumption] 230 qed. 233 qed.*) 231 234 232 235 inductive pre_measurable_trace (S : abstract_status) :
Note: See TracChangeset
for help on using the changeset viewer.