¶Union of s₁..t₁ or s₂..t₂
When one of the bounds is entirely contained within the other, the union simplifies to the larger bounds. Otherwise it cannot be simplified.
(s₁..t₁) ∨ (s₂..t₂) = (s₂..t₂) if s₂ ⊆ s₁ ∧ t₁ ⊆ t₂
= (s₁..t₁) ∨ (s₂..t₂) otherwise
¶Equationally
⟦s₁..t₁⟧ = {x | s₁ ⊆ x ∧ x ⊆ t₁}
⟦s₂..t₂⟧ = {x | s₂ ⊆ x ∧ x ⊆ t₂}
When s₂ ⊆ s₁ ∧ t₁ ⊆ t₂, transitivity lets us expand from the "smaller" bounds (s₁ and t₁) to the "larger" bounds (s₂ and t₂):
⟦s₁..t₁ ∨ s₂..t₂⟧
= {x | (s₁ ⊆ x ∧ x ⊆ t₁) ∨ (s₂ ⊆ x ∧ x ⊆ t₂)}
= {x | (s₂ ⊆ x ∧ x ⊆ t₂) ∨ (s₂ ⊆ x ∧ x ⊆ t₂)}
= {x | s₂ ⊆ x ∧ x ⊆ t₂}
= ⟦s₂..t₂⟧