Nuprl - mb_hybrid Citations of P_no

mb hybrid Sections GenAutomata Doc

Def No-dup-deliver(E)(tr) ==

i,j:

||tr||.

(is-send(E)(tr[i]))

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

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

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

i = j

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)(No-dup-deliver(E)) [P_no_dup_switchable0]

Thm* E:EventStruct. R_permutation(E) preserves No-dup-deliver(E) [P_no_dup_permutable]

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. Tag-by-msg(E) fuses No-dup-deliver(E) [no_dup_fusion]

Thm* E:EventStruct. safetyR(E) preserves No-dup-deliver(E) [P_no_dup_deliver_safety]

Thm* E:EventStruct. send-enabledR(E) preserves No-dup-deliver(E) [P_no_dup_send_enabled]

Thm* E:EventStruct. R_strong_safety(E) preserves No-dup-deliver(E) [P_no_dup_strong_safety]

Thm* E:EventStruct. (ternary) composableR(E) preserves No-dup-deliver(E) [P_no_dup_composable]

Thm* E:EventStruct, tr:|E| List. No-dup-deliver(E)(tr) (x,y:|E|. is-send(E)(x) is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr)) [P_no_dup_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)(No-dup-deliver(E))`	[P_no_dup_switchable0]
`Thm* E:EventStruct. R_permutation(E) preserves No-dup-deliver(E)`	[P_no_dup_permutable]
`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. Tag-by-msg(E) fuses No-dup-deliver(E)`	[no_dup_fusion]
`Thm* E:EventStruct. safetyR(E) preserves No-dup-deliver(E)`	[P_no_dup_deliver_safety]
`Thm* E:EventStruct. send-enabledR(E) preserves No-dup-deliver(E)`	[P_no_dup_send_enabled]
`Thm* E:EventStruct. R_strong_safety(E) preserves No-dup-deliver(E)`	[P_no_dup_strong_safety]
`Thm* E:EventStruct. (ternary) composableR(E) preserves No-dup-deliver(E)`	[P_no_dup_composable]
`Thm* E:EventStruct, tr:\|E\| List. No-dup-deliver(E)(tr) (x,y:\|E\|. is-send(E)(x) is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(\|E\|;[x; y];tr))`	[P_no_dup_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]