At: switch normal exists 2 1 1 1 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)])
is-send(E)(x[(i+1)])
By:
ParallelOp -1
THEN
Unfold `R_ad_normal` 0
THEN
Reduce 0
THEN
SimpConcl
Generated subgoals:None
About:
