At: switch inv rel closure send 1 2 1
1. E: EventStruct
2. tr: |E| List
3. ls: 
||tr||
4. i: ||tr||
5. is-send(E)(tr[ls])
6. i (switchR(tr)^*) ls
7. 
x,y:||tr||. (x (switchR(tr)^*) y) 
is-send(E)(tr[x]) 
x = y
8. i = ls
is-send(E)(tr[i])
By: HypSubst -1 0
Generated subgoals:None
About:
