¶Union of s₁..t₁ or ≠ t₂
When the range constraint contains the "hole" from the non-equivalent constraint, then the result is always satisfiable. Otherwise the range constrant is subsumed by the non-equivalent constraint.
(s₁..t₁) ∨ (≠ t₂) = 𝟙 is s₁ ⊆ t₂ ∧ t₂ ⊆ t₁
= (≠ t₂) otherwise
¶Equationally
⟦s₁..t₁⟧ = {x | s₁ ⊆ x ∧ x ⊆ t₁}
⟦≠ t₂⟧ = {x | x ⊈ t₂ ∨ t₂ ⊈ x}
When s₁ ⊆ t₂ ∧ t₂ ⊆ t₁, transitivity lets us show that t₂ ⊆ x and x ⊆ t₂, which shows that t₂ is in the result. The ≠ t₂ constraint adds every other type to the result as well.
⟦s₁..t₁ ∨ (≠ t₂)⟧
= {x | (s₁ ⊆ x ∧ x ⊆ t₁) ∨ (x ⊈ t₂ ∨ t₂ ⊈ x)}
= {x | (s₁ ⊆ x ∨ x ⊈ t₂ ∨ t₂ ⊈ x) ∧ (x ⊆ t₁ ∨ x ⊈ t₂ ∨ t₂ ⊈ x)}
= {x | (t₂ ⊆ x ∨ x ⊈ t₂ ∨ t₂ ⊈ x) ∧ (x ⊆ t₂ ∨ x ⊈ t₂ ∨ t₂ ⊈ x)}
= {x | (true ∨ x ⊈ t₂) ∧ (true ∨ t₂ ⊈ x)}
= {x | true ∧ true}
= {x | true}
= 𝟙
When t₂ ⊂ s₁:
[s₁ ⊆ x ∧ x ⊆ t₁]¹
─────────────────
s₁ ⊆ x [t₂ ⊂ s₁]⁰
────────────────────────
t₂ ⊂ x
──────
x ≠ t₂
──────────────────────────¹
(s₁ ⊆ x ∧ x ⊆ t₁) → x ≠ t₂
────────────────────────────────────
{x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≠ t₂}
─────────────────
⟦s1..t₁⟧ ⊆ ⟦≠ t₂⟧
──────────────────────────
⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
────────────────────────────────────⁰
t₂ ⊂ s₁ → ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
When s₁ ≁ t₂:
[s₁ ⊆ x ∧ x ⊆ t₁]¹ [x = t₂]²
───────────────── ────────
s₁ ⊆ x x ⊆ t₂ [s₁ ≁ t₂]⁰
────────────────────── ─────────
s₁ ⊆ t₂ s₁ ⊈ t₂
────────────────────────────
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₂ → ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
When t₁ ⊂ t₂:
[s₁ ⊆ x ∧ x ⊆ t₁]¹
─────────────────
x ⊆ t₁ [t₁ ⊂ t₂]⁰
────────────────────────
x ⊂ t₂
──────
x ≠ t₂
──────────────────────────¹
(s₁ ⊆ x ∧ x ⊆ t₁) → x ≠ t₂
────────────────────────────────────
{x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≠ t₂}
─────────────────
⟦s1..t₁⟧ ⊆ ⟦≠ t₂⟧
──────────────────────────
⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
────────────────────────────────────⁰
t₁ ⊂ t₂ → ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
When t₁ ≁ t₂:
[s₁ ⊆ x ∧ x ⊆ t₁]¹ [x = t₂]²
───────────────── ────────
x ⊆ t₁ t₂ ⊆ x [t₁ ≁ t₂]⁰
────────────────────── ─────────
t₂ ⊆ t₁ t₂ ⊈ t₁
────────────────────────────
false
──────²
x ≠ t₂
──────────────────────────¹
(s₁ ⊆ x ∧ x ⊆ t₁) → x ≠ t₂
────────────────────────────────────
{x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≠ t₂}
─────────────────
⟦s1..t₁⟧ ⊆ ⟦≠ t₂⟧
──────────────────────────
⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
────────────────────────────────────⁰
t₁ ≁ t₂ → ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