1 | 1. E: TaggedEventStruct 2. P: (|E| List)Prop 3. I: (|E| List)Prop 4. P refines Causal(E) 5. tr:|E| List. (m:Label. P( < tr > _m)) I(tr) & No-dup-send(E)(tr) & Tag-by-msg(E)(tr) P(tr) 6. tr: |E| List 7. m:Label. P( < tr > _m) 8. I(tr) 9. No-dup-send(E)(tr) Tag-by-msg(E)(tr) |
About: