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.