E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), tr_l:A List. No-dup-send(E)(map(evt;tr_l)) No-dup-send( < A,evt,tg > (E))(tr_l)

1

1. E: EventStruct 2. A: Type 3. evt: A|E| 4. tg: ALabel 5. tr_l: A List 6. i,j:||map(evt;tr_l)||. is-send(E)(map(evt;tr_l)[i]) is-send(E)(map(evt;tr_l)[j]) (map(evt;tr_l)[i] =msg=(E) map(evt;tr_l)[j]) i = j 7. i: ||tr_l|| 8. j: ||tr_l|| 9. is-send( < A,evt,tg > (E))(tr_l[i]) 10. is-send( < A,evt,tg > (E))(tr_l[j]) 11. tr_l[i] =msg=( < A,evt,tg > (E)) tr_l[j] i = j

About: