¶Intersection of s₁..t₁ and ≠ t₂
The intersection of a range and a non-equivalent depends on how the two types are related.
(s₁..t₁) ∧ (≠ t₂) = ∅ if s₁ = t₁ = t₂
= (s₁..t₁) if s₁ ⊈ t₂ ∨ t₂ ⊈ t₁
= (s₁..t₁) ∧ (≠ t₂) otherwise
¶Equationally
⟦s₁..t₁⟧ = {x | s₁ ⊆ x ∧ x ⊆ t₁}
⟦≠ t₂⟧ = {x | x ⊈ t₂ ∨ t₂ ⊈ x}
¶Case 1
If s₁ = t₁, then the range constraint s₁..t₁ is actually an equivalence constraint = s₁; if also s₁ = t₂, then it's intuitive that the constraints should conflict with each other.
⟦(s..s) ∧ (≠ s)⟧
= {x | s ⊆ x ∧ x ⊆ s} ∩ {x | x ⊈ s ∨ s ⊈ x}
= {x | (s ⊆ x ∧ x ⊆ s) ∧ (x ⊈ s ∨ s ⊈ x)}
= {x | (s ⊆ x ∧ x ⊆ s ∧ x ⊈ s) ∨ (s ⊆ x ∧ x ⊆ s ∧ s ⊈ x)}
= {x | (s ⊆ x ∧ false) ∨ (false ∧ x ⊆ s)}
= {x | false ∨ false}
= {x | false}
= ∅
¶Case 2
If s₁ ⊈ t₂ ∨ t₂ ⊈ t₁:
[s₁ ⊆ x ∧ x ⊆ t₁]¹
─────────────────
[x = t₂]² s₁ ⊆ x x ⊆ t₁ [x = t₂]²
───────────────── ─────────────────
[s₁ ⊈ t₂]³ s₁ ⊆ t₂ t₂ ⊆ t₁ [t₂ ⊈ t₁]³
─────────────────────── ────────────────────────
false false
⋮ ⋮
⋮ [s₁ ⊈ t₂ ∨ t₂ ⊈ t₁]⁰ ⋮
───────────────────────────────────────────³
false
───────²
x ≠ t₂
──────────────────────────¹
(s₁ ⊆ x ∧ x ⊆ t₁) → x ≠ t₂
────────────────────────────────────
{x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≠ t₂}
─────────────────
⟦s₁..t₁⟧ ⊆ ⟦≠ t₂⟧
────────────────────────────
⟦s₁..t₁⟧ ∩ ⟦≠ t₂⟧ = ⟦s₁..t₁⟧
──────────────────────────────────────────────────⁰
(s₁ ⊈ t₂ ∨ t₂ ⊈ t₁) → ⟦s₁..t₁⟧ ∩ ⟦≠ t₂⟧ = ⟦s₁..t₁⟧
¶Otherwise
Otherwise, the two constraints cannot be simplified.