At: switch normal exists 2 1 2
1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. No-dup-send(E)(tr)
5. L': |E| List
6. tr (swap adjacent[
R_ad_normal(tr)(x,y)]^*) L'
7. 
i:
(||L'||-1). R_ad_normal(tr)(L'[i],L'[(i+1)])
8. swap adjacent[R_ad_normal(tr)(x,y)]^* preserves switch_inv(E)
switch_inv(E)(L')
By:
Unfold `preserved_by` -1
THEN
Reduce -1
THEN
InstHyp [tr;L'] -1
Generated subgoals:None
About:
