¶Union of ≠ t₁ or ≁ t₂
When the "hole" of the non-equivalent constraint and the "pivot" of the incomparable constraint are not comparable, then the "hole" is covered by the incomparable constraint, and the union is therefore always satisfied.
Otherwise, the hole and pivot are comparable, and the non-equivalent constraint subsumes the incomparable constraint.
(≠ t₁) ∨ (≁ t₂) = 𝟙 if t₁ ≁ t₂
= (≠ t₁) otherwise
¶Equationally
⟦≠ t₁⟧ = {x | x ⊈ t₁ ∨ t₁ ⊈ x}
⟦≁ t₂⟧ = {x | x ⊈ t₂ ∧ t₂ ⊈ x}
When t₁ ≁ t₂, we want to show that x ≠ t₁ ∨ x ≁ t₂ is always true. Do that, we'll assume it's not true, and prove false.
[x = t₁ ∧ x ~ t₂]¹
─────────────────
[t₁ ≁ t₂]⁰ x = t₁ ⋮
─────────────────── ⋮
x ≁ t₂ x ~ t₂
───────────────────────
false
───────────────¹
x ≠ t₁ ∨ x ≁ t₂
─────────────────────────
{x | x ≠ t₁ ∨ x ≁ t₂} = 𝟙
───────────────────────────────
{x | x ≠ t₁} ∪ {x | x ≁ t₂} = 𝟙
───────────────────────────────
⟦x ≠ t₁⟧ ∪ ⟦x ≁ t₂⟧ = 𝟙
─────────────────────────────────⁰
t₁ ≁ t₂ → ⟦x ≠ t₁⟧ ∪ ⟦x ≁ t₂⟧ = 𝟙
When t₁ ~ t₂, we want to show that x ≁ t₂ → x ≠ t₁, so that the union is ≠ t₁.
[x = t₁]² [t₁ ⊆ t₂]³ [x ≁ t₂]¹ [x = t₁]² [t₂ ⊆ t₁]³ [x ≁ t₂]¹
──────────────────── ──────── ──────────────────── ────────
x ⊆ t₂ x ⊈ t₂ t₂ ⊈ x t₂ ⊈ x
──────────────────────── ────────────────────────
false false
⋮ [t₁ ~ t₂]⁰ ⋮
⋮ ───────────────── ⋮
⋮ t₁ ⊆ t₂ ∨ t₂ ⊆ t₁ ⋮
────────────────────────────────────────³
false
──────²
x ≠ t₁
───────────────¹
x ≁ t₂ → x ≠ t₁
───────────────────────────
{x | x ≁ t₂} ⊆ {x | x ≠ t₁}
───────────────────
⟦x ≁ t₂⟧ ⊆ ⟦x ≠ t₁⟧
──────────────────────────────
⟦x ≁ t₂⟧ ∪ ⟦x ≠ t₁⟧ = ⟦x ≠ t₁⟧
────────────────────────────────────────⁰
t₁ ~ t₂ → ⟦x ≁ t₂⟧ ∪ ⟦x ≠ t₁⟧ = ⟦x ≠ t₁⟧