ch:erasure-execution: ch:erasure-execution

Rule Rel-Var gives $\mathrm{\Gamma }⊢y\mathsf{runtime}$. In $\mathrm{\Gamma },z^{\mathsf{runtime}}:\mathbf{2}$, a second instance gives $z\mathsf{runtime}$; hence Rel-Lam-R derives runtime relevance of the displayed abstraction. Rule Rel-App-R applied to those two premises derives runtime relevance of the application.

Suppose the Boolean eliminator had a runtime-relevance derivation. Inversion leaves only Rel-Bool-Elim, whose scrutinee premise is $\mathrm{\Gamma }⊢x\mathsf{runtime}$. Inversion of a runtime judgment for a variable leaves Rel-Var, but $\mathrm{\Gamma }$ contains $x^{\mathsf{erased}}:\mathbf{2}$, not a runtime-marked binding. Thus the scrutinee premise is missing. Rule Rel-Erased cannot repair it because its conclusion is the erased judgment.

The runtime-field list is $\mathsf{run}(\mathsf{pack})=(2)$, so $$|\mathsf{pack}(\mathsf{suc}\mathsf{0},\mathsf{tt})|=C_{\mathsf{pack}}(C_{\mathsf{tt}}).$$ The source branch erases to $$C_{\mathsf{pack}}(b)\Rightarrow C_{\mathsf{0}}.$$ The erased index binder $i$ has no target position. The Boolean field is a retained constructor field, so it contributes the binder $b$ even though the independent branch-use mark is erased and $b$ does not occur in the body. Deleting that binder would give the branch arity zero while the tag has arity one, violating representation well-formedness and preventing E-Case from installing the constructor payload.

Source substitution gives $e[\mathsf{tt}/x]=(\mathsf{tt},{\mathsf{refl}}_{\mathsf{tt}})$, and therefore $$|e[\mathsf{tt}/x]|=C_{\mathsf{pair}}(C_{\mathsf{tt}},C_{\mathsf{refl}}).$$ On the other side, $$|e|[|\mathsf{tt}|/x]=C_{\mathsf{pair}}(x,C_{\mathsf{refl}})[C_{\mathsf{tt}}/x]=C_{\mathsf{pair}}(C_{\mathsf{tt}},C_{\mathsf{refl}}).$$ The reflexivity clause emits the nullary tag $C_{\mathsf{refl}}$; its endpoint is a source annotation and contributes no target variable.

Erasing the element type, both lengths, and predecessor indices leaves the closure $|\mathsf{append}|=\mathsf{clos}(\mathsf{append},\cdot )$ and the two runtime arguments. Abbreviate $p=C_{\mathsf{vcons}}(a,C_{\mathsf{vnil}})$ and $q=C_{\mathsf{vcons}}(b,C_{\mathsf{vnil}})$. First derive $${\mathcal{D}}_0:\mathsf{call}(|\mathsf{append}|,C_{\mathsf{vnil}},q)\Downarrow q.$$ Its outer rule is E-Call: E-Val supplies the closure and both arguments, while its body premise is an E-Case derivation whose scrutinee and selected $C_{\mathsf{vnil}}$ branch both use E-Val. The complete call is the derivation $$\mathsf{call}(|\mathsf{append}|,p,q)\Downarrow C_{\mathsf{vcons}}(a,q).$$ Its outer E-Call again evaluates the closure and arguments by E-Val. The body premise uses E-Case to select the $C_{\mathsf{vcons}}$ branch. That branch uses E-Con, with E-Val for $a$ and ${\mathcal{D}}_0$ for the recursive field. Hence the target constructor tree is $C_{\mathsf{vcons}}(a,C_{\mathsf{vcons}}(b,C_{\mathsf{vnil}}))$, and both case selections inspect only retained vector tags.

Put $$q_0=C_{\mathsf{stream}}(\mathsf{clos}(h_{\ast },C_{\mathsf{0}}),\mathsf{clos}(t_{\ast },C_{\mathsf{0}})).$$ For the head word, Obs-Head forces $\mathsf{clos}(h_{\ast },C_{\mathsf{0}})$; its E-Call body evaluates to $C_{\mathsf{0}}$. Thus $\mathsf{Obs}(q_0,\mathsf{head},C_{\mathsf{0}})$. For the tail word, Obs-Tail first forces $\mathsf{clos}(t_{\ast },C_{\mathsf{0}})$. Its E-Call derivation evaluates the transition once and returns $$q_1=C_{\mathsf{stream}}(\mathsf{clos}(h_{\ast },C_{\mathsf{suc}}(C_{\mathsf{0}})),\mathsf{clos}(t_{\ast },C_{\mathsf{suc}}(C_{\mathsf{0}}))).$$ The remaining Obs-Head premise forces the head closure of $q_1$, whose E-Call result is $C_{\mathsf{suc}}(C_{\mathsf{0}})$. These premises derive the second requested observation.

The four index-erasure clauses give $$(\mathrm{\forall }{i}^{\mathbb{N}}.\mathsf{Vec}A\{i\}\to \mathbb{N}{)}^{\circ }=\mathsf{List}A\to \mathbb{N}.$$ The outer index-polymorphic binder disappears, and the index abstraction and application inside $\mathsf{Vec}A\{i\}$ disappear. The Curry term inhabiting the type is unchanged.

The constructor clauses are $$\mathsf{vnil}\mathcal{R}{C}_{\mathsf{vnil}},\frac{a\mathcal{R}{a}^{\prime }xs\mathcal{R}x{s}^{\prime }}{\mathsf{vcons}(n,a,xs)\mathcal{R}{C}_{\mathsf{vcons}}(a^{\prime },x{s}^{\prime })}.$$ For a source constructor evaluation, apply the induction hypothesis to every runtime field. The erased index $n$ produces no target field, so the target forms the declared arity-two block and the second displayed relation applies. For a recursive branch body $e$, retained bindings satisfy $|e[a/x,xs/y]|=|e|[a^{\prime }/x,x{s}^{\prime }/y]$ by two instances of lemma 126.11; substitution for the erased predecessor index disappears by its erased clause. The target therefore selects the matching constructor branch and preserves $\mathcal{R}$.

Let $b={\lambda }^{\mathsf{erased}}x:\mathbf{2}.\mathsf{if}x\mathsf{then}0\mathsf{else}1$. Then $b\mathsf{tt}\Downarrow 0$ and $b\mathsf{ff}\Downarrow 1$. Under the unsafe erasure clauses, both applications erase their argument and abstraction, so both yield the same phrase $|\mathsf{if}x\mathsf{then}0\mathsf{else}1|$. The phrase is open because the erased binder supplies no target $x$, already violating target well-formedness. Any deterministic repair that closes the phrase has one outcome, and therefore cannot relate simultaneously to the distinct canonical source values zero and one. Runtime relevance rejects $b$ before this contradiction arises.