Manuscript IX-D-ST@1 · IX-D-ST.tex · lemma · b1dc631a

Lemma: A comparison domain for both free orderings

Functional support and separate causal interfaces · lines 651–672 · proof included or linked

IX-D-ST@1#lem:comparison

The domain

D_{cmp} = D_{decl} \cap σ (D_{decl})

is stable under $σ, γ, †$ . It contains $D_{first}$ .

Proof. Flip stability is immediate. Dagger stability of $D_{decl}$ gives $γ (D_{decl}) = σ (D_{decl})$ . Thus

γ (D_{cmp}) = σ (D_{decl}) \cap D_{decl} = D_{cmp} .

The first-stage domain contains both orderings, so is contained in $D_{cmp}$ .

Displayed formulas in this passage