nx_lpo.nx

nx_lpo.nx -- Lexicographic Path Ordering (LPO). Per Vampire-displacement roadmap Phase 2. Sibling to KBO -- both well-founded simplification orders on first-order terms. LPO is purely structural: no symbol weights, just a total precedence on symbols. Useful when KBO can't be admissibly weighted (e.g. theories with many constants where all weights tied to w_0). Kamin-Levy 1980 standard formulation: s >_LPO t iff one of: (LPO1) t is a proper subterm of s (LPO2) s = f(s_1..s_n), t = g(t_1..t_m), f > g in precedence, and s >_LPO t_j for every j in 1..m (LPO3) s = f(s_1..s_n), t = f(t_1..t_n) (same head, same arity), (s_1..s_n) >_LPO_lex (t_1..t_n) at the first differing pair, and s >_LPO t_j for every j after that index Sealed verdict {GT, EQ, LT, INCOMP}. Reuses KboState's precedence + arity fields -- the precedence concept is identical across KBO and LPO, so two stores would just be redundant. weights field is ignored by LPO.