Rewrite-to-normal-form under a set of ground NCPO-LNF-oriented equations, restricted to rewrites that produce no variable bindings.

The ground restriction

An equation is admitted as a rewrite rule only when neither side mentions a free variable (ground?/1). Equations carrying rigid γ-variables are still recorded on the branch — ShotTx.Prover.Branch.model_certain?/2 consults them, and the Leibniz/extensional α-expansion still fires — but they never rewrite anything.

The reason is that rewriting with such an equation destroys the very literal pair the branch needs in order to close. In a free-variable tableau a branch closes when the ContradictionAgent finds one global substitution making some literal pair complementary; both literals must therefore survive, and stay syntactically distinct, until the CSP runs.

The surjective Cantor theorem is the sharp case. Its negation yields c (d Y) = Y with Y rigid, whose left side is a primitive η-expansion, so head rewriting turns every occurrence of c (d Y) … into Y …. The branch that should hold the pair {c (d Y) X, Y X} collapses to {Y X} and there is nothing left to close — the refutation needs those two to become contradictory under [λx. ¬(c x x) / Y], which is exactly what the rewrite pre-empts. The rewrite is sound; it is simply backwards for a refutation, because the equation is the hypothesis being contradicted rather than a fact to normalise with. With the restriction in place the theorem closes in 16 steps and one CSP call.

Ground equations have the opposite effect: they create clashes. A branch holding a, ¬b and b = a closes only because ¬b normalises to ¬a. That is the case this module exists to serve, and it is unaffected.

The variable-binding restriction (rigid tableau architecture)

ShotTx maintains a rigid-variable discipline: every branch-level rule is forbidden from committing to a value for any free variable. Free variables in branch formulas — γ-instantiation placeholders (X_γ) and unification variables — must be reconciled globally across sibling branches by ShotTx.Prover.ContradictionAgent, which runs a CSP over all recorded clash options and finds a single substitution satisfying every open branch's rigid-unification requirement. If any branch-level rule locally committed to X_γ ↦ t, it could:

• Close a branch using a σ inconsistent with the σ CA eventually chooses (unsoundness), or
• Force CA to solve a strictly harder problem because the local σ pre-emptively constrained the search (loss of completeness).

Neither is acceptable. This module therefore admits only rewrites whose matcher σ is the empty substitution — i.e. the equation LHS must be structurally identical (memoized term-id equal) to the target subterm. No ShotUn.unify call, no σ, no commitment.

Head-position rewriting via primitive η-expansion equations (λv̄. h(v̄) = rhs) is also binding-free: it structurally matches the head declaration h and applies rhs to the existing arguments via TF.fold_apply!. No free-variable substitution occurs.

What this rules out

The classical paramodulation case where equation f(X) = a rewrites a subterm f(sk_b) via matcher σ = {X ↦ sk_b} is not performed here — binding X (a γ-variable from the equation's ∀-quantifier) is a local commitment to X's value on this branch. Users get such rewrites only after γ produces the necessary instance and the resulting concrete equation is added to branch.equations, or by the Leibniz/extensional α-expansion — never as a shortcut by this module.

Requirements this satisfies

• Soundness. Every rewrite replaces L[s] with L[t] given s = t ∈ equations and s structurally identical to a subterm of L. Substitutivity of equality; no σ involved.
• No variable commitment. By construction — σ = ∅ throughout. The branch's residual free variables are unchanged.
• Termination. Every step is gated by strict_gt?(s, t, order) (the paper's NCPO). By Theorem 2 of Niederhauser & Middeldorp (2025), a chain of such steps is dominated by a well-founded CPO⁺ chain; no infinite descent.
• Determinism per session. Term-id equality and equation-map iteration order are both deterministic.

Requirements this does not satisfy

• Confluence. Not pursued (would require Knuth-Bendix completion, out of scope).
• Refutational completeness for equational reasoning. By design — the Leibniz/extensional α-expansion is the complete fallback. Demodulation is a canonicalization shortcut for the binding-free fragment.

The connective restriction

An equation with a connective application on either side — (a ∧ b) = C, ⊤ = (⊥ ∧ ⊥) — is not a rewrite rule either. It is a propositional equivalence, which :iff_o expansion decides completely; using it to rewrite instead replaces a formula the tableau can still decompose by an opaque atom, and the propositional content is gone before classification sees it.

:rename abbreviates a ∧ b as a fresh C and records (a ∧ b) = C, so an :instantiate child choosing a := ⊤, b := ⊤, C := ⊥ holds its own refutation as (⊤ ∧ ⊤) = ⊥ — and rewrote it, by the very equation whose consequences it was checking, to the vacuous C = ⊥. Without simplification: :deep to evaluate ⊤ ∧ ⊤ the branch then saturated, and its literals were reported as a countermodel for a theorem.

Atoms are unaffected: b = a still rewrites ¬b to ¬a.