nx_eq_factor.nx

nx_eq_factor.nx -- equality factoring (Bachmair-Ganzinger 1994). Per Vampire-displacement roadmap Phase 2. Standard inference rule in superposition calculus, paired with paramodulation. Required for completeness when an equational saturation fires. Standard formulation: C ∨ s ≃ t ∨ s' ≃ t' (two positive equality literals) σ = mgu(s, s') -------------------------- (C ∨ s ≃ t ∨ t ≄ t')σ Reading: when two equality literals share a unifiable LHS, ONE of them (here s ≃ t) is kept and the OTHER's RHS is asserted DIFFERENT from the kept RHS (t ≄ t'). Future inference may resolve t≄t' against an equality elsewhere; if t and t' really were equal the resolvent is contradicted, otherwise the disequality survives. Ordering side conditions for full Bachmair-Ganzinger soundness are the caller's responsibility (typically checked via KBO/LPO): - s ≃ t is selected or maximal in C - sσ ⊁ tσ - (s ≃ t)σ ⊁ (s' ≃ t')σ API: caller picks the two equality-literal indices i and j; the primitive validates polarity + equality head, unifies the LHS pair, and emits the residual.