At: switch inv rel closure 1 1 1
1. E: TaggedEventStruct
2. tr: |E| List
3. ls: 
||tr||
4. switch_inv(E)(tr)
5. i: ||tr||
6. j: ||tr||
7. i (switchR(tr)^*) ls
8. j (switchR(tr)^*) ls
9. x: ||tr||
10. y: ||tr||
11. x switchR(tr) y
tag(E)(tr[x]) = tag(E)(tr[y])
By: BackThru
Thm* 
E:TaggedEventStruct, tr:|E| List.
switch_inv(E)(tr) 
(i,j:||tr||. (i switchR(tr) j) 
tag(E)(tr[i]) = tag(E)(tr[j]))
Generated subgoals:None
About:
