Nuprl - mb_hybrid Citations of single_tag

mb hybrid Sections GenAutomata Doc

Def single-tag-decomposable(E)(L) ==

L = nil

|E| List

(

L_1,L_2:Trace(E). L = (L_1 @ L_2)

|E| List &

L_2 = nil

|E| List & (

L_1.(

L_2.

(x =msg=(E) y))) & (

m:Label. (

L_2.tag(E)(x) = m)))

is mentioned by

Thm* E:TaggedEventStruct, P,I:TraceProperty(E). MCS(E)(P) safetyR(E) preserves I (I refines single-tag-decomposable(E)) (I fuses P) [M_DASH_C_DASH_S_SPACE_induction]

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]

Try larger context: GenAutomata

mb hybrid Sections GenAutomata Doc

`Thm* E:TaggedEventStruct, P,I:TraceProperty(E). MCS(E)(P) safetyR(E) preserves I (I refines single-tag-decomposable(E)) (I fuses P)`	[M_DASH_C_DASH_S_SPACE_induction]
`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]