Nuprl - Pf switch_inv_plus

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

E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) (P refines (Causal(E) No-dup-deliver(E))) (((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P)

By: Unfolds [`str_trace`;`trace_property`] 0 THEN Try ((Fold `trace_property` 0) THEN (Complete Auto)) THEN Try ((Unfold `trace_property` 0) THEN (Complete Auto)) THEN BackThru `no-dup-fusion` THEN Try (Fold `trace_property` 0)

Generated subgoal:

1 1. E: TaggedEventStruct
2. P: (|E| List)Prop
3. MCS(E)(P)
4. P refines (Causal(E) No-dup-deliver(E))
((switch_inv(E) AD-normal(E)) No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P

About:

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