Changeset 3579 for LTS/Simulation.ma


Ignore:
Timestamp:
Jul 10, 2015, 4:08:09 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3549 r3579  
    1515(rel : relations …S1 S2) : Prop ≝
    1616 { initial_is_initial :
    17    ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
    18  ; final_is_final :
    19    ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
     17   ∀s1,s2.(bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2)) → Srel … rel s1 s2
     18 ; final_is_final : 
     19   ∀s1,s2.bool_to_Prop (as_final … s1) → Srel … rel s1 s2 → bool_to_Prop (as_final … s2)
    2020 ; io_is_io :
    2121   ∀s1,s2.Srel … rel s1 s2 → as_classify … s2 = cl_io → as_classify … s1 = cl_io
Note: See TracChangeset for help on using the changeset viewer.