Nuprl - Pf no_DASH_dup_DASH

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

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 Causal(E)

By: Inst Thm* E:TaggedEventStruct. PTrue fuses Causal(E) [E] THEN BackThruLemma' Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E). (J refines I) (I fuses P) (J fuses P) THEN Try (Unfold `trace_property` 0) THEN Try (Fold `trace_property` 0)

Generated subgoal:

1 (I No-dup-send(E) Tag-by-msg(E)) refines PTrue

About:

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