source: LTS/Simulation.ma @ 3382

include "Common.ma".

replace_last x
   epsilon ⇒ epsilon, Some x
 | hd::[

theorem simulates:
 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
  pre_measurable_trace … t1 →
  well_formed_trace … t1.
 ∀l1: option NonFunctionalLabel.
 ∀s1'.
   S s1 s1' →
   ∃s2'. ∃t2: raw_trace … s1' s2'.
    pre_mesurable_trace … t2 ∧
    well_formed_trace … t2.
   ∃l2: option NonFunctionalLabel.
    match l1 with
    [ None ⇒
       match l2 with
       [ None ⇒ |t1| = |t2|
       | Some l2' ⇒ |t1| = l2'::|t2| ]
    | Some l1' ⇒
       let 〈t1',x〉 ≝ replace_last l1' t1 in
       match x with
       [ None ⇒
          match l2 with
          [ None ⇒ |t1'| = |t2|
          | Some l2' ⇒ |t1'| = l2'::|t2| ]
       | Some x ⇒ l2 = x ]