ch:ordered-lambek: ch:ordered-lambek

Apply Prod-L twice to the antecedent of the first sequent. Its remaining premise is supplied by $$\frac{\begin{array}{c}A\Rightarrow A\\ {\displaystyle \frac{\begin{array}{c}B\Rightarrow B\\ C\Rightarrow C\end{array}}{B,C\Rightarrow B\cdot C}}\mathrm{Prod}-\mathrm{R}\end{array}}{A,B,C\Rightarrow A\cdot (B\cdot C)}\mathrm{Prod}-\mathrm{R}.$$ The marked splits are $A\mid B,C$ and then $B\mid C$. Reapplying Prod-L first to $A\cdot B$, then to $(A\cdot B)\cdot C$, gives the requested first derivation.

For the reverse direction, expand the antecedent by two uses of Prod-L. Use $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}A\Rightarrow A\\ B\Rightarrow B\end{array}}{A,B\Rightarrow A\cdot B}}\mathrm{Prod}-\mathrm{R}\\ C\Rightarrow C\end{array}}{A,B,C\Rightarrow (A\cdot B)\cdot C}\mathrm{Prod}-\mathrm{R}.$$ Here the splits are $A,B\mid C$ and then $A\mid B$. The two outer Prod-L steps reconstruct $A\cdot (B\cdot C)$ on the left. No formula equality between the two associations was used.

Only the input word $p,q,r$ succeeds. Its derivation ends with the split $p\mid q,r$, followed in the right premise by $q\mid r$: $$\frac{\begin{array}{c}p\Rightarrow p\\ {\displaystyle \frac{\begin{array}{c}q\Rightarrow q\\ r\Rightarrow r\end{array}}{q,r\Rightarrow q\cdot r}}\mathrm{Prod}-\mathrm{R}\end{array}}{p,q,r\Rightarrow p\cdot (q\cdot r)}\mathrm{Prod}-\mathrm{R}.$$ For every derivable final Prod-R, its left premise has atomic succedent $p$. The atomic last-rule lemma forces that premise’s prefix to be exactly the one-letter word $p$. In the words $q,p,r$, $q,r,p$, $r,p,q$, and $r,q,p$, none of the four possible prefixes is that word, so every final split already fails on its left premise. In the remaining word $p,r,q$, the only possible outer split is $p\mid r,q$. The right premise would be $r,q\Rightarrow q\cdot r$; its middle split asks for $r\Rightarrow q$ and $q\Rightarrow r$, while either outer split asks an empty context to derive an atom. All three fail by the same lemma.

Given $\mathcal{D}:\mathrm{\Gamma },p\Rightarrow q$, one application of Slash-R gives $\mathrm{\Gamma }\Rightarrow q/p$. Conversely, identities and Slash-L give the application derivation $$\frac{\begin{array}{c}p\Rightarrow p\\ q\Rightarrow q\end{array}}{q/p,p\Rightarrow q}\mathrm{Slash}-\mathrm{L}.$$ If $\mathcal{E}:\mathrm{\Gamma }\Rightarrow q/p$, cut $\mathcal{E}$ into the marked first antecedent occurrence $q/p$ in this derivation. Ordered cut has conclusion $\mathrm{\Gamma },p\Rightarrow q$. Cut elimination replaces the cut by a cut-free derivation of that same sequent. The block $\mathrm{\Gamma }$ remains before $p$; no exchange has occurred.

Starting with $\mathcal{D}:\mathrm{\Gamma },A,B\Rightarrow C$, first abstract the final $B$, then the final $A$: $$\frac{{\displaystyle \frac{\mathcal{D}:\mathrm{\Gamma },A,B\Rightarrow C}{\mathrm{\Gamma },A\Rightarrow C/B}}\mathrm{Slash}-\mathrm{R}}{\mathrm{\Gamma }\Rightarrow (C/B)/A}\mathrm{Slash}-\mathrm{R}.$$ For the other conclusion, apply Prod-L and then Slash-R: $$\frac{{\displaystyle \frac{\mathcal{D}:\mathrm{\Gamma },A,B\Rightarrow C}{\mathrm{\Gamma },A\cdot B\Rightarrow C}}\mathrm{Prod}-\mathrm{L}}{\mathrm{\Gamma }\Rightarrow C/(A\cdot B)}\mathrm{Slash}-\mathrm{R}.$$ The rule Bslash-R would instead require $A\cdot B,\mathrm{\Gamma }\Rightarrow C$. That premise follows by Prod-L from $A,B,\mathrm{\Gamma }\Rightarrow C$, not from the given word $\mathrm{\Gamma },A,B$; moving the product across $\mathrm{\Gamma }$ would be exchange.

At the root, Id is inapplicable, the atomic succedent supplies no right candidate, and there is no product antecedent. The first residual occurrence is $p\mathrm{\backslash }q$. With the prefix split $ϵ\mid p$, Bslash-L asks for $p\Rightarrow p$ and $q,q\mathrm{\backslash }r\Rightarrow r$. The first closes by identity. At the second premise, identity and right rules are again inapplicable; the first residual candidate uses $q\mathrm{\backslash }r$ with split $ϵ\mid q$, producing two identities. Thus no failed split precedes the first successful branch under the stipulated enumeration. The branch is $$\frac{\begin{array}{c}p\Rightarrow p\\ {\displaystyle \frac{\begin{array}{c}q\Rightarrow q\\ r\Rightarrow r\end{array}}{q,q\mathrm{\backslash }r\Rightarrow r}}\mathrm{Bslash}-\mathrm{L}\end{array}}{p,p\mathrm{\backslash }q,q\mathrm{\backslash }r\Rightarrow r}\mathrm{Bslash}-\mathrm{L}.$$ Atoms have size (1), so each residual has size (3). The root weight is $1+1+3+3=8$. The continuation has weight $1+1+3=5$, and every identity node has weight $1+1=2$. Hence the longest branch has weights ; the other root premise gives .

