Strong Normalization for the Safe Fragment of a Minimal Rewrite System: A Triple-Lexicographic Proof and the Termination Conjecture for the Full System

Strong Normalization for the Safe Fragment of a Minimal Rewrite System: A Triple-Lexicographic Proof and the Termination Conjecture for the Full System Moses Rahnama November 24, 2025 Abstract We present a minimal operator-only term rewriting system with seven constructors and eight reduction rules. Our main contribution is a mechanically-verified proof of strong normalization for a guarded fragment using a novel triple-lexicographic measure combining a phase bit, multiset ordering (Dershowitz-Manna), and ordinal ranking. From strong normalization, we derive a certified normalizer with proven totality and soundness. Assuming local confluence (verified through critical pair analysis), Newman’s Lemma yields confluence and therefore unique normal forms for the safe fragment. We establish impossibility results showing that simpler measures, such as additive counters, polynomial interpretations, and single-bit flags, provably fail for rules with term duplication. The work demonstrates fundamental limitations in termination proving for self-referential systems. It connects to classical undecidability results while providing constructive, mechanically-verified proofs, and it states a conjecture on undecidable termination: some terminating operator-only systems have termination that is true but unprovable within a given base theory using internally definable methods. All theorems have been formally verified in a proof assistant. The formal development is available to program committee members and referees upon request for purposes of peer review. 1 Introduction We develop a minimal operator-only rewrite calculus (KO7): the object language contains only constructors and operators with rewrite rules; there are no binders, types, external axioms, or semantic predicates. The rules are the semantics. Our goals are: (i) a clean, duplication-robust proof of strong normalization (SN); (ii) a certified normalizer that always returns a normal form; (iii) (optionally) unique normal forms via Newman’s Lemma under a local-confluence assumption; and (iv) an explicit conjecture that some terminating operator-only systems have termination that is true but unprovable in a given base theory using internally definable methods. Scope. All formal results are established for a guarded safe subrelation. We do not claim a single global measure for the full unguarded relation. Moreover, we exhibit a precise negative: at the root peak eqW a a with κM ( a ) = 0, local join fails in the full relation. Therefore the full relation is not locally confluent at that peak, hence not confluent. The designed remedy is to work in the safe fragment with guarded/context joiners ( § 6). A second conceptual goal is to situate KO7 against results about fixed-target reachability in terminating TRSs. If we define an internal provability predicate by “ t reduces to ⊤ ”, then under SN the set {t|t⇒∗⊤} is decidable by normalization/backtracking. With confluence, decision reduces to normal-form equality. This explains why single-level G¨odel encodings cannot coexist with globally terminating proof search; the right move is stratification. 1 Contributions. (1) A duplication-robust SN proof for KO7 using a triple-lex measure with a multiset (DM) component and an MPO-style head precedence; (2) a total, proved-correct normalizer; (3) a guarded Newman module for the safe relation that yields confluence (hence unique normal forms) from SN + local confluence; (4) a decidability result for reachability under SN; (5) a catalog of impossibility results for additive and polynomial measures under duplication; (6) a formal verification of all results; (7) a conjecture on undecidable termination for operator-only systems within a fixed base theory. Highlights (formalization summary).  SN (SafeStep) via triple lex: Formally proven using a lexicographic measure combining a δ-phase bit, a Dershowitz–Manna multiset rank, and an ordinal.  Certified normalizer: A total and sound normalization function is defined by well-founded recursion.  Newman (SafeStep): Confluence is established via Newman’s Lemma using a verified local confluence property for the safe fragment.  Full Step caveat: We exhibit a specific peak ( eqW a a with κM ( a ) = 0) where local join fails, justifying the restriction to the safe subrelation.  Impossibility results: The failure of simpler additive and polynomial measures is formally witnessed by counterexamples. 2 Background: TRSs, SN, reachability, and Newman We assume standard abstract reduction and term rewriting notions [ 2 , 11 ]. A term is in normal form if no rule applies. A TRS is strongly normalizing (SN) if there are no infinite reductions. A relation is confluent if for any t⇒∗u and t⇒∗v there exists w with u⇒∗w and v⇒∗w . Local confluence requires this only for single-step forks. Newman’s Lemma asserts SN + local confluence ⇒confluence [10], yielding unique normal forms. Fixed-target (“small-term”) reachability in terminating TRSs has well-charted complexity: NP-complete for length-reducing systems (dropping to P under confluence), NExpTime/N2ExpTime for (linear) polynomial interpretations, and PSPACE for KBO-terminating TRSs [ 1 ]. Modularity holds in certain linear, non-collapsing combinations [ 4 ], while even flat non-linear systems exhibit undecidable reachability and confluence [ 9 ]. Termination under duplication typically requires orders beyond plain sizes; a naive size can increase under duplicating rules. The cure is a multiset extension of a base order [6] or (recursive) path orders [5]. 3 The KO7 calculus KO7 is a finite TRS over a small signature (7 constructors) with 8 rules (including a conditional split on eqW). For concreteness we list the rule shapes below. Tiny example (trace consequences). Using the verified normalizer, we observe:  Integrate/delta: integrate(δ t)⇒∗void (verified).  Equality (meta-level consequence under confluence): –If nf(a) = nf(b) then eqW a b ⇒∗void. –Otherwise eqW a b ⇒∗integrate(merge a b). Note: In the safe fragment, confluence ensures these outcomes are unique. Note. We prove SN and Newman-based confluence for the safe fragment. 2 Rule Head Arity Shape Dup? R1 merge 2 merge void t→tNo R2 merge 2 merge tvoid →tNo R3 merge 2 merge t t →tNo R4 rec∆ 3 rec ∆ b s void →bNo R5 rec∆ 3 rec ∆ b s (delta n)→app s(rec ∆ b s n) No R6 integrate 1 integrate (delta t)→void No R7 eqW 2 eqW a a →void No R8 eqW 2 eqW a b →integrate (merge a b) (if a=b) No Table 1: KO7’s 8 rules. Note that R7/R8 provide a complete case split on equality. R3 is collapsing (erases one copy); R5 is non-duplicating. 4 Strong normalization We define a triple-lexicographic measure µ3(t) := (δ-flag(t), κM(t), µord(t)) ordered by the lex product of: (i) a phase bit dropping on the successor recursion; (ii) a multiset of ranks κM (Dershowitz–Manna) with an explicit precedence/status orienting redex > pieces; and (iii) an ordinal payload µord for non-duplicating ties. Ordinal hazards are stated explicitly (right-addition is not strictly monotone; absorption α + β = β requires ω≤β ). In duplicating branches (if extended to broader systems) we would use a compact MPO-style head precedence. Step vs SafeStep (measure unification). For the SafeStep relation we use a single unified triple lex order ( δ, κM, µord ). For the full relation we only provide a disjunctive decrease certificate: each step is covered by either a KO7 lex drop or an MPO triple drop. We do not claim a single global well-founded measure for all full steps. Theorem 1 (Per-step decrease (SafeStep)).For every rule instance t⇒t′ in the guarded SafeStep relation, we have µ3(t′)<Lex µ3(t). Proof idea. By rule head. For collapsing rules (e.g., merge-cancel) we use the multiset component with the chosen precedence so that every RHS piece is strictly smaller than the removed LHS redex in the base order. For rec-succ the δ bit drops (1 → 0). In the formalization, each branch is a one-liner dispatched by a wrapper lemma. DM vs MPO on rules (explicit). For merge-cancel, we use a DM multiset lift over a base order where merge t t strictly dominates t . For eqW, we use a compact MPO-leaning measure where the head precedence orients eqW a b strictly above integrate(merge a b).  Base-order premise (merge-cancel): in merge t t →t , the RHS is strictly smaller than the LHS.  Base-order premise (eqW): in eqW a b →integrate ( merge a b ), the RHS is strictly smaller under head precedence. No-Go for constant bumps on κ(generic duplicator). Lemma 1 (No fixed + k or boolean flag orients a generic duplicator).Let κ be a max-depth-style counter and fix any k∈N . For a duplicating rule of the shape r ( S ) →C [ S, S ](one redex replaced by two occurrences of a subterm S ), there exists an instance where κ ( LHS ) +k = κ ( RHS ) +k , so no strict lex drop occurs. The same holds for a boolean phase flag alone. 3 Proof sketch. Choose S with κ ( S ) ≥ 1 and let base bound the context. Then κ ( LHS ) = base+ 1 while κ ( RHS ) = max ( κ ( C [ S ]) , κ ( C [ S ])) = base+ 1. Adding a fixed k preserves equality; a single flag does not alter the tie. □ Remark 1.In KO7, the successor recursion rule rec ∆ b s ( δ n ) →app s ( rec ∆ b s n ) is nonduplicating in the strict variable sense (it redistributes s and b ), but its orientation relies on the δphase bit (1→0). Duplication stress identity. For any additive counter ρ that counts a single removed redex and sums subpieces, generic duplicators satisfy ρ(after) = ρ(before) −1 + ρ(S), so there is no strict drop when ρ ( S ) ≥ 1. The robust fix uses DM/MPO: replace one element by a multiset of strictly smaller elements (DM), or use RPO/MPO with a precedence/status such that the LHS redex strictly dominates each RHS piece. Corollary 1 (Strong normalization).The guarded relation SafeStep for KO7 is strongly normalizing. Genealogy of failures (why DM/MPO). We record minimal counterpatterns that motivate the multiset/path components:  Pure ordinal (µ) only: shape-blind bounds fail to separate nested δfrom its context.  Additive bumps on κ: ties persist on duplicators (Lemma 1).  Additive counters ρ : by the identity ρ ( after ) = ρ ( before ) − 1 + ρ ( S ) there is no strict drop when ρ(S)≥1. The fix is DM/MPO: ensure each RHS piece is strictly smaller than the removed redex in a base order and lift via a multiset/path extension. 5 A certified normalizer By well-founded recursion on µ3 we define a normalization function. We prove the following properties (separated to avoid overfull lines): (Totality) ∀t∃n. Normalize(t) = n (Soundness) ∀t. normal(Normalize(t)) ∧t⇒∗Normalize(t). These are exposed in the formalization. We make no efficiency claim: worst-case normalization cost follows the termination witness in play (cf. the small-term reachability bounds in [ 1 ]). In confluent systems, decision reduces to one normalization and an equality check. 6 Local confluence and Newman (guarded safe relation) We discharge local confluence by joining the finite set of critical pairs (when present). Combining Cor. 1 with Newman’s Lemma [10] yields: Theorem 2 (Confluence and unique normal forms).If a relation is strongly normalizing and locally confluent, then it is confluent. Hence every term reduces to a unique normal form. 4 Instantiation (SafeStep). Combining Cor. 1 (SN for SafeStep ) with local-join lemmas yields confluence and unique normal forms for the safe fragment by Newman’s Lemma. In contrast, the full relation is not locally confluent at the root peak eqW a a under κM ( a ) = 0; thus full confluence does not hold. The SafeStep relation restricts eqW to cases where arguments are guarded, preventing this divergence. The star-star join proof follows the standard accessibility (Acc) recursion at the source, with a case split over star shapes (“head step + tail”) and composition via transitivity. The module also provides corollaries for uniqueness of normal forms and equality of normalizers under star. Scope and Guarantees (formalization-accurate). We work with a guarded safe subrelation SafeStep for which we prove:  SN (SafeStep). The KO7 triple measure µ3 strictly drops on every SafeStep . This yields acertified normalizer that is total and sound for the safe fragment.  Local Confluence (SafeStep). We provide local-join lemmas per root shape and context wrappers. Newman then yields confluence and unique NFs for the safe fragment.  Full Step per-rule decreases (Hybrid). For each kernel rule, there is a per-step decrease witnessed either by KO7’s δ/κM/µ lex or by an MPO-leaning µ -first triple. A uniform global aggregator for all of Step is left as future work. Critical-pair coverage. The following table covers the safe root configurations with explicit local-join lemmas. This is exhaustive for SafeStep except the reflexive eqW a a peak under κM ( a ) = 0, which we show is not locally joinable at the root. We discharge many eqW cases via guarded/context wrappers. Source Lemma integrate(δ t)localJoin int delta (unique target void) merge void tlocalJoin merge void left (unique target t) merge tvoid localJoin merge void right (unique target t) merge t t localJoin merge tt (unique target t) rec ∆ b s void localJoin rec zero (unique target b) rec ∆ b s (δ n)localJoin rec succ (unique target app s(rec ∆ b s n)) eqW a b, a =blocalJoin eqW ne (unique target integrate(merge a b)) eqW a a, κM(a)=0 not locally joinable at root Guarded variants exclude spurious branches. Contextual wrappers lift root joins to context. δ -guard: definition and decidability. Define the safe-phase predicate by δ-guard ( t ) ⇐⇒ δFlag ( t ) = 0. Here δFlag : Term →N is a structurally recursive function defined on terms in the artifact (tracking split parity), so the predicate is decidable. Facts: δFlag ( eqW a b ) = 0; merge-void rules require δFlag(t) = 0. Tiny δ-flag walk-through (1→0). rec ∆ b s (δ n) app s(rec ∆ b s n) δ-flag drop 5 7 Impossibility results We formally establish the failure of several simpler measure strategies, which necessitate the use of DM multiset orders or MPO. These negative results are verified in the formal development.  Additive bumps fail: No measure of the form κ ( t ) + k strictly decreases on generic duplicating rules.  Bare flags fail: A single boolean flag is insufficient to orient rules that lift depth.  Polynomial interpretations fail: Any polynomial interpretation involving fixed constants requires external arithmetic axioms to “orient” the rule, violating the operator-only constraint. Polynomial Impossibility (The “FruitSystem” Counterexample). We specifically investigate polynomial interpretations of the form M ( t ) ∈N . Consider a system with a constant c and a rule f ( x ) →g ( x, x ). A polynomial measure might assign M ( c ) = k and M ( f ( x )) = M ( x ) + p . For the rule to decrease, we need M ( x ) + p > 2 M ( x ), which implies p>M(x). This cannot hold for all xif M(x) is unbounded. In our formalization, we demonstrate that a polynomial proof for a similar system (isomorphic to KO7) relies on hardcoding specific constants (e.g., M ( void ) = 2) to satisfy inequalities like 2 M ( s ) > M ( s ) + 1. This succeeds only by importing external arithmetic properties (multiplication) and imposing arbitrary values on the operators, violating the principle that the operators’ semantics should be defined solely by their rewrite rules. If the constant is changed (e.g., M ( void ) = 1), the proof collapses. This failure is structurally identical to the difficulty in orienting generic duplicating rules without such external hacks. Internally definable measures. We use a simple contract for internally defined termination measures to structure these negative results: Definition 1 (Internally definable measure).An internally definable measure for a type α consists of ( β, < β, wf, m, ctxMono,piecesLt )where: β is a base order carrier; < β is a well-founded relation with witness wf ; m : α→β is the measure; ctxMono expresses context compatibility; and piecesLt asserts that in each rule instance, every RHS piece is strictly smaller than the removed LHS redex w.r.t. < β. 8 Decidability of Reachability Theorem 3 (Fixed-target reachability).In a strongly normalizing TRS, the set {t|t⇒∗c} for any constant cis decidable via normalization. This connects our work to classical results: if we could encode undecidable properties through reduction to constants, we would violate known theoretical limits. This motivates stratified approaches in proof assistants, where object-level and meta-level reasoning are carefully separated. Assumptions (model). We work with a finite first-order TRS over finite terms. The decision method is: compute a normal form (by SN) and check whether it is ⊤ ; with local confluence, this reduces to one normalization and an equality test. 6 Complexity context. Small-term reachability in terminating TRSs ranges from NP (lengthreducing) to NExpTime/N2ExpTime (polynomial interpretations) and PSPACE (KBO), with confluence lowering the length-reducing class to P [ 1 ]. This situates our “normalize and compare” decision procedure for KO7 within the established landscape. Moreover, decidability can be modular for disjoint unions under left-linearity/non-collapsing assumptions [ 4 ], while termination alone does not guarantee decidability: even flat non-linear TRSs have undecidable reachability/joinability/confluence [9]. 9 Conjecture: TRS Termination Conjecture Conjecture 1 (TRS Termination Conjecture).For every recursively axiomatizable base theory T of arithmetic (e.g., PA), there exists an operator-only TRS R that encodes arithmetic such that R terminates, but the termination of at least one self-referential rule of R is not provable in T. Evidence stems from true but unprovable termination phenomena (Goodstein sequences, hydra battles), which admit TRS encodings whose termination requires proof-theoretic strength beyond PA. This suggests a gap between internally definable ranking functions and the ordinal strength actually needed. Internal method class and base theory. Fix a signature Σ. Let C (Σ) denote internal termination methods assembled from KO7-definable ingredients: simplification orders with fixed precedence/status on Σ (LPO/RPO/MPO), DM-multiset lifts of N -valued ranks, algebraic interpretations, and dependency pairs discharged by these. Choose a base theory T (KO7internal, PRA, or PA) that soundly formalizes C (Σ). The sharpened claim reads: there exists a KO7 rule whose strict decrease is true but not provable in Tusing only methods from C(Σ). 10 Formalization structure The formal verification is implemented in a proof assistant. The project structure separates the kernel definitions, meta-theory proofs, and impossibility results:  Termination proofs: Establishes the per-rule decreases and strong normalization for the safe fragment using the triple-lexicographic measure.  Normalization: Defines the normalization function and proves its totality and soundness.  Confluence: Implements the Newman engine and the star-star join, relying on local join lemmas.  Impossibility results: Contains the verified counterexamples for additive measures and the proofs that simple measures fail under duplication. All claimed results are formally proven without reliance on unproven postulates in the current build. The formal development is available to reviewers under appropriate confidentiality agreements. References References [1] Franz Baader and J”urgen Giesl. On the complexity of the small term reachability problem for terminating trss. In FSCD 2024, volume 299 of LIPIcs, pages 16:1–16:18, 2024. 7 [2] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. [3] Wilfried Buchholz. A new system of proof-theoretic ordinal functions. Annals of Pure and Applied Logic, 32(3):195–207, 1986. [4] Anne-Catherine Caron and Jean-Louis Coquid´e. Decidability of reachability for disjoint union of term rewriting systems. Theoretical Computer Science, 126(1):31–52, 1994. [5] Nachum Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1–2):69–116, 1987. [6] Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, 1979. [7] R. L. Goodstein. On the restricted ordinal theorem. Journal of Symbolic Logic, 9(2):33–41, 1944. [8] Laurence Kirby and Jeff Paris. Accessible independence results for peano arithmetic. Bulletin of the London Mathematical Society, 14(4):285–293, 1982. [9] Isao Mitsuhashi, Masahiro Oyamaguchi, and Florent Jacquemard. The confluence problem for flat trss. In AISC 2006, volume 4120 of LNCS, pages 73–84, 2006. [10] M. H. A. Newman. On theories with a combinatorial definition of “equivalence”. Annals of Mathematics, 43(2):223–243, 1942. [11] Terese. Term Rewriting Systems. Cambridge University Press, 2003. Appendix: Addendum KO7 Rules Table (7 constructors, 8 rules) Rule Head Arity Shape Dup? R1 merge 2 merge void t→tNo R2 merge 2 merge tvoid →tNo R3 merge 2 merge t t →tNo R4 rec∆ 3 rec ∆ b s void →bNo R5 rec∆ 3 rec ∆ b s (delta n)→app s(rec ∆ b s n) No R6 integrate 1 integrate (delta t)→void No R7 eqW 2 eqW a a →void No R8 eqW 2 eqW a b →integrate (merge a b) (if a=b) No Table 2: KO7’s 8 rules. Note that R7/R8 provide a complete case split on equality. R3 is collapsing (erases one copy); R5 is non-duplicating. Triple-lexicographic measure and duplication handling (DM/MPO) We order µ3(t)=(δ-flag(t), κM(t), µord(t)) by lex:  δ-flag: phase bit dropping on the successor recursion branch.  Multiset κM : a Dershowitz–Manna multiset extension over a base precedence/status (or MPO head precedence) orienting redexes strictly above pieces; covers duplicators.  Ordinal µord : resolves non-duplicating ties; right-addition is not strictly monotone; absorption α+β=βneeds ω≤β. Per-rule lemmas show every RHS component is strictly smaller than the removed redex in the base order. 8 Aggregation for κM (union, not sum). We emphasize that κM aggregates via multiset union ( ∪ ), not numeric addition. For duplicating rules, the multiset of piece-weights on the RHS is DM-smaller than the singleton multiset containing the LHS redex weight, yielding a strict drop in the κM component. For non-duplicating rules, κM ties by definitional equality and the ordinal µord resolves the branch. In particular, for unguarded instances of eqW -refl and merge-cancel we use a κ -branch: when κM ( a )  = 0 we obtain a left-lex drop via DM; when κM ( a ) = 0 the κM component ties by rfl and the strict decrease is witnessed in the µord coordinate (right branch of Prod.Lex). Short witness snippets (toy duplication). Toy rule: pair(s x, y)→pair(x, pair(y, y)). DM multiset on sizes. Let S ( x, y ) = size ( pair (s x, y )) = size ( x ) + size ( y ) + 2. Then size ( x ) < S ( x, y ) and size ( y ) < S ( x, y ). Use X = ∅ , Y = {size ( x ) ,size ( y ) } , Z = {S ( x, y ) } to conclude Y <DM Z. MPO triple weight. weight ( pair a b ) = ( headRank ( a ) ,size ( a ) ,size ( b )) with headRank (s ) = 2, else 1. If x is unit/pair then first components decrease (1¡2). If x = s t then tie on 2; the second components satisfy size(t)+1<size(t) + 2. δ-flag phase drop κM(DM/MPO) redex >pieces µord tie-break lex lex Figure 1: Triple-lex measure components. Duplicators decrease via κM ; non-duplicating ties via µord. Newman scope (guarded safe relation) SN + local confluence implies confluence; in the artifact this is instantiated for the safe relation via an Acc-based star–star join. Scope note: all confluence statements and their Newman instantiations are for SafeStep only. Full Step is not locally joinable at root for eqW a a with κM(a) = 0; accordingly we do not claim full-step confluence. Module map The verification logic is distributed across key modules for SN, normalizer, and confluence engine. Local confluence lemmas are proved separately. Note: context closure and local-join lemmas are explicitly instantiated for the SafeStep fragment (SafeStepCtx) rather than the full relation. Per-rule orientation (DM/MPO/δ/µ) Rule Base component Precedence/Status Witness Source merge void left µ(ordinal) — Theorem 4.1 Termination merge void right µ(ordinal) — Theorem 4.2 Termination merge cancel DM on κM(redex >pieces) head precedence Theorem 4.3 Termination rec zero DM on κMrec >pieces Theorem 4.4 Termination rec succ δphase bit (1 →0) — Theorem 4.5 Termination eqW refl MPO (µ-first triple) head precedence Theorem 4.6 Termination eqW diff MPO (µ-first triple) head precedence Theorem 4.7 Termination integrate (delta t) µ(unique target) — Theorem 4.8 Termination toy duplication DM on size s >pair Lemma 7.1 Impossibility toy duplication MPO triple headRank(s) > headRank(pair) Lemma 7.2 Impossibility Table 3: Per-rule orientation summary. Parenthetical aliases: for substitution convenience we expose simp forms alongside the main rec lemmas. 9