At: switch inv rel closure lemma1 1 2 1 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
i (switchR(tr)^*) ls
By:
Unfold `rel_star` 0
THEN
Reduce 0
THEN
InstConcl [n]
Generated subgoals:None
About:
