2. tr: |E| List
3. No-dup-send(E)(tr)
4. i:
||tr||5. j:
||tr||6. tr[i] =msg=(E) tr[j]
7. Causal(E)( < tr > _tag(E)(tr[i]))
8. Causal(E)( < tr > _tag(E)(tr[j]))
tag(E)(tr[i]) = tag(E)(tr[j]) 
E:TaggedEventStruct, tr:|E| List.
(m:Label. Causal(E)( < tr > _m)) 
No-dup-send(E)(tr) Tag-by-msg(E)(tr)
h.(InstHyp [tag(E)(tr[i])] h) THEN (InstHyp [tag(E)(tr[j])] h) THEN (Thin h))| 1 | 1. E: TaggedEventStruct 2. tr: |E| List 3. No-dup-send(E)(tr) 4. i: ||tr||5. j: ||tr||6. tr[i] =msg=(E) tr[j] 7. Causal(E)( < tr > _tag(E)(tr[i])) 8. Causal(E)( < tr > _tag(E)(tr[j])) tag(E)(tr[i]) = tag(E)(tr[j]) |
About:
 |  |  |  |  |