Changeset 3506 for LTS/Vm.ma


Ignore:
Timestamp:
Sep 26, 2014, 5:00:57 PM (5 years ago)
Author:
sacerdot
Message:

Refactoring.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3505 r3506  
    702702]
    703703qed.
    704 
    705 include "Simulation.ma".
    706704
    707705definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
     
    11021100qed.
    11031101
    1104 definition measurable :
    1105  ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
    1106 λS,si,s1,s3,sn,t.
    1107  pre_measurable_trace … t ∧
    1108  ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
    1109  ∃l1,l2,prf1,prf2.
    1110   t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
    1111  ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n.
    1112  
    11131102lemma chop_cons : ∀A : Type[0].∀x : A.∀xs: list A. xs ≠ [ ] → chop … (x :: xs) = x :: (chop … xs).
    11141103#A #x * [ #H cases(absurd ?? H) % ] // qed.
Note: See TracChangeset for help on using the changeset viewer.