(22steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: switch inv rel closure lemma1 1 1 2 1 1 2 1 2
1. E: EventStruct
2. tr: |E| List
3. ls: ||tr||
4. is-send(E)(tr[ls])
5. j:||tr||. ls < j is-send(E)(tr[j])
6. n:
7. 0 < n
8. i,j:||tr||. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n-1 ls) (j (switchR(tr)^*) ls)
9. i: ||tr||
10. j: ||tr||
11. ij
12. is-send(E)(tr[i])
13. is-send(E)(tr[j])
14. i switchR(tr)^n ls
15. n = 0
16. z: ||tr||
17. is-send(E)(tr[i])
18. is-send(E)(tr[z])
19. i < z
20. tr[z] somewhere delivered before tr[i]
21. z switchR(tr)^n-1 ls
22. i (switchR(tr)^*) ls
23. z (switchR(tr)^*) ls
24. zj
25. j = i

j (switchR(tr)^*) ls
By:
Inst Thm* E:EventStruct, a,b,c:|E|, tr:|E| List. a somewhere delivered before b a somewhere delivered before c c somewhere delivered before b [E;tr[z];tr[i];tr[j];tr]
THEN
Analyze -1
Generated subgoals:

126. tr[z] somewhere delivered before tr[j]
j (switchR(tr)^*) ls
226. tr[j] somewhere delivered before tr[i]
j (switchR(tr)^*) ls

About:
listassertintnatural_numbersubtractless_thanapplyequalimpliesall

(22steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc