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

At: no DASH dup DASH fusion

E:TaggedEventStruct, P,I:((|E| List)Prop). (P refines (Causal(E) No-dup-deliver(E))) ((I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P) ((I No-dup-send(E)) fuses P)
By:
Auto
THEN
Try (Unfold `trace_property` 0)
THEN
Try (Fold `trace_property` 0)
THEN
BackThru Thm* E:TaggedEventStruct, P,I:((|E| List)Prop). (P refines Causal(E)) ((I No-dup-send(E) Tag-by-msg(E)) fuses P) ((I No-dup-send(E)) fuses P)
Generated subgoals:

11. 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
P refines Causal(E)
21. 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

About:
listfunctionpropimpliesall

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