¶Union of s₁..t₁ or ≁ t₂
When the "pivot" of the incomparable constraint is not comparable with either bound of the range constraint, the incomparable constraint subsumes the range constraint. Otherwise the union cannot be simplified.
(s₁..t₁) ∨ (≁ t₂) = (≁ t₂) if s₁ ≁ t₂ ∧ t₁ ≁ t₂
= (s₁..t₁) ∨ (≁ t₂) otherwise
¶Equationally
⟦s₁..t₁⟧ = {x | s₁ ⊆ x ∧ x ⊆ t₁}
⟦≁ t₂⟧ = {x | x ⊈ t₂ ∧ t₂ ⊈ x}
When s₁ ≁ t₂ ∧ t₁ ≁ t₂:
[s₁ ≁ t₂ ∧ t₁ ≁ t₂]⁰ [s₁ ≁ t₂ ∧ t₁ ≁ t₂]⁰
─────────────────── ───────────────────
⋮ [s₁ ⊆ x ∧ x ⊆ t₁]¹ ⋮
⋮ ───────────────── ⋮
⋮ [x ⊆ t₂]³ s₁ ⊆ x x ⊆ t₁ [t₂ ⊆ x]³ ⋮
⋮ ───────────────────── ──────────────────── ⋮
s₁ ⊈ t₂ s₁ ⊆ t₂ t₂ ⊆ t₁ t₂ ⊈ t₁
────────────────────── ─────────────────────────
false [x ~ t₂]² false
⋮ ─────────────── ⋮
⋮ x ⊆ t₂ ∨ t₂ ⊆ x ⋮
────────────────────────────────────────────────³
false
──────²
x ≁ t₂
──────────────────────────¹
(s₁ ⊆ x ∧ x ⊆ t₁) → x ≁ t₂
────────────────────────────────────
{x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≁ t₂}
─────────────────
⟦s1..t₁⟧ ⊆ ⟦≁ t₂⟧
──────────────────────────
⟦s1..t₁⟧ ∪ ⟦≁ t₂⟧ = ⟦≁ t₂⟧
────────────────────────────────────────────────⁰
(s₁ ≁ t₂ ∧ t₁ ≁ t₂) → ⟦s1..t₁⟧ ∪ ⟦≁ t₂⟧ = ⟦≁ t₂⟧