nx_demodulation.nx

nx_demodulation.nx -- term rewriting via oriented equations. Per Vampire-displacement roadmap Phase 1 step 3. An oriented equation l = r (with l >_KBO r) is a rewrite rule. Demodulation rewrites every subterm of a target that matches l to the corresponding instance of r, normalizing terms before they re-enter the saturation loop. Together with subsumption, this is the second-largest pruner in Vampire-class provers. Match direction: l is the pattern, target subterm is the term. We walk the target outermost-first; on any successful match we substitute and recurse into the result. Single-pass per call -- callers run it to a fixpoint when full normal form is required. Bits-up nx_int. Result-typed for orientation.