(10steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: no DASH dup DASH fusion 2
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)) fuses P
By:
Using [`J',(Causal(E) No-dup-deliver(E))] (BackThru Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E). ((I J) fuses P) (I fuses J) (P refines J) (I fuses P))
THEN
Try (Unfold `trace_property` 0)
THEN
Try (Fold `trace_property` 0)
Generated subgoals:

1 ((I No-dup-send(E) Tag-by-msg(E)) Causal(E) No-dup-deliver(E)) fuses P
2 (I No-dup-send(E) Tag-by-msg(E)) fuses (Causal(E) No-dup-deliver(E))

About:
listfunctionprop

(10steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc