At: no DASH dup DASH fusion 2 2 1 1
1. E: TaggedEventStruct
2. P: (|E| List)
Prop
3. I: (|E| List)Prop
4. P refines (Causal(E) 
No-dup-deliver(E))
5. (I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P
(I No-dup-send(E) Tag-by-msg(E)) refines PTrue
By:
Unfolds [`tr_refines`;`PTrue`] 0
THEN
Reduce 0
THEN
Try (Fold `trace_property` 0)
Generated subgoals:None
About:
