ch:semi-unification: ch:semi-unification

Problem and result. Represent finite arrow terms, replay ordinary equations under one outer substitution, and replay every inequality under that same outer substitution followed by its own matcher. Report rejection only with the displayed finite-tree certificate; bounded search exhaustion would be UNKNOWN.

Representation. Use algebraic trees for types and finite name–tree lists for substitutions. Store a matcher beside each inequality rather than in a single global field. Simultaneous substitution keeps the chapter equation $R_i(S(M_i))=S(N_i)$ visible and avoids silently composing the two roles.

First complete version. Implement structural type equality, lookup, simultaneous substitution, and both replay clauses. Use the two-record input $$\alpha \doteq \mathsf{Bool},\alpha {⪯}_{\mathsf{su}}\alpha \to \alpha .$$ Replay the equation with outer substitution $[\mathsf{Bool}/\alpha ]$. In a separate family with empty outer substitution, replay the inequality with matcher $[\alpha \to \alpha /\alpha ]$. Print acceptance only after reapplying the outer substitution on both sides and the local matcher on the already outer-substituted left side.

Remaining cases. Add a list of several inequalities, keeping one matcher beside each entry. Recognize the exact syntax $\alpha \to \alpha {⪯}_{\mathsf{su}}\alpha$, derive its symbolic linear node-count certificate, and verify the exact conditions and $k_L\ge k_R$. Then add the opening polymorphic-recursion inequality. A search extension must enumerate finite witnesses fairly and preserve UNKNOWN when its fuel ends.

A failing version. Omitting application of the local matcher leaves the program check- and audit-clean but changes three inequality traces to FAILED and the two aggregate status lines to FAIL. This mutation detects the most important role confusion.

Acceptance test. Require the Bool equation, two inequalities with visibly distinct matchers, the verified symbolic node-count certificate, and the protected polymorphic-recursion replay. Require the exact four-case summary, mutation rejection, and an empty audit.

Mathematical boundary. Finite replay checks supplied certificates. It is not a decision procedure for semi-unification and proves neither the Henglein equivalence nor the Dudenhefner reduction.