At: switch inv rel closure lemma1 1 2 1 1
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:, i,j:||tr||.
i
j is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n ls) (j (switchR(tr)^*) ls)
7. i: ||tr||
8. j: ||tr||
9. ij
10. is-send(E)(tr[j])
11. n:
12. i switchR(tr)^n ls
is-send(E)(tr[i])
By: Inst
Thm* E:EventStruct, tr:|E| List, ls,i:||tr||.
is-send(E)(tr[ls]) (i (switchR(tr)^*) ls) is-send(E)(tr[i])
[E;tr;ls;i]
Generated subgoal:| 1 | i (switchR(tr)^*) ls |
About:
