At: switch inv rel closure send 1 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: ||tr||
8. y: ||tr||
9. x switchR(tr) y
is-send(E)(tr[x])
By:
Unfold `switch_inv_rel` -1
THEN
Reduce -1
THEN
Complete Auto
Generated subgoals:None
About:
