¶Intersection of ≁ t₁ and ~ t₂
(≁ t₁) ∧ (~ t₂) = ∅ if t₁ = t₂
= (≠ t₁) ∧ (~ t₂) otherwise
¶Equationally
¶Case 1
If t₁ = t₂:
⟦(≁ t₁) ∧ (~ t₂)⟧
= {x | x ⊈ t₁ ∧ t₁ ⊈ x} ∩ {x | x ⊆ t₂ ∨ t₂ ⊆ x}
= {x | x ⊈ t₁ ∧ t₁ ⊈ x ∧ (x ⊆ t₂ ∨ t₂ ⊆ x)}
= {x | (x ⊈ t₁ ∧ t₁ ⊈ x ∧ x ⊆ t₂) ∨ (x ⊈ t₁ ∧ t₁ ⊈ x ∧ t₂ ⊆ x)}
= {x | (x ⊈ t₁ ∧ t₁ ⊈ x ∧ x ⊆ t₁) ∨ (x ⊈ t₁ ∧ t₁ ⊈ x ∧ t₁ ⊆ x)}
= {x | (false) ∨ (false)}
= {x | false}
= ∅
¶Otherwise
Otherwise, the two constraints cannot be simplified.