Changeset 3531 for LTS/Traces.ma


Ignore:
Timestamp:
Mar 13, 2015, 6:42:58 PM (5 years ago)
Author:
piccolo
Message:

new notion of measurable: some lemmas are still broken

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3524 r3531  
    638638 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
    639639λS,si,s1,s3,sn,t.
    640  pre_measurable_trace … t ∧
    641640 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
    642641 ∃l1,l2,prf1,prf2.
     642 pre_measurable_trace … t12 ∧
    643643  t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
    644644 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ (is_call_act l2 → bool_to_Prop (is_call_post_label … s2))
    645  ∧ silent_trace … ti0 ∧ silent_trace … t3n.
     645 ∧ silent_trace … ti0 ∧ silent_trace … t3n ∧ (is_call_act l1 → bool_to_Prop (is_call_post_label … s0)).
    646646
    647647 
     
    791791lemma measurable_is_measurable_suffix : ∀S : abstract_status.
    792792∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t.
    793 #S #si #s1 #s3 #sn #t * #_ * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 *****
     793#S #si #s1 #s3 #sn #t * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 ******* #_
    794794#EQ destruct /11 width=20 by conj,ex_intro/
    795795qed.
     
    863863qed.
    864864
     865(*
     866
    865867lemma measurable_suffix_is_measurable:
    866868∀S : abstract_status.
     
    881883  /20 width=20 by conj,ex_intro/
    882884]
    883 qed.
     885qed.*)
Note: See TracChangeset for help on using the changeset viewer.