¶Intersection of s₁..t₁ and ~ t₂
The intersection of a range and a comparable depends on how the two types are related.
(s₁..t₁) ∧ (≠ t₂) = (s₁..t₁) if 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}
¶Case 1
If s₁ ⊆ t₂ ∧ t₂ ⊆ t₁ (which also holds when s₁ = t₁ = t₂):
⟦(s₁..t₁) ∧ (~ t₂)⟧
= {x | s₁ ⊆ x ∧ x ⊆ t₁} ∩ {x | x ⊆ t₂ ∨ t₂ ⊆ x}
= {x | s₁ ⊆ x ∧ x ⊆ t₁ ∧ (x ⊆ t₂ ∨ t₂ ⊆ x)}
= {x | (s₁ ⊆ x ∧ x ⊆ t₁ ∧ x ⊆ t₂) ∨ (s₁ ⊆ x ∧ x ⊆ t₁ ∧ t₂ ⊆ x)}
= {x | (s₁ ⊆ x ∧ x ⊆ t₁ ∧ x ⊆ t₂) ∨ (s₁ ⊆ x ∧ x ⊆ t₁ ∧ s₁ ⊆ x)}
= {x | (s₁ ⊆ x ∧ x ⊆ t₁ ∧ x ⊆ t₂) ∨ (s₁ ⊆ x ∧ x ⊆ t₁)}
= {x | (s₁ ⊆ x ∧ x ⊆ t₁ ∧ x ⊆ t₁) ∨ (s₁ ⊆ x ∧ x ⊆ t₁)}
= {x | (s₁ ⊆ x ∧ x ⊆ t₁) ∨ (s₁ ⊆ x ∧ x ⊆ t₁)}
= {x | s₁ ⊆ x ∧ x ⊆ t₁}
= ⟦s₁..t₁⟧
¶Case 2
If s₁ ≁ t₂ ∧ t₁ ≁ t₂:
[s₁ ⊆ x ∧ x ⊆ t₁ ∧ x ⊆ t₂]¹ [s₁ ⊆ x ∧ x ⊆ t₁ ∧ t₂ ⊆ x]²
────────────────────────── ──────────────────────────
s₁ ⊆ x x ⊆ t₂ [s₁ ≁ t₂ ∧ t₁ ≁ t₂]⁰ x ⊆ t₁ t₂ ⊆ x
───────────────── ─────────────────────────── ─────────────────
s₁ ⊆ t₂ s₁ ⊈ t₂ t₂ ⊈ t₁ t₂ ⊆ t₁
─────────────────────── ──────────────────────
false false
───────────────────────────¹ ───────────────────────────²
¬(s₁ ⊆ x ∧ x ⊆ t₁ ∧ x ⊆ t₂) ¬(s₁ ⊆ x ∧ x ⊆ t₁ ∧ t₂ ⊆ x)
──────────────────────────────────────────────────────────────
¬(s₁ ⊆ x ∧ x ⊆ t₁ ∧ x ⊆ t₂) ∧ ¬(s₁ ⊆ x ∧ x ⊆ t₁ ∧ t₂ ⊆ x)
──────────────────────────────────────────────────────────
¬((s₁ ⊆ x ∧ x ⊆ t₁ ∧ x ⊆ t₂) ∨ (s₁ ⊆ x ∧ x ⊆ t₁ ∧ t₂ ⊆ x))
──────────────────────────────────────────────────────────
¬(s₁ ⊆ x ∧ x ⊆ t₁ ∧ (x ⊆ t₂ ∨ t₂ ⊆ x))
─────────────────────────────────────────────
{x | s₁ ⊆ x ∧ x ⊆ t₁ ∧ (x ⊆ t₂ ∨ t₂ ⊆ x)} = ∅
─────────────────────────────────────────────────
{x | s₁ ⊆ x ∧ x ⊆ t₁} ∩ {x | x ⊆ t₂ ∨ t₂ ⊆ x} = ∅
─────────────────────────────────────────────────
⟦s₁..t₁⟧ ∩ ⟦~ t₂⟧ = ∅
───────────────────────────────────────────⁰
(s₁ ≁ t₂ ∧ t₁ ≁ t₂) → ⟦s₁..t₁⟧ ∩ ⟦~ t₂⟧ = ∅
¶Otherwise
Otherwise, the two constraints cannot be simplified.