ch:ordered-lambek: ch:ordered-lambek
Problem, result, and invariant. Implement deterministic backward search for the cut-free ordered calculus. The concrete result is six Boolean oracle lines and an all-pass summary. The cases establish product association, reject atomic exchange, check residuation and the residual chain, and accept the distinct-category sentence while rejecting each single adjacent swap. The invariant is that every recursive sequent preserves the input context as a word: a rule may split a contiguous interval, but it never permutes formula occurrences.
Representation. Represent a context as a word of formulas and enumerate every legal contiguous split in left-to-right order. A multiset representation would reuse commutative search machinery, but would make the exchange counterexample impossible to state and would invalidate the Lambek rules.
First complete version. Implement identity and product right. Enumerate a split
Remaining cases. Add the two residual introductions. Then scan antecedent occurrences from left to right, dispatching to product left or the matching residual-left split; for a backslash split enumerate the fixed prefix first, and for a slash split enumerate the argument block first. Run product association and atomic exchange first, then the residuation pair, residual chain, sentence, and the three adjacent swaps.
A failing version. Reverse the two premise blocks of product right. The program still typechecks and audits cleanly, but either product association or an exchange-sensitive oracle changes, exposing the illicit permutation.
Acceptance test. Run all four commands in appendix E. Require the exact six-case summary, failure of the reversed-block mutation, and audit output [].
Mathematical boundary. The bounded run illustrates deterministic enumeration of cut-free rules. Its fuel is an implementation totality witness, not the strictly decreasing sequent weight of lemma 38.12. It does not prove cut admissibility, residuation, search completeness, termination, or complexity.