Strong behavior refinement

Terminating, Diverging, Aborting and Blocking are the four shapes a behavior refinement takes, one per way a target run can end. StrongRefinement bundles all four for a single pass; the Comp, Trans, Mono, star and sequential lemmas are their algebra.

Each definition is a commuting square, drawn in its doc comment:

• top edge — the pre-relation R between a source configuration σₛ and a target σₜ;
• verticals — one step of each semantics, right-labelled by the trace it emits (ε' source, ε target); the left label names the source semantics taken, sem_s the one being matched (reducing, diverging or blocking) and sem_s' the aborting one;
• bottom row — where each side lands: σₛ'/σₜ' a configuration, ↯ an abort, ∞ a divergence, ∅ a stuck configuration. @. is no edge.

The source trace is existentially quantified and only ever related to the target's — by Rτ on a matched step, by ≼[Rτ] (a sequentially consistent prefix, not a syntactic one; \preceq in the squares) on an abort — never shared. In each square the top and right edges are the hypothesis and the bottom and left are what the definition supplies; amscd draws every edge solid, so that split is not visible.

def StrongRefinement.Terminating {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] {α : Type u_3} {β : Type u_4} (R S : Rel α β) (Rτ : Rel εₛ εₜ) (semₛ : Set (α × εₛ × α)) (semₛ' : Set (α × εₛ)) (semₜ : Set (β × εₜ × β)) : Prop

Behavior refinement for a target run that terminates.

From R σₛ σₜ and a semₜ step (σₜ, ε, σₜ'), the source either takes a matching semₛ step to some σₛ' with S σₛ' σₜ' and Rτ ε' ε, or aborts via semₛ' on a trace with ε' ≼[Rτ] ε. S is the post-relation, usually R again.

$$ \begin{CD} \sigma_s @>R>> \sigma_t \\ @V{\mathit{sem}_s}V{\varepsilon'}V @V{\mathit{sem}_t}V{\varepsilon}V \\ \sigma_s' @>S>> \sigma_t' \end{CD} $$ or $$ \begin{CD} \sigma_s @>R>> \sigma_t \\ @V{\mathit{sem}_s'}V{\varepsilon' \preceq \varepsilon}V @V{\mathit{sem}_t}V{\varepsilon}V \\ \unicode{x21AF} @. \sigma_t' \end{CD} $$

Equations

• One or more equations did not get rendered due to their size.

theorem StrongRefinement.Terminating.Comp {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R S T : Rel α β} [T₂ : Trace εₛ εₜ] {semₛ semᵤ : Set (α × εₛ × α)} {semₛ' semᵤ' : Set (α × εₛ)} {semₜ semᵥ : Set (β × εₜ × β)} : StrongRefinement.Terminating R S Trace.Rτ semₛ semₛ' semₜ → StrongRefinement.Terminating S T Trace.Rτ semᵤ semᵤ' semᵥ → StrongRefinement.Terminating R T Trace.Rτ (semₛ ∘ᵣ₂ semᵤ) (semₛ' ∪ semₛ ∘ᵣ₁ semᵤ') (semₜ ∘ᵣ₂ semᵥ)

Vertical composition: a Terminating refinement of semₛ ∘ᵣ₂ semᵤ against semₜ ∘ᵣ₂ semᵥ, from one refinement of each factor sharing the middle relation S. Trace relation stays Rτ; the composite aborting set is semₛ' ∪ semₛ ∘ᵣ₁ semᵤ'.

theorem StrongRefinement.Terminating.Mono {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R S : Rel α β} [T : Trace εₛ εₜ] {semᵣ semₛ : Set (α × εₛ × α)} {semᵣ' semₛ' : Set (α × εₛ)} {semₜ semᵤ : Set (β × εₜ × β)} (hyp₁ : semₛ ≤ semᵣ) (hyp₂ : semₛ' ≤ semᵣ') (concl : semᵤ ≤ semₜ) : StrongRefinement.Terminating R S Trace.Rτ semₛ semₛ' semₜ ≤ StrongRefinement.Terminating R S Trace.Rτ semᵣ semᵣ' semᵤ

Monotone in the state sets: widen either source set, shrink the target set.

theorem StrongRefinement.Terminating.restrictEnd {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {semₛ' : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} {Qₛ : α → Prop} {Qₜ : β → Prop} (ref : StrongRefinement.Terminating R R Trace.Rτ semₛ semₛ' semₜ) (hback : ∀ (σₛ : α) (σₜ : β), R σₛ σₜ → Qₜ σₜ → Qₛ σₛ) : StrongRefinement.Terminating R R Trace.Rτ {x : α × εₛ × α | x ∈ semₛ ∧ Qₛ x.2.2} semₛ' {x : β × εₜ × β | x ∈ semₜ ∧ Qₜ x.2.2}

Both reducing sets cut to the runs whose final state satisfies a predicate. hback carries the target predicate back across R; without it, restricting the source set would not be monotone. Turns a reachability relation into a terminating semantics on both sides at once.

theorem StrongRefinement.Terminating.Empty {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R S : Rel α β) [T : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {semₛ' : Set (α × εₛ)} : StrongRefinement.Terminating R S Trace.Rτ semₛ semₛ' ∅

A target with no reducing behavior is refined by anything: the empty target set vacates the premise, so the pre- and post-relations and both source sets are unconstrained.

theorem StrongRefinement.Terminating.Id {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) [T : Trace εₛ εₜ] {X : Set (α × εₛ)} : StrongRefinement.Terminating R R Trace.Rτ Relation.Idle X Relation.Idle

Doing nothing refines doing nothing: Relation.Idle on the source refines Relation.Idle on the target, at any aborting set.

theorem StrongRefinement.Terminating.sup {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R S : Rel α β} [T : Trace εₛ εₜ] {A : Set (Set (α × εₛ × α))} {B : Set (Set (β × εₜ × β))} {C : Set (Set (α × εₛ))} (sup : ∀ y ∈ B, ∃ x ∈ A, ∃ z ∈ C, StrongRefinement.Terminating R S Trace.Rτ x z y) : StrongRefinement.Terminating R S Trace.Rτ (⋃₀ A) (⋃₀ C) (⋃₀ B)

⋃₀ on all three sets: every target reducing set in B is refined by some source reducing set in A and some source aborting set in C.

theorem StrongRefinement.Terminating.union {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R S : Rel α β} [T : Trace εₛ εₜ] {Aₛ Bₛ : Set (α × εₛ × α)} {semₛ' : Set (α × εₛ)} {Aₜ Bₜ : Set (β × εₜ × β)} (h₁ : StrongRefinement.Terminating R S Trace.Rτ Aₛ semₛ' Aₜ) (h₂ : StrongRefinement.Terminating R S Trace.Rτ Bₛ semₛ' Bₜ) : StrongRefinement.Terminating R S Trace.Rτ (Aₛ ∪ Bₛ) semₛ' (Aₜ ∪ Bₜ)

Binary union on the reducing sets, aborting set shared and summands paired positionally. The two-element case of Terminating.sup.

theorem StrongRefinement.Terminating.star {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {Yₛ : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} (ref : StrongRefinement.Terminating R R Trace.Rτ semₛ (Relation.star semₛ ∘ᵣ₁ Yₛ) semₜ) : StrongRefinement.Terminating R R Trace.Rτ (Relation.star semₛ) (Relation.star semₛ ∘ᵣ₁ Yₛ) (Relation.star semₜ)

Terminating refinement for Relation.star: from a step-level refinement that answers one target step with a source Relation.star semₛ run, a refinement of Relation.star semₜ with aborting set Relation.star semₛ ∘ᵣ₁ Yₛ. The operator-preservation law standing in for induction over Algebra.reducing's least fixed point.

The hypothesis answers a target step with a source run, not a source step, so a pass whose target has steps with no source counterpart still fits it by instantiating semₛ at a star; Terminating.starStutter packages that instantiation.

theorem StrongRefinement.Terminating.starStutter {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {stepₛ : Set (α × εₛ × α)} {Yₛ : Set (α × εₛ)} {stepₜ : Set (β × εₜ × β)} (ref : StrongRefinement.Terminating R R Trace.Rτ (Relation.star stepₛ) (Relation.star stepₛ ∘ᵣ₁ Yₛ) stepₜ) : StrongRefinement.Terminating R R Trace.Rτ (Relation.star stepₛ) (Relation.star stepₛ ∘ᵣ₁ Yₛ) (Relation.star stepₜ)

Terminating.star with the source instantiated at Relation.star stepₛ and the resulting doubled star collapsed, so a target step is answered by a source run — possibly empty — and the conclusion still reads at Relation.star stepₛ.

def StrongRefinement.Diverging {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] {α : Type u_3} {β : Type u_4} (R : Rel α β) (Rτ : Rel εₛ εₜ) (semₛ semₛ' : Set (α × εₛ)) (semₜ : Set (β × εₜ)) : Prop

Behavior refinement for a target run that diverges.

From R σₛ σₜ and a diverging semₜ run (σₜ, ε), the source either diverges too via semₛ with Rτ ε' ε, or aborts via semₛ' with ε' ≼[Rτ] ε.

$$ \begin{CD} \sigma_s @>R>> \sigma_t \\ @V{\mathit{sem}_s}V{\varepsilon'}V @V{\mathit{sem}_t}V{\varepsilon}V \\ \infty @. \infty \end{CD} $$ or $$ \begin{CD} \sigma_s @>R>> \sigma_t \\ @V{\mathit{sem}_s'}V{\varepsilon' \preceq \varepsilon}V @V{\mathit{sem}_t}V{\varepsilon}V \\ \unicode{x21AF} @. \infty \end{CD} $$

Equations

• StrongRefinement.Diverging R Rτ semₛ semₛ' semₜ = ∀ (σₜ : β) (ε : εₜ) (σₛ : α), R σₛ σₜ → (σₜ, ε) ∈ semₜ → (∃ (ε' : εₛ), Rτ ε' ε ∧ (σₛ, ε') ∈ semₛ) ∨ ∃ (ε' : εₛ), ε' ≼[Rτ] ε ∧ (σₛ, ε') ∈ semₛ'

theorem StrongRefinement.Diverging.Comp {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T₂ : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {semₛ' semₛ'' semᵤ' semᵤ'' : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} {semₜ'' semᵥ'' : Set (β × εₜ)} : StrongRefinement.Diverging R Trace.Rτ semₛ'' semₛ' semₜ'' → StrongRefinement.Diverging R Trace.Rτ semᵤ'' semᵤ' semᵥ'' → StrongRefinement.Terminating R R Trace.Rτ semₛ semₛ' semₜ → StrongRefinement.Diverging R Trace.Rτ (semₛ'' ∪ semₛ ∘ᵣ₁ semᵤ'') (semₛ' ∪ semₛ ∘ᵣ₁ semᵤ') (semₜ'' ∪ semₜ ∘ᵣ₁ semᵥ'')

Vertical composition: a divergence of the first factor, or a terminating run of the first then a divergence of the second, is a divergence of semₛ'' ∪ semₛ ∘ᵣ₁ semᵤ'' against semₜ'' ∪ semₜ ∘ᵣ₁ semᵥ''. Aborting set semₛ' ∪ semₛ ∘ᵣ₁ semᵤ'.

theorem StrongRefinement.Diverging.Mono {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semᵣ'' semᵣ' semₛ'' semₛ' : Set (α × εₛ)} {semₜ'' semᵤ'' : Set (β × εₜ)} (hyp₁ : semₛ'' ≤ semᵣ'') (hyp₂ : semₛ' ≤ semᵣ') (concl : semᵤ'' ≤ semₜ'') : StrongRefinement.Diverging R Trace.Rτ semₛ'' semₛ' semₜ'' ≤ StrongRefinement.Diverging R Trace.Rτ semᵣ'' semᵣ' semᵤ''

Monotone: widen either source set, shrink the target diverging set.

theorem StrongRefinement.Diverging.Empty {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) [T : Trace εₛ εₜ] {semₛ'' semₛ' : Set (α × εₛ)} : StrongRefinement.Diverging R Trace.Rτ semₛ'' semₛ' ∅

An empty target diverging set is refined by anything.

theorem StrongRefinement.Diverging.omega {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [ωMonoid εₛ] [ωMonoid εₜ] [T : ωTrace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {Yₛ : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} (ref : StrongRefinement.Terminating R R Trace.Rτ semₛ (Relation.star semₛ ∘ᵣ₁ Yₛ) semₜ) : StrongRefinement.Diverging R Trace.Rτ (Relation.omega semₛ) (Relation.star semₛ ∘ᵣ₁ Yₛ) (Relation.omega semₜ)

Divergence refinement for Relation.omega, standing in for coinduction. From a step-level Terminating refinement, a refinement of Relation.omega semₜ: the source either keeps pace with the target forever, its trace the infinite product related by Rτ_omega, or aborts at the first index it cannot. The aborting set is fixed to the closed form Relation.star semₛ ∘ᵣ₁ Yₛ, so its absorption law holds by Relation.star.lcomp₁_absorb rather than as a hypothesis.

theorem StrongRefinement.Diverging.omegaStutter {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [ωMonoid εₛ] [ωMonoid εₜ] [T : ωTrace εₛ εₜ] {stepₛ : Set (α × εₛ × α)} {Yₛ : Set (α × εₛ)} {stepₜ : Set (β × εₜ × β)} {μ : β → ℕ} (ref : ∀ (σₜ σₜ' : β) (ε : εₜ) (σₛ : α), R σₛ σₜ → (σₜ, ε, σₜ') ∈ stepₜ → (∃ (σₛ' : α) (ε' : εₛ), R σₛ' σₜ' ∧ Trace.Rτ ε' ε ∧ (σₛ, ε', σₛ') ∈ stepₛ) ∨ R σₛ σₜ' ∧ ε = 1 ∧ μ σₜ' < μ σₜ ∨ ∃ (ε' : εₛ), ε' ≼[Trace.Rτ] ε ∧ (σₛ, ε') ∈ Relation.star stepₛ ∘ᵣ₁ Yₛ) : StrongRefinement.Diverging R Trace.Rτ (Relation.omega stepₛ) (Relation.star stepₛ ∘ᵣ₁ Yₛ) (Relation.omega stepₜ)

Divergence refinement for a stuttering source, where instantiating semₛ at a star is not available (Relation.omega (Relation.star stepₛ) ≤ Relation.omega stepₛ is false). The hypothesis is a stuttering simulation: per target step the source takes one step, or none while a well-founded measure μ on target configurations strictly drops, or aborts. The idle branch requires the target trace to be 1 there — a step the source does not answer must be unobservable.

theorem StrongRefinement.Diverging.star {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {immₛ Yₛ : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} {Yₜ : Set (β × εₜ)} (ref : StrongRefinement.Terminating R R Trace.Rτ semₛ (Relation.star semₛ ∘ᵣ₁ immₛ) semₜ) (refY : StrongRefinement.Diverging R Trace.Rτ Yₛ (Relation.star semₛ ∘ᵣ₁ immₛ) Yₜ) : StrongRefinement.Diverging R Trace.Rτ (Relation.star semₛ ∘ᵣ₁ Yₛ) (Relation.star semₛ ∘ᵣ₁ immₛ) (Relation.star semₜ ∘ᵣ₁ Yₜ)

Divergence refinement for Relation.star semₛ ∘ᵣ₁ Yₛ: finitely many steps, then a divergence. With Diverging.omega it covers the general closed form — gfp (λ x, Y ∪ X ∘ᵣ₁ x) denotes (X* ∘ᵣ₁ Y) ∪ X^∞, and omega alone would force Y = ∅.

theorem StrongRefinement.Diverging.union {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {Aₛ Bₛ semₛ' : Set (α × εₛ)} {Aₜ Bₜ : Set (β × εₜ)} (h₁ : StrongRefinement.Diverging R Trace.Rτ Aₛ semₛ' Aₜ) (h₂ : StrongRefinement.Diverging R Trace.Rτ Bₛ semₛ' Bₜ) : StrongRefinement.Diverging R Trace.Rτ (Aₛ ∪ Bₛ) semₛ' (Aₜ ∪ Bₜ)

Binary union on the diverging sets, aborting set shared.

theorem StrongRefinement.Diverging.closedForm {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [ωMonoid εₛ] [ωMonoid εₜ] [T : ωTrace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {immₛ Yₛ : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} {Yₜ : Set (β × εₜ)} (ref : StrongRefinement.Terminating R R Trace.Rτ semₛ (Relation.star semₛ ∘ᵣ₁ immₛ) semₜ) (refY : StrongRefinement.Diverging R Trace.Rτ Yₛ (Relation.star semₛ ∘ᵣ₁ immₛ) Yₜ) : StrongRefinement.Diverging R Trace.Rτ (Relation.star semₛ ∘ᵣ₁ Yₛ ∪ Relation.omega semₛ) (Relation.star semₛ ∘ᵣ₁ immₛ) (Relation.star semₜ ∘ᵣ₁ Yₜ ∪ Relation.omega semₜ)

The closed form in one piece: gfp (λ x, Y ∪ X ∘ᵣ₁ x) denotes (X* ∘ᵣ₁ Y) ∪ X^∞, and this refines it as such. Diverging.omega is the Y = ∅ special case.

def StrongRefinement.Aborting {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] {α : Type u_3} {β : Type u_4} (R : Rel α β) (Rτ : Rel εₛ εₜ) (semₛ' : Set (α × εₛ)) (semₜ' : Set (β × εₜ)) : Prop

Behavior refinement for a target run that aborts.

From R σₛ σₜ and an aborting semₜ' run (σₜ, ε), the source aborts too via semₛ' with ε' ≼[Rτ] ε. No bottom edge — an abort has no "after".

$$ \begin{CD} \sigma_s @>R>> \sigma_t \\ @V{\mathit{sem}_s'}V{\varepsilon' \preceq \varepsilon}V @V{\mathit{sem}_t'}V{\varepsilon}V \\ \unicode{x21AF} @. \unicode{x21AF} \end{CD} $$

Equations

• StrongRefinement.Aborting R Rτ semₛ' semₜ' = ∀ (σₜ : β) (ε : εₜ) (σₛ : α), R σₛ σₜ → (σₜ, ε) ∈ semₜ' → ∃ (ε' : εₛ), ε' ≼[Rτ] ε ∧ (σₛ, ε') ∈ semₛ'

theorem StrongRefinement.Aborting.toDiverging {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semₛ semₛ' semₛ'' : Set (α × εₛ)} {semₜ' : Set (β × εₜ)} (h : StrongRefinement.Aborting R Trace.Rτ semₛ' semₜ') (hle : semₛ' ≤ semₛ'') : StrongRefinement.Diverging R Trace.Rτ semₛ semₛ'' semₜ'

An abort is a divergence that always takes the aborting branch; the reducing set is unconstrained. hle places the witness in whichever aborting set the diverging statement carries.

theorem StrongRefinement.Diverging.toAborting {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semₛ' : Set (α × εₛ)} {semₜ' : Set (β × εₜ)} (h : StrongRefinement.Diverging R Trace.Rτ semₛ' semₛ' semₜ') : StrongRefinement.Aborting R Trace.Rτ semₛ' semₜ'

The converse of Aborting.toDiverging when the two source sets coincide: the matched branch weakens into the aborting one, so the disjunction collapses.

theorem StrongRefinement.Terminating.Trans {εₛ : Type u_5} {εₜ : Type u_6} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} {γ : Type u_1} {εₘ : Type u_2} [Monoid εₘ] {R₁ S₁ : Rel α β} {R₂ S₂ : Rel β γ} [T₁ : Trace εₛ εₘ] [T₂ : Trace εₘ εₜ] {semₛ : Set (α × εₛ × α)} {semₛ' : Set (α × εₛ)} {semₜ : Set (β × εₘ × β)} {semₜ' : Set (β × εₘ)} {semᵤ : Set (γ × εₜ × γ)} : StrongRefinement.Terminating R₁ S₁ Trace.Rτ semₛ semₛ' semₜ → StrongRefinement.Aborting R₁ Trace.Rτ semₛ' semₜ' → StrongRefinement.Terminating R₂ S₂ Trace.Rτ semₜ semₜ' semᵤ → StrongRefinement.Terminating (R₁ ∘ᵣ R₂) (S₁ ∘ᵣ S₂) (Trace.Rτ ∘ᵣ Trace.Rτ) semₛ semₛ' semᵤ

Horizontal composition through an intermediate language with trace type εₘ. The first leg's trace relation must be left-total and closed (bundled as T₁); the second leg's needs nothing.

theorem StrongRefinement.Diverging.Trans {εₛ : Type u_5} {εₜ : Type u_6} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} {γ : Type u_1} {εₘ : Type u_2} [Monoid εₘ] {R₁ : Rel α β} {R₂ : Rel β γ} [T₁ : Trace εₛ εₘ] [T₂ : Trace εₘ εₜ] {semₛ'' semₛ' : Set (α × εₛ)} {semₜ'' semₜ' : Set (β × εₘ)} {semᵤ'' : Set (γ × εₜ)} : StrongRefinement.Diverging R₁ Trace.Rτ semₛ'' semₛ' semₜ'' → StrongRefinement.Aborting R₁ Trace.Rτ semₛ' semₜ' → StrongRefinement.Diverging R₂ Trace.Rτ semₜ'' semₜ' semᵤ'' → StrongRefinement.Diverging (R₁ ∘ᵣ R₂) (Trace.Rτ ∘ᵣ Trace.Rτ) semₛ'' semₛ' semᵤ''

Horizontal composition through an intermediate language, Terminating.Trans for divergence: only the first leg's trace relation needs laws (bundled as T₁).

theorem StrongRefinement.Aborting.Comp {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T₂ : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {semₛ' semᵤ' : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} {semₜ' semᵥ' : Set (β × εₜ)} : StrongRefinement.Aborting R Trace.Rτ semₛ' semₜ' → StrongRefinement.Aborting R Trace.Rτ semᵤ' semᵥ' → StrongRefinement.Terminating R R Trace.Rτ semₛ semₛ' semₜ → StrongRefinement.Aborting R Trace.Rτ (semₛ' ∪ semₛ ∘ᵣ₁ semᵤ') (semₜ' ∪ semₜ ∘ᵣ₁ semᵥ')

Vertical composition: an abort of the first factor, or a terminating run of the first then an abort of the second, is an abort of semₛ' ∪ semₛ ∘ᵣ₁ semᵤ' against semₜ' ∪ semₜ ∘ᵣ₁ semᵥ'.

theorem StrongRefinement.Aborting.Trans {εₛ : Type u_5} {εₜ : Type u_6} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} {γ : Type u_1} {εₘ : Type u_2} [Monoid εₘ] {R₁ : Rel α β} {R₂ : Rel β γ} [T₁ : Trace εₛ εₘ] [T₂ : Trace εₘ εₜ] {semₛ' : Set (α × εₛ)} {semₜ' : Set (β × εₘ)} {semᵤ' : Set (γ × εₜ)} : StrongRefinement.Aborting R₁ Trace.Rτ semₛ' semₜ' → StrongRefinement.Aborting R₂ Trace.Rτ semₜ' semᵤ' → StrongRefinement.Aborting (R₁ ∘ᵣ R₂) (Trace.Rτ ∘ᵣ Trace.Rτ) semₛ' semᵤ'

Horizontal composition through an intermediate language, Terminating.Trans for aborts.

theorem StrongRefinement.Aborting.Mono {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semᵣ' semₛ' : Set (α × εₛ)} {semₜ' semᵤ' : Set (β × εₜ)} (hyp : semₛ' ≤ semᵣ') (concl : semᵤ' ≤ semₜ') : StrongRefinement.Aborting R Trace.Rτ semₛ' semₜ' ≤ StrongRefinement.Aborting R Trace.Rτ semᵣ' semᵤ'

Monotone: widen the source aborting set, shrink the target aborting set.

theorem StrongRefinement.Aborting.Empty {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) [T : Trace εₛ εₜ] {semₛ' : Set (α × εₛ)} : StrongRefinement.Aborting R Trace.Rτ semₛ' ∅

An empty target aborting set is refined by anything.

theorem StrongRefinement.Aborting.sup {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) [T : Trace εₛ εₜ] {A : Set (Set (α × εₛ))} {B : Set (Set (β × εₜ))} (sup : ∀ y ∈ B, ∃ x ∈ A, StrongRefinement.Aborting R Trace.Rτ x y) : StrongRefinement.Aborting R Trace.Rτ (⋃₀ A) (⋃₀ B)

⋃₀ on both sets: every target aborting set in B is refined by some source aborting set in A.

theorem StrongRefinement.Aborting.union {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {Aₛ Bₛ : Set (α × εₛ)} {Aₜ Bₜ : Set (β × εₜ)} (h₁ : StrongRefinement.Aborting R Trace.Rτ Aₛ Aₜ) (h₂ : StrongRefinement.Aborting R Trace.Rτ Bₛ Bₜ) : StrongRefinement.Aborting R Trace.Rτ (Aₛ ∪ Bₛ) (Aₜ ∪ Bₜ)

Binary union on both aborting sets, summands paired positionally. The two-element case of Aborting.sup.

theorem StrongRefinement.Aborting.star {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {Yₛ : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} {Yₜ : Set (β × εₜ)} (ref : StrongRefinement.Terminating R R Trace.Rτ semₛ (Relation.star semₛ ∘ᵣ₁ Yₛ) semₜ) (refY : StrongRefinement.Aborting R Trace.Rτ Yₛ Yₜ) : StrongRefinement.Aborting R Trace.Rτ (Relation.star semₛ ∘ᵣ₁ Yₛ) (Relation.star semₜ ∘ᵣ₁ Yₜ)

Aborting refinement for Relation.star semₛ ∘ᵣ₁ Yₛ: finitely many steps, then an abort — the shape of Algebra.aborting (step* ∘ᵣ₁ immediate). The operator-preservation law standing in for induction over its least fixed point.

The step-level hypothesis names Relation.star semₛ ∘ᵣ₁ Yₛ as its aborting set — the conclusion's own left-hand side. Not circular: its absorption law holds by Relation.star.lcomp₁_absorb, so it is not an added assumption.

theorem StrongRefinement.Aborting.starStutter {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {stepₛ : Set (α × εₛ × α)} {Yₛ : Set (α × εₛ)} {stepₜ : Set (β × εₜ × β)} {Yₜ : Set (β × εₜ)} (ref : StrongRefinement.Terminating R R Trace.Rτ (Relation.star stepₛ) (Relation.star stepₛ ∘ᵣ₁ Yₛ) stepₜ) (refY : StrongRefinement.Aborting R Trace.Rτ Yₛ Yₜ) : StrongRefinement.Aborting R Trace.Rτ (Relation.star stepₛ ∘ᵣ₁ Yₛ) (Relation.star stepₜ ∘ᵣ₁ Yₜ)

Aborting.star with the source instantiated at Relation.star stepₛ and the doubled star collapsed, so a target step is answered by a source run and the conclusion still reads at Relation.star stepₛ ∘ᵣ₁ Yₛ.

def StrongRefinement.Blocking {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] {α : Type u_3} {β : Type u_4} (R : Rel α β) (Rτ : Rel εₛ εₜ) (semₛ_blk semₛ_abt : Set (α × εₛ)) (semₜ_blk : Set (β × εₜ)) : Prop

Behavior refinement for a target run that blocks: a finite run ending in a configuration that is stuck — nothing steps, nothing aborts — and is not terminal.

From R σₛ σₜ and a blocking semₜ_blk run (σₜ, ε), the source either blocks too via semₛ_blk with Rτ ε' ε, or aborts via semₛ_abt with ε' ≼[Rτ] ε. ∅ marks the stuck configuration; no bottom edge.

$$ \begin{CD} \sigma_s @>R>> \sigma_t \\ @V{\mathit{sem}_s}V{\varepsilon'}V @V{\mathit{sem}_t}V{\varepsilon}V \\ \emptyset @. \emptyset \end{CD} $$ or $$ \begin{CD} \sigma_s @>R>> \sigma_t \\ @V{\mathit{sem}_s'}V{\varepsilon' \preceq \varepsilon}V @V{\mathit{sem}_t}V{\varepsilon}V \\ \unicode{x21AF} @. \emptyset \end{CD} $$

Equations

• One or more equations did not get rendered due to their size.

theorem StrongRefinement.Blocking.Comp {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T₂ : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {semₛ_blk semₛ_abt semᵤ_blk semᵤ_abt : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} {semₜ_blk semᵥ_blk : Set (β × εₜ)} : StrongRefinement.Blocking R Trace.Rτ semₛ_blk semₛ_abt semₜ_blk → StrongRefinement.Blocking R Trace.Rτ semᵤ_blk semᵤ_abt semᵥ_blk → StrongRefinement.Terminating R R Trace.Rτ semₛ semₛ_abt semₜ → StrongRefinement.Blocking R Trace.Rτ (semₛ_blk ∪ semₛ ∘ᵣ₁ semᵤ_blk) (semₛ_abt ∪ semₛ ∘ᵣ₁ semᵤ_abt) (semₜ_blk ∪ semₜ ∘ᵣ₁ semᵥ_blk)

Vertical composition: a blocking run of the second factor after a terminating run of the first is a blocking run of the sequence, with the aborting sets as shared fallback. Same conclusion shape as Diverging.Comp.

theorem StrongRefinement.Blocking.Trans {εₛ : Type u_5} {εₜ : Type u_6} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} {γ : Type u_1} {εₘ : Type u_2} [Monoid εₘ] {R₁ : Rel α β} {R₂ : Rel β γ} [T₁ : Trace εₛ εₘ] [T₂ : Trace εₘ εₜ] {semₛ_blk semₛ_abt : Set (α × εₛ)} {semₜ_blk semₜ_abt : Set (β × εₘ)} {semᵤ_blk : Set (γ × εₜ)} : StrongRefinement.Blocking R₁ Trace.Rτ semₛ_blk semₛ_abt semₜ_blk → StrongRefinement.Aborting R₁ Trace.Rτ semₛ_abt semₜ_abt → StrongRefinement.Blocking R₂ Trace.Rτ semₜ_blk semₜ_abt semᵤ_blk → StrongRefinement.Blocking (R₁ ∘ᵣ R₂) (Trace.Rτ ∘ᵣ Trace.Rτ) semₛ_blk semₛ_abt semᵤ_blk

Horizontal composition through an intermediate language: a blocking run of the composite pass is matched by a blocking run of the first leg, with an abort of the middle language as fallback.

theorem StrongRefinement.Blocking.Mono {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semᵣ_blk semᵣ_abt semₛ_blk semₛ_abt : Set (α × εₛ)} {semₜ_blk semᵤ_blk : Set (β × εₜ)} (hyp₁ : semₛ_blk ≤ semᵣ_blk) (hyp₂ : semₛ_abt ≤ semᵣ_abt) (concl : semᵤ_blk ≤ semₜ_blk) : StrongRefinement.Blocking R Trace.Rτ semₛ_blk semₛ_abt semₜ_blk ≤ StrongRefinement.Blocking R Trace.Rτ semᵣ_blk semᵣ_abt semᵤ_blk

Monotone: widen either source set or shrink the target blocking set.

theorem StrongRefinement.Blocking.Empty {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) [T : Trace εₛ εₜ] {semₛ_blk semₛ_abt : Set (α × εₛ)} : StrongRefinement.Blocking R Trace.Rτ semₛ_blk semₛ_abt ∅

An empty target blocking set is refined by anything.

theorem StrongRefinement.Blocking.union {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {Aₛ Bₛ semₛ_abt : Set (α × εₛ)} {Aₜ Bₜ : Set (β × εₜ)} (h₁ : StrongRefinement.Blocking R Trace.Rτ Aₛ semₛ_abt Aₜ) (h₂ : StrongRefinement.Blocking R Trace.Rτ Bₛ semₛ_abt Bₜ) : StrongRefinement.Blocking R Trace.Rτ (Aₛ ∪ Bₛ) semₛ_abt (Aₜ ∪ Bₜ)

Binary union on the blocking sets, aborting set shared.

theorem StrongRefinement.Blocking.sup {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) [T : Trace εₛ εₜ] {A : Set (Set (α × εₛ))} {B : Set (Set (β × εₜ))} {C : Set (Set (α × εₛ))} (sup : ∀ y ∈ B, ∃ x ∈ A, ∃ z ∈ C, StrongRefinement.Blocking R Trace.Rτ x z y) : StrongRefinement.Blocking R Trace.Rτ (⋃₀ A) (⋃₀ C) (⋃₀ B)

Blocking refinement distributes over an arbitrary union of target blocking sets: each target summand is matched by a source blocking set and a source aborting set of its own.

theorem StrongRefinement.Blocking.star {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {immₛ Yₛ : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} {Yₜ : Set (β × εₜ)} (ref : StrongRefinement.Terminating R R Trace.Rτ semₛ (Relation.star semₛ ∘ᵣ₁ immₛ) semₜ) (refY : StrongRefinement.Blocking R Trace.Rτ Yₛ (Relation.star semₛ ∘ᵣ₁ immₛ) Yₜ) : StrongRefinement.Blocking R Trace.Rτ (Relation.star semₛ ∘ᵣ₁ Yₛ) (Relation.star semₛ ∘ᵣ₁ immₛ) (Relation.star semₜ ∘ᵣ₁ Yₜ)

Blocking refinement for Relation.star semₛ ∘ᵣ₁ Yₛ: finitely many steps, then a block — the shape of an algorithm's blocking semantics (step* ∘ᵣ₁ immediateBlock). Operator-preservation standing in for induction over its least fixed point; same conclusion shape as Diverging.star.

theorem StrongRefinement.Blocking.starStutter {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {stepₛ : Set (α × εₛ × α)} {immₛ Yₛ : Set (α × εₛ)} {stepₜ : Set (β × εₜ × β)} {Yₜ : Set (β × εₜ)} (ref : StrongRefinement.Terminating R R Trace.Rτ (Relation.star stepₛ) (Relation.star stepₛ ∘ᵣ₁ immₛ) stepₜ) (refY : StrongRefinement.Blocking R Trace.Rτ Yₛ (Relation.star stepₛ ∘ᵣ₁ immₛ) Yₜ) : StrongRefinement.Blocking R Trace.Rτ (Relation.star stepₛ ∘ᵣ₁ Yₛ) (Relation.star stepₛ ∘ᵣ₁ immₛ) (Relation.star stepₜ ∘ᵣ₁ Yₜ)

Blocking.star with the source instantiated at Relation.star stepₛ and the doubled star collapsed, so a target step is answered by a source run and the conclusion still reads at Relation.star stepₛ ∘ᵣ₁ Yₛ.

structure StrongRefinement {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) (Rτ : Rel εₛ εₜ) (semₛ₁ : Set (α × εₛ × α)) (semₛ₂ semₛ₃ : Set (α × εₛ)) (semₜ₁ : Set (β × εₜ × β)) (semₜ₂ semₜ₃ : Set (β × εₜ)) (semₛ₄ : Set (α × εₛ)) (semₜ₄ : Set (β × εₜ)) : Prop

All four behavior refinements for one pass, sharing the pre-relation R and trace relation Rτ. The aborting sets semₛ₂/semₜ₂ are the fallback for the terminating, diverging and blocking components alike; semₛ₁/semₜ₁ reduce, semₛ₃/semₜ₃ diverge, semₛ₄/semₜ₄ block.

• terminating : StrongRefinement.Terminating R R Rτ semₛ₁ semₛ₂ semₜ₁
• aborting : StrongRefinement.Aborting R Rτ semₛ₂ semₜ₂
• diverging : StrongRefinement.Diverging R Rτ semₛ₃ semₛ₂ semₜ₃
• blocking : StrongRefinement.Blocking R Rτ semₛ₄ semₛ₂ semₜ₄

theorem StrongRefinement.Comp {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) [T₂ : Trace εₛ εₜ] {semₛ semᵤ : Set (α × εₛ × α)} {semₛ' semₛ'' semₛb semᵤ' semᵤ'' semᵤb : Set (α × εₛ)} {semₜ semᵥ : Set (β × εₜ × β)} {semₜ' semₜ'' semₜb semᵥ' semᵥ'' semᵥb : Set (β × εₜ)} : StrongRefinement R Trace.Rτ semₛ semₛ' semₛ'' semₜ semₜ' semₜ'' semₛb semₜb → StrongRefinement R Trace.Rτ semᵤ semᵤ' semᵤ'' semᵥ semᵥ' semᵥ'' semᵤb semᵥb → StrongRefinement R Trace.Rτ (semₛ ∘ᵣ₂ semᵤ) (semₛ' ∪ semₛ ∘ᵣ₁ semᵤ') (semₛ'' ∪ semₛ ∘ᵣ₁ semᵤ'') (semₜ ∘ᵣ₂ semᵥ) (semₜ' ∪ semₜ ∘ᵣ₁ semᵥ') (semₜ'' ∪ semₜ ∘ᵣ₁ semᵥ'') (semₛb ∪ semₛ ∘ᵣ₁ semᵤb) (semₜb ∪ semₜ ∘ᵣ₁ semᵥb)

Vertical composition of two full refinements, staying at the trace relation Rτ. Composing a chain stays at Rτ however long the chain.

theorem StrongRefinement.ofNonDiverging {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) [T : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {semₛ' semₛ'' semₛ''' : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} {semₜ' : Set (β × εₜ)} (h₁ : StrongRefinement.Terminating R R Trace.Rτ semₛ semₛ' semₜ) (h₂ : StrongRefinement.Aborting R Trace.Rτ semₛ' semₜ') : StrongRefinement R Trace.Rτ semₛ semₛ' semₛ'' semₜ semₜ' ∅ semₛ''' ∅

A full refinement from just the terminating and aborting components, with the target diverging and blocking sets empty.

theorem StrongRefinement.ofTerminating {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} (R : Rel α β) [T : Trace εₛ εₜ] {semₛ : Set (α × εₛ × α)} {semₛ' semₛ'' semₛ''' : Set (α × εₛ)} {semₜ : Set (β × εₜ × β)} (h : StrongRefinement.Terminating R R Trace.Rτ semₛ semₛ' semₜ) : StrongRefinement R Trace.Rτ semₛ semₛ' semₛ'' semₜ ∅ ∅ semₛ''' ∅

A full refinement from just the terminating component, with every other target set empty.

theorem StrongRefinement.Trans {εₛ : Type u_3} {εₜ : Type u_6} [Monoid εₛ] [Monoid εₜ] {α : Type u_4} {β : Type u_5} {γ : Type u_1} {εₘ : Type u_2} [Monoid εₘ] [T₁ : Trace εₛ εₘ] {R₁ : Rel α β} {R₂ : Rel β γ} [T₂ : Trace εₘ εₜ] {semₛ : Set (α × εₛ × α)} {semₛ' semₛ'' semₛb : Set (α × εₛ)} {semₜ : Set (β × εₘ × β)} {semₜ' semₜ'' semₜb : Set (β × εₘ)} {semᵤ : Set (γ × εₜ × γ)} {semᵤ' semᵤ'' semᵤb : Set (γ × εₜ)} : StrongRefinement R₁ Trace.Rτ semₛ semₛ' semₛ'' semₜ semₜ' semₜ'' semₛb semₜb → StrongRefinement R₂ Trace.Rτ semₜ semₜ' semₜ'' semᵤ semᵤ' semᵤ'' semₜb semᵤb → StrongRefinement (R₁ ∘ᵣ R₂) (Trace.Rτ ∘ᵣ Trace.Rτ) semₛ semₛ' semₛ'' semᵤ semᵤ' semᵤ'' semₛb semᵤb

Horizontal composition of two full refinements through an intermediate language. T₁ bundles the first leg's trace relation and its laws. No union in the conclusion, unlike Comp: every run passes through the middle language.

theorem StrongRefinement.Mono {εₛ : Type u_3} {εₜ : Type u_4} [Monoid εₛ] [Monoid εₜ] {α : Type u_1} {β : Type u_2} {R : Rel α β} [T : Trace εₛ εₜ] {semᵣ semₛ : Set (α × εₛ × α)} {semᵣ' semᵣ'' semᵣb semₛ' semₛ'' semₛb : Set (α × εₛ)} {semₜ semᵤ : Set (β × εₜ × β)} {semₜ' semₜ'' semₜb semᵤ' semᵤ'' semᵤb : Set (β × εₜ)} (hyp₁ : semₛ ≤ semᵣ) (hyp₂ : semₛ' ≤ semᵣ') (hyp₃ : semₛ'' ≤ semᵣ'') (hyp₄ : semₛb ≤ semᵣb) (concl₁ : semᵤ ≤ semₜ) (concl₂ : semᵤ' ≤ semₜ') (concl₃ : semᵤ'' ≤ semₜ'') (concl₄ : semᵤb ≤ semₜb) : StrongRefinement R Trace.Rτ semₛ semₛ' semₛ'' semₜ semₜ' semₜ'' semₛb semₜb ≤ StrongRefinement R Trace.Rτ semᵣ semᵣ' semᵣ'' semᵤ semᵤ' semᵤ'' semᵣb semᵤb

Monotone in all eight state sets: widen the four source sets, shrink the four target sets.

theorem StrongRefinement.sequential {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} [ωMonoid εₛ] [ωMonoid εₜ] [T : ωTrace εₛ εₜ] {R : Rel α β} {stepₛ : Set (α × εₛ × α)} {immₛ Yₛ blkₛ : Set (α × εₛ)} {stepₜ : Set (β × εₜ × β)} {immₜ Yₜ blkₜ : Set (β × εₜ)} (ref : StrongRefinement.Terminating R R Trace.Rτ stepₛ (Relation.star stepₛ ∘ᵣ₁ immₛ) stepₜ) (refImm : StrongRefinement.Aborting R Trace.Rτ immₛ immₜ) (refY : StrongRefinement.Diverging R Trace.Rτ Yₛ (Relation.star stepₛ ∘ᵣ₁ immₛ) Yₜ) (refBlk : StrongRefinement.Blocking R Trace.Rτ blkₛ (Relation.star stepₛ ∘ᵣ₁ immₛ) blkₜ) : StrongRefinement R Trace.Rτ (Relation.star stepₛ) (Relation.star stepₛ ∘ᵣ₁ immₛ) (Relation.star stepₛ ∘ᵣ₁ Yₛ ∪ Relation.omega stepₛ) (Relation.star stepₜ) (Relation.star stepₜ ∘ᵣ₁ immₜ) (Relation.star stepₜ ∘ᵣ₁ Yₜ ∪ Relation.omega stepₜ) (Relation.star stepₛ ∘ᵣ₁ blkₛ) (Relation.star stepₜ ∘ᵣ₁ blkₜ)

Assembles per-step refinements into a full StrongRefinement at the shapes a step-and-iterate semantics takes: step*, step* ∘ᵣ₁ immediate, (step* ∘ᵣ₁ Y) ∪ step^∞, step* ∘ᵣ₁ blocking. Standing in for induction over Algebra's fixed points.

Four hypotheses, each about one step: a Terminating for the step, and Aborting/Diverging/ Blocking for the sets a step can abort, diverge or block into. Yₛ/Yₜ are the immediate-divergence sets — general because whether a step can diverge is a property of the semantics, not this framework. sequentialOmega is the Y = ∅ case that Algebra uses.

theorem StrongRefinement.sequentialOmega {εₛ : Type u_1} {εₜ : Type u_2} [Monoid εₛ] [Monoid εₜ] {α : Type u_3} {β : Type u_4} [ωMonoid εₛ] [ωMonoid εₜ] [T : ωTrace εₛ εₜ] {R : Rel α β} {stepₛ : Set (α × εₛ × α)} {immₛ blkₛ : Set (α × εₛ)} {stepₜ : Set (β × εₜ × β)} {immₜ blkₜ : Set (β × εₜ)} (ref : StrongRefinement.Terminating R R Trace.Rτ stepₛ (Relation.star stepₛ ∘ᵣ₁ immₛ) stepₜ) (refImm : StrongRefinement.Aborting R Trace.Rτ immₛ immₜ) (refBlk : StrongRefinement.Blocking R Trace.Rτ blkₛ (Relation.star stepₛ ∘ᵣ₁ immₛ) blkₜ) : StrongRefinement R Trace.Rτ (Relation.star stepₛ) (Relation.star stepₛ ∘ᵣ₁ immₛ) (Relation.omega stepₛ) (Relation.star stepₜ) (Relation.star stepₜ ∘ᵣ₁ immₜ) (Relation.omega stepₜ) (Relation.star stepₛ ∘ᵣ₁ blkₛ) (Relation.star stepₜ ∘ᵣ₁ blkₜ)

sequential at Y = ∅, so the diverging component is just step^∞. The algorithm layer's case — an atomic block has no diverging semantics — where the conclusion is then definitionally Algebra.reducing/.aborting/.diverging, applied without rewriting.