At: switch normal exists 2 1 1 1 2 1
1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. No-dup-send(E)(tr)
5. x: |E| List
6. switch_inv(E)(x)
7. i: 
(||x||-1)
8. 
R_ad_normal(tr)(x[i],x[(i+1)])
9. is-send(E)(x[i])
loc(E)(x[i]) = loc(E)(x[(i+1)])
By:
ParallelOp -2
THEN
Unfold `R_ad_normal` 0
THEN
Reduce 0
THEN
SimpConcl
Generated subgoals:None
About:
