nx_term_order.nx

nx_term_order.nx -- Knuth-Bendix Order (KBO) over first-order Terms. Per Vampire-displacement roadmap Phase 1 step 1: KBO is the foundation every saturation prover uses to orient rewrites, pick the smaller half of a critical pair, and prune redundant clauses (forward subsumption, demodulation, tautology deletion all depend on it). Knuth + Bendix 1970. Standard formulation: Given: - weight function w : Symbol -> nx_int - precedence > on symbols (total order) - constant w_0 >= 1 (minimum weight; weight of a variable) Admissibility (KBO is well-founded iff): (A1) for every constant c, w(c) >= w_0 (A2) if f is a unary symbol with w(f) = 0, then f is maximal in > weight(x) = w_0 for variables x weight(f(t1,..,tn)) = w(f) + sum_i weight(t_i) s >_KBO t iff (for every variable x, count(x, s) >= count(x, t)) AND ONE OF: (W1) weight(s) > weight(t) (W2) weight(s) = weight(t) AND (P1) head(s) > head(t) in precedence, (P2) head(s) = head(t) AND args(s) >_lex args(t) Result is a sealed verdict {GT, EQ, LT, INCOMPARABLE}. Bits-up: pure nx_int arithmetic, no f64, no external library. Result-typed for all fallible API. Scale-agnostic via nx_tier.