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

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.