Nuprl - mb_hybrid Citations of P

mb hybrid Sections GenAutomata Doc

Def Causal(E)(tr) ==

||tr||.

||tr||. j

i &

(is-send(E)(tr[j])) &

(tr[j] =msg=(E) tr[i])

is mentioned by

Thm* E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) asyncR(E) preserves P delayableR(E) preserves P (P refines (Causal(E) No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P) [switch_inv_theorem]

Thm* 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) [switch_inv_plus_normal]

Thm* E:TaggedEventStruct. (switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E) [strong_switch_inv_decomposable]

Thm* E:EventStruct. switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E)) [totalorder_switchable]

Thm* E:EventStruct, P:TraceProperty(E). switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E)) [switchable0_switchable]

Thm* E:EventStruct. switchable0(E)(Causal(E)) [P_causal_switchable0]

Thm* E:TaggedEventStruct. (switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E)) refines single-tag-decomposable(E) [switch_decomp_implies_single_tag_decomp]

Thm* 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) [no_DASH_dup_DASH_fusion]

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) [tag_by_msg_fusion_lemma]

Thm* E:EventStruct. safetyR(E) preserves Causal(E) [P_causal_safety]

Thm* E:TaggedEventStruct. PTrue fuses Causal(E) [causal_fusion]

Thm* E:EventStruct, L:|E| List. L = nil Causal(E)(L) (i:||L||. is-send(E)(L[i])) [P_causal_non_nil]

Thm* E:TaggedEventStruct, tr:|E| List. (m:Label. Causal(E)( < tr > _m)) No-dup-send(E)(tr) Tag-by-msg(E)(tr) [P_tag_by_msg_lemma]

Thm* E:EventStruct, tr:|E| List. Causal(E)(tr) (tr':|E| List. tr' tr (xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x)))) [P_causal_iff]

Def switchable(E)(P) == safetyR(E) preserves P & memorylessR(E) preserves P & (ternary) composableR(E) preserves P & send-enabledR(E) preserves P & asyncR(E) preserves P & delayableR(E) preserves P & (P refines Causal(E)) & (P refines No-dup-deliver(E)) [b_switchable]

Try larger context: GenAutomata

mb hybrid Sections GenAutomata Doc

`Thm* E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) asyncR(E) preserves P delayableR(E) preserves P (P refines (Causal(E) No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P)`	[switch_inv_theorem]
`Thm* 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)`	[switch_inv_plus_normal]
`Thm* E:TaggedEventStruct. (switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E)`	[strong_switch_inv_decomposable]
`Thm* E:EventStruct. switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E))`	[totalorder_switchable]
`Thm* E:EventStruct, P:TraceProperty(E). switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E))`	[switchable0_switchable]
`Thm* E:EventStruct. switchable0(E)(Causal(E))`	[P_causal_switchable0]
`Thm* E:TaggedEventStruct. (switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E)) refines single-tag-decomposable(E)`	[switch_decomp_implies_single_tag_decomp]
`Thm* 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)`	[no_DASH_dup_DASH_fusion]
`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)`	[tag_by_msg_fusion_lemma]
`Thm* E:EventStruct. safetyR(E) preserves Causal(E)`	[P_causal_safety]
`Thm* E:TaggedEventStruct. PTrue fuses Causal(E)`	[causal_fusion]
`Thm* E:EventStruct, L:\|E\| List. L = nil Causal(E)(L) (i:\|\|L\|\|. is-send(E)(L[i]))`	[P_causal_non_nil]
`Thm* E:TaggedEventStruct, tr:\|E\| List. (m:Label. Causal(E)( < tr > _m)) No-dup-send(E)(tr) Tag-by-msg(E)(tr)`	[P_tag_by_msg_lemma]
`Thm* E:EventStruct, tr:\|E\| List. Causal(E)(tr) (tr':\|E\| List. tr' tr (xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x))))`	[P_causal_iff]
`Def switchable(E)(P) == safetyR(E) preserves P & memorylessR(E) preserves P & (ternary) composableR(E) preserves P & send-enabledR(E) preserves P & asyncR(E) preserves P & delayableR(E) preserves P & (P refines Causal(E)) & (P refines No-dup-deliver(E))`	[b_switchable]