Write the two final inferences as $$\mathcal{D}=\frac{\begin{array}{c}{\mathcal{D}}_1:{\mathrm{\Gamma }}_1\Rightarrow A\\ {\mathcal{D}}_2:{\mathrm{\Gamma }}_2\Rightarrow B\end{array}}{{\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2\Rightarrow A\cdot B}\mathrm{Prod}-\mathrm{R}.$$ The right derivation ends as $$\mathcal{E}=\frac{{\mathcal{E}}_0:\mathrm{\Delta },A,B,\mathrm{\Theta }\Rightarrow C}{\mathrm{\Delta },A\cdot B,\mathrm{\Theta }\Rightarrow C}\mathrm{Prod}-\mathrm{L}.$$ Cutting their conclusions gives $\mathrm{\Delta },{\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2,\mathrm{\Theta }\Rightarrow C$. Replace that cut by two ordered cuts: first cut ${\mathcal{D}}_2$ for the marked $B$ in ${\mathcal{E}}_0$, obtaining $\mathrm{\Delta },A,{\mathrm{\Gamma }}_2,\mathrm{\Theta }\Rightarrow C$; then cut ${\mathcal{D}}_1$ for the marked $A$. The resulting context is exactly $\mathrm{\Delta },{\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2,\mathrm{\Theta }$. Since each new cut rank is strictly smaller in its first lexicographic component, independently of its height component. These are the two required strict inequalities.

The principal pair has premises $${\mathcal{D}}_0:A,\mathrm{\Gamma }\Rightarrow B,{\mathcal{E}}_1:\mathrm{\Sigma }\Rightarrow A,{\mathcal{E}}_2:\mathrm{\Delta },B,\mathrm{\Theta }\Rightarrow C,$$ where Bslash-R concludes $\mathrm{\Gamma }\Rightarrow A\mathrm{\backslash }B$ and Bslash-L concludes $$\mathrm{\Delta },\mathrm{\Sigma },A\mathrm{\backslash }B,\mathrm{\Theta }\Rightarrow C.$$ First cut ${\mathcal{E}}_1$ for the initial $A$ in ${\mathcal{D}}_0$, obtaining $\mathrm{\Sigma },\mathrm{\Gamma }\Rightarrow B$. Then cut this derivation for $B$ in ${\mathcal{E}}_2$. The final sequent is $$\mathrm{\Delta },\mathrm{\Sigma },\mathrm{\Gamma },\mathrm{\Theta }\Rightarrow C.$$ The two cut formulas are $A$ and $B$, and both satisfy . Their order is forced: the argument block $\mathrm{\Sigma }$ replaces the left argument $A$, so it remains before $\mathrm{\Gamma }$; the second cut inserts that whole block after $\mathrm{\Delta }$.

Assign $$\text{Ada}:\mathsf{a},\text{sends}:((\mathsf{a}\mathrm{\backslash }\mathsf{s})/\mathsf{m})/\mathsf{b},\text{Bert}:\mathsf{b},\text{mail}:\mathsf{m}.$$ The three applications, from the inside out, are $$\mathsf{a},\mathsf{a}\mathrm{\backslash }\mathsf{s}\Rightarrow \mathsf{s},$$ by Bslash-L and two identities, $$\mathsf{a},(\mathsf{a}\mathrm{\backslash }\mathsf{s})/\mathsf{m},\mathsf{m}\Rightarrow \mathsf{s},$$ by Slash-L using the preceding sequent as continuation, and finally $$\mathsf{a},((\mathsf{a}\mathrm{\backslash }\mathsf{s})/\mathsf{m})/\mathsf{b},\mathsf{b},\mathsf{m}\Rightarrow \mathsf{s},$$ by Slash-L, using $\mathsf{b}\Rightarrow \mathsf{b}$ as argument and the preceding sequent as continuation. This is the required parse.

There is only one compound formula in each swapped word, so a cut-free proof with atomic succedent must eventually select that formula by Slash-L. After swapping Ada and sends, the suffix to the right of the verb begins with $\mathsf{a}$, so no initial argument block is the one-letter word $\mathsf{b}$. After swapping sends and Bert, the verb’s suffix is $\mathsf{m}$, again not $\mathsf{b}$. After swapping Bert and mail, the suffix is $\mathsf{m},\mathsf{b}$, whose prefixes are $ϵ$, $\mathsf{m}$, and $\mathsf{m},\mathsf{b}$, none of which derives the atom $\mathsf{b}$. The atomic last-rule lemma rejects the argument premise in all three cases.

Cut elimination and two Prod-L inversions expose the antecedent frontier $A,B,C$. Every ordered rule preserves that left-to-right atomic frontier, whereas the succedent has frontier $A,C,B$. Hence no cut-free ordered derivation exists.

With exchange, derive $A,C\Rightarrow A\cdot C$ by identities and Prod-R, combine it with $B\Rightarrow B$, and obtain $A,C,B\Rightarrow (A\cdot C)\cdot B$. One Ex crosses $B$ and $C$, yielding the premise with frontier $A,B,C$; two Prod-L steps reconstruct $A\cdot (B\cdot C)$. The earlier proposition exchanges two whole product factors. It does not by itself expose the nested factors or supply these product rules.

Read products of crossings from left to right and label the input order $123$. The first route gives $$123\stackrel{{\sigma }_1}{\to }213\stackrel{{\sigma }_2}{\to }231\stackrel{{\sigma }_1}{\to }321,$$ while the second gives $$123\stackrel{{\sigma }_2}{\to }132\stackrel{{\sigma }_1}{\to }312\stackrel{{\sigma }_2}{\to }321.$$ Thus both routes have the same source and target permutation. The braid equation declares these two three-crossing proofs equal. Applying ${\sigma }_i$ twice also returns the labels to their original order, but that permutation calculation does not identify the resulting two-crossing proof with the identity proof. The additional equation ${\sigma }_i^2=\mathsf{id}$ is exactly the symmetric, not braided, quotient.