Line | |
---|
1 | include "Common.ma". |
---|
2 | |
---|
3 | replace_last x |
---|
4 | epsilon ⇒ epsilon, Some x |
---|
5 | | hd::[ |
---|
6 | |
---|
7 | theorem 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.