2. tr: |E| List
3. ls:
||tr||4. i:
||tr||5. is-send(E)(tr[ls])
6. i (switchR(tr)^*) ls
is-send(E)(tr[i]) 
E:EventStruct, tr:|E| List, ls,i:||tr||.
is-send(E)(tr[ls]) 
(i (switchR(tr)^*) ls) is-send(E)(tr[i])| 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 is-send(E)(tr[i]) |
About:
 |  |  |  |  |  |