ch:dependent-session-types: dependent sessions

Induct on $A$. Constructors without binders commute with substitution by the induction hypotheses on their immediate components. For a universal, alpha-rename its binder to $y\notin \mathrm{FV}(M)\cup \{x\}$. Then For an existential, use the same fresh $y$ and calculate If the outer binder were also named $x$, substitution would stop at that binder; if it occurred free in $M$, substitution without alpha-renaming would capture it. The fresh $y$ makes both sides use the same capture-avoiding operation.

Let $v_3=\mathsf{cons}a(\mathsf{cons}b(\mathsf{cons}c\mathsf{nil}))$, so $\mathrm{\Psi }⊢v_3:\mathsf{Vec}(E,3)$. Two applications of $\mathrm{\exists }$R derive the provider, first with witness $3$, then with witness $v_3$; dually the client uses $\mathrm{\exists }$L twice. The first communication leaves $$\mathrm{\exists }v:\mathsf{Vec}(E,3).1,$$ and the second leaves $1$. Both cut classifiers are identical after each functional substitution. If $v_2:\mathsf{Vec}(E,2)$ replaces $v_3$, the first step still fixes the continuation index at three. The term premise $\mathrm{\Psi }⊢v_2:\mathsf{Vec}(E,3)$ required by the second $\mathrm{\exists }$R has no derivation, so the trace is rejected before its second communication.

Take an environment endpoint $y:\mathrm{\exists }n:\mathsf{Nat}.1$. Rule $\mathbf{1}$R derives $n:\mathsf{Nat};\cdot ;\cdot ⟹0::z:1$, and $\mathbf{1}$L adds the inert assumption $y:1$. From that premise, rule $\mathrm{\exists }$L derives the live process $$\cdot ;\cdot ;y:\mathrm{\exists }n:\mathsf{Nat}.1⟹y(n).0::z:1.$$ It is well typed, offers $1$, and is live because it contains the input prefix. It is not closed: its linear environment contains $y$. No local reduction applies until a provider sends a witness on $y$. Thus every premise of theorem 102.9 except the empty linear context is represented, and the missing premise is exactly what permits the exposed environment action instead of a reduction.

At index $n=3$, the guard is evaluated before a branch is selected at every unfolding. The successive positive indices $3,2,1$ select the message branch, while is false. Thus If the guard is changed to $n\ge 0$ over the integers, the terminating branch is never reached: at $n=0$ the message branch is selected and the recursive index becomes $-1$, after which every further index still follows the recursive definition under the erroneous guard. The first wrong branch selection therefore occurs at $n=0$.

Choose a fresh functional name $a\notin \mathrm{FV}(M)\cup \mathrm{dom}(\mathrm{\Psi })$. The provider ends in $\mathrm{\exists }$R with $$\mathrm{\Psi }⊢M:\tau ,\mathrm{\Psi };\mathrm{\Gamma };{\mathrm{\Delta }}_1⟹P::x:A[M/a],$$ and the client ends in $\mathrm{\exists }$L with $$\mathrm{\Psi },a:\tau ;\mathrm{\Gamma };{\mathrm{\Delta }}_2,y:A⟹Q::z:C.$$ Before reduction the cut uses the disjoint split ${\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2$. Functional substitution turns the client premise into $$\mathrm{\Psi };\mathrm{\Gamma };{\mathrm{\Delta }}_2,y:A[M/a]⟹Q[M/a]::z:C[M/a].$$ The principal cut therefore reduces to $(\nu y)(P\mid Q[M/a])$, whose provider and client classifiers are both $A[M/a]$. Channel substitution removes $y$ and retains the same union ${\mathrm{\Delta }}_1\uplus {\mathrm{\Delta }}_2$; no linear declaration is duplicated.

The companion prints rejected: expected Vec 2. The failed premise of $\mathrm{\exists }$R is $\mathrm{\Psi }⊢M:\tau$ at $\tau =\mathsf{Vec}(E,2)$. Its length-one witness derives only $\mathrm{\Psi }⊢w_1:\mathsf{Vec}(E,1)$, so the required premise cannot be constructed. This finite rejection does not establish theorem 102.8: that theorem also assumes that every linear declaration occurs in exactly one premise of each multiplicative rule, a property of complete derivations rather than of one execution trace.

Use For $n=2$, transmit the canonical proof , then $\mathsf{fzero}:\mathsf{Fin}(2)$. Successive substitutions leave , then $\mathrm{\exists }i:\mathsf{Fin}(2).1$, then $1$. For a rejected trace, first transmit $1$ but next supply . The second $\mathrm{\exists }$R requires a term of type , whereas $p_2$ has type ; conversion cannot identify the two indices. Alternatively, a later $i:\mathsf{Fin}(2)$ fails the required $\mathsf{Fin}(1)$ premise. Proof irrelevance would identify proofs already inhabiting one proposition; it would not convert into . Adding it changes equality and requires a separate preservation and erasure argument.