source: LTS/Simulation.ma @ 3382

Last change on this file since 3382 was 3382, checked in by sacerdot, 6 years ago

The simulation statement.

File size: 766 bytes
Line 
1include "Common.ma".
2
3replace_last x
4   epsilon ⇒ epsilon, Some x
5 | hd::[
6
7theorem simulates:
8 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
9  pre_measurable_trace … t1 →
10  well_formed_trace … t1.
11 ∀l1: option NonFunctionalLabel.
12 ∀s1'.
13   S s1 s1' →
14   ∃s2'. ∃t2: raw_trace … s1' s2'.
15    pre_mesurable_trace … t2 ∧
16    well_formed_trace … t2.
17   ∃l2: option NonFunctionalLabel.
18    match l1 with
19    [ None ⇒
20       match l2 with
21       [ None ⇒ |t1| = |t2|
22       | Some l2' ⇒ |t1| = l2'::|t2| ]
23    | Some l1' ⇒
24       let 〈t1',x〉 ≝ replace_last l1' t1 in
25       match x with
26       [ None ⇒
27          match l2 with
28          [ None ⇒ |t1'| = |t2|
29          | Some l2' ⇒ |t1'| = l2'::|t2| ]
30       | Some x ⇒ l2 = x ]
Note: See TracBrowser for help on using the repository browser.