Declaration processing, copatterns, and erasure

Signed positivity and generated induction

For the families $\mathcal{I}$ of one mutual component, direct occurrences pass only at positive sign with an open ancestry flag. Function domains reverse sign and block recursive occurrences: $$\begin{array}{c}\frac{D\in \mathcal{I}ϵ=+\delta =\mathsf{open}\mathcal{I}\cap \mathrm{Fam}(\overrightarrow{A})=\varnothing }{\mathcal{I};ϵ;\delta ⊢D\overrightarrow{A}\mathsf{pos}},\\ \frac{\mathcal{I};-ϵ;\mathsf{blocked}⊢A\mathsf{pos}\mathcal{I};ϵ;\delta ⊢B\mathsf{pos}}{\mathcal{I};ϵ;\delta ⊢\prod _{x:A}B\mathsf{pos}}.\end{array}$$ An external type-level application $H\overrightarrow{a}$, including a local type-family variable or a family accepted earlier, passes at either sign exactly when its head and arguments are block-family-free; a covariant occurrence such as $\mathsf{List}(D)$ is positive but needs an $\mathsf{All}$ combinator the target does not have. Identity ${\mathsf{Id}}_B(u,v)$ and primitive $\mathsf{Vec}(B,n)$ pass exactly when all displayed type and term arguments are block-family-free. A type-level eliminator or projection headed by ${\mathsf{ind}}_{\mathbf{2}}$, ${\mathsf{ind}}_{\mathbb{N}}$, $\mathsf{J}$, $\mathsf{vind}$, ${\mathsf{pr}}_1$, or ${\mathsf{pr}}_2$ passes exactly when all its immediate subterms are block-family-free; the checker does not reduce that head. A strict lift passes when its argument passes at the same state. The Kappa companion of chapter 122 implements only the five-node subgrammar through external-head application, not these identity, vector, opaque-elimination, or lift clauses.

Every accepted binder $x:A$ contributes the hypothesis type. For a pair type $\sum _{y:B}{A}^{\prime }$, choose $w\notin \mathrm{FV}(B)\cup \mathrm{FV}(A^{\prime })\cup \mathrm{FV}(\overrightarrow{P})\cup \{x,y\}$, and put ${\sigma }_x:=[{\pi }_{1}x/y,{\pi }_{2}x/w]$: so a field of type $\mathbb{N}\to D$ receives $(y:\mathbb{N})\to P_D(xy)$ rather than nothing. The $\mathrm{\Pi }$ clause is legitimate only because $B$ was checked at negative sign, hence cannot mention the block.

The computation rule also needs a generated term of that type. With the simultaneous eliminators in scope, define The family-free clause takes precedence. The nonpositive-family-free lemma ensures that the recursive calls in the function clause are made only beneath an accepted family-free domain.

Strict positivity is a premise of Block-I, not only a source-side filter. Without it a field of type $D\overrightarrow{p}\overrightarrow{i}\to \mathbb{N}$ would be admitted, and blindly applying the function clause would yield $\prod _{y:D\overrightarrow{p}\overrightarrow{i}}\mathbf{1}$, a hypothesis quantifying over the family being defined. The hypothesis recursion is total only on accepted binder types.

Datatype rejection returns $\mathsf{DataReject}(\varphi ,D_r,c_s,\omega ,E,O)$ from definition 122.5. Phase order, declaration order, binder order, and type-preorder make the record deterministic; its expected and observed fields name the exact failed rule premise.

The component is formed simultaneously. Given its motives and one method per constructor, Tfam-block supplies $${\mathsf{ind}}_r:(\overrightarrow{p}:{\mathrm{\Delta }}_p)(\overrightarrow{i}:{\mathrm{\Delta }}_r)(z:D_r\overrightarrow{p}\overrightarrow{i})\to P_r\overrightarrow{p}\overrightarrow{i}z$$ and, for every constructor $c_s$, the rule $${\mathsf{ind}}_{r_s}(\overrightarrow{p},{\overrightarrow{u}}_s,c_s(\overrightarrow{z}))\equiv b_s(\overrightarrow{z},{\overrightarrow{z}}^{\mathsf{ih}})(Block-comp).$$ Here ${\overrightarrow{z}}^{\mathsf{ih}}$ inserts ${\mathsf{ih}}_{\overrightarrow{P}}(A,z)$ immediately after every field $z:A$ whose type mentions the block, including function- and pair-nested occurrences. Writing $\mathsf{lev}(\mathrm{\Delta })$ for the maximum universe inhabited by a binder type in $\mathrm{\Delta }$, the generated eliminator package has level $$max(\mathsf{lev}({\mathrm{\Delta }}_p),\underset{r}{max}\mathsf{lev}({\mathrm{\Delta }}_r),\underset{s}{max}\mathsf{lev}({\mathrm{\Theta }}_s),\underset{r}{max}{\ell }_r,\underset{r}{max}{k}_r).$$ The encoded empty target has the independent fixed definition and typing $${\mathsf{Empty}}_{\mathsf{Timpl}}:=\prod _{X:{\mathcal{U}}_0}X:{\mathcal{U}}_1.$$ No-confusion is stated at one index instance. For $\overrightarrow{ı}:{\mathrm{\Delta }}_r$ and arguments with ${\overrightarrow{u}}_s[\overrightarrow{a}]\equiv \overrightarrow{ı}\equiv {\overrightarrow{u}}_t[\overrightarrow{b}]$, distinct constructor tags eliminate $${\mathsf{Id}}_{D_r\overrightarrow{p}\overrightarrow{ı}}(c_s(\overrightarrow{a}),c_t(\overrightarrow{b}))$$ into ${\mathsf{Empty}}_{\mathsf{Timpl}}$; equal tags produce $\overrightarrow{a}{\equiv }_{{\mathrm{\Theta }}_s}\overrightarrow{b}$, the homogeneous telescopic equality of their arguments. Without the index premise the identity type is not well formed, because the two constructor applications need not inhabit the same type.

Certified recursive calls

A structural certificate is $$\frac{u\in \mathsf{Child}(x)}{\mathrm{\Theta };x⊢u\mathsf{desc}x}.$$ A structural component over a mutual block $\mathcal{B}=(D_1,\dots ,D_r)$ at common parameters $\overrightarrow{p}$ stores, independently of the $q$ functions, a family map $\kappa :{\mathsf{Fin}}_{\mathsf{ind}}(q)\to {\mathsf{Fin}}_{\mathsf{ind}}(r)$. Only this discipline has $\kappa$. It uses the total-space carrier $$L_{\mathcal{B}}:=max(0,\underset{l}{max}\mathsf{lev}({\mathrm{\Delta }}_l),\underset{l}{max}{\ell }_l),{\mathsf{Payload}}_{\mathcal{B}}(l):=\sum _{\overrightarrow{ı}:{\mathrm{\Delta }}_l}{D}_l\overrightarrow{p}\overrightarrow{ı}:{\mathcal{U}}_{L_{\mathcal{B}}},$$ where the payload family is defined by the dependent eliminator for ${\mathsf{Fin}}_{\mathsf{ind}}(r)$, inserting strict lifts into the common universe when required. Then $${\mathsf{Carrier}}_{\mathcal{B}}(\overrightarrow{p}):=\sum _{l:{\mathsf{Fin}}_{\mathsf{ind}}(r)}{\mathsf{Payload}}_{\mathcal{B}}(l):{\mathcal{U}}_{L_{\mathcal{B}}}$$ and the uniform relation generated by $${\mathsf{child}}_{c,r}:{\mathsf{DChild}}_{\mathcal{B}}((k,(\overrightarrow{ȷ},x_r)),(l,(\overrightarrow{ı},c\overrightarrow{x})))$$ for each recursive field $x_r:D_k\overrightarrow{p}\overrightarrow{ȷ}$ of a constructor $c:\mathrm{\Theta }\to D_l\overrightarrow{p}\overrightarrow{ı}$. The stored $u\in \mathsf{Child}(x)$ certificate selects one such generator after the leaf substitution. Thus the tagged call relation is defined uniformly on all inputs, rather than by a leaf-specific child set. This relation is a nonrecursive Timpl-data block at $$K_{\mathcal{B}}=max(\mathsf{lev}({\mathrm{\Delta }}_p),L_{\mathcal{B}},\underset{s}{max}\mathsf{lev}({\mathrm{\Theta }}_s)),$$ the maximum emitted by definition 122.13; its constructor telescopes contain no occurrence of the relation, so positivity accepts it. A primitive structural component uses either ${\mathsf{child}}_{\mathsf{suc}}:{\mathsf{DChild}}_{\mathbb{N}}(n,\mathsf{suc}n)$ or, at fixed $c$, $${\mathsf{child}}_{\mathsf{vcons}}:{\mathsf{DChild}}_{\mathsf{Vec}(c,-)}((n,xs),(\mathsf{suc}n,\mathsf{vcons}(n,a,xs))).$$ Accessibility follows from mutual block induction, Nat-elim, or Vec-elim, respectively. The three carriers and state-constructor maps are For the one discipline chosen by the component, $${\mathsf{in}}_j(\overrightarrow{b})R_S{\mathsf{in}}_i(\overrightarrow{a}):={\mathsf{DChild}}_S({\mu }_j^S(\overrightarrow{b}),{\mu }_i^S(\overrightarrow{a})).$$ A structural component fixes one common block parameter vector, or one common vector element code. It never coerces a primitive carrier into the mutual block carrier. A lexicographic certificate selects the least $k$ for which $a_h\equiv b_h$ for and $b_k{R}_k{a}_k$. The compiled body replaces a call at $\overrightarrow{b}$ by the accessibility recursor hypothesis applied to this stored predecessor proof. Rejection returns $\mathsf{RecReject}(S,f_i\to f_j,\omega ,\delta ,\overrightarrow{a},\overrightarrow{b},F)$ from definition 123.5. The record names the first internal call without a complete direct-child or least-coordinate predecessor proof and stores the failed comparison rather than a fixture-specific message. For each recursive component $S$, compilation first generates the nonrecursive Timpl-data block $${\mathsf{State}}_S:{\mathcal{U}}_{\ell },{\mathsf{in}}_i:(\overrightarrow{a}:{\mathrm{\Delta }}_i)\to {\mathsf{State}}_S(f_i\in S).$$ No constructor argument mentions the generated family, so positivity accepts the block. The relation $R_S$ and the accessibility recursor range over these state constructors; the generated signature is program data, not a Timpl-rec-core rule. For accepted groups, the signature ${\mathrm{\Sigma }}_{\mathcal{G}}$ contains every fixed Timpl contraction and every generated Block-comp equation used by its clause trees and state blocks. The source program root families are those contractions and R-Call. The target replaces R-Call by the C-Call macro whose deterministic nonempty raw-core expansion is the outer definition beta prefix, generated state-block step, WF-$\beta$, and the compiler’s administrative beta prefix. Their dynamic compatible contexts do not enter compiler-generated accessibility proofs, predecessor certificates, or conversion witnesses. Nor are fixed-kernel contractions inside a compiler-marked C-Call administrative region independent target program roots; the macro schedules that whole region atomically. Then $t{\Downarrow }_{\mathsf{R}}v$ and $t{\Downarrow }_{\mathsf{RC}}v$ are finite closures of the respective program steps to a closed constructor normal form. Root-step correspondence treats a fixed contraction, generated block computation, and the R-Call/C-Call pair separately; dynamic-context and finite-closure induction give lemma 123.17, lemma 123.18.

Guarded stream groups

Each finite group fixes one element type $A$, and all its declarations have codomain $\mathsf{Stream}(A)$; heterogeneous streams are checked as separate groups. This side condition is what gives coiterator elaboration one map $h:{\mathsf{State}}_{\mathcal{G}}\to A$, where the compiler generates ${\mathsf{State}}_{\mathcal{G}}$ with one constructor ${\mathsf{in}}_i:(\overrightarrow{a}:{\mathrm{\Delta }}_i)\to {\mathsf{State}}_{\mathcal{G}}$ per declaration. The state block is nonrecursive and accepted by Timpl-data. An edge $f\stackrel{k}{\to }g$ records that $k$ tail observations have been discharged before the call. The card’s two right-side forms make $k$ total and confine it to $\{0,1\}$: a head alias emits $0$ and a tail step emits $1$. A group passes exactly when its zero-weight subgraph is acyclic, which for these weights coincides with every cycle having positive total weight. Each binder retains its inherited Timpl relevance mark. For closed $\cdot ⊢t:A$, group-free subevaluation is defined by the extended typed NbE normalizer: $$t{\Downarrow }_{\mathsf{T}}n⟺n={\mathrm{nf}}_{\mathrm{\Sigma },\cdot }^A(t).$$ Its result is the unique typed $\beta \eta$-long normal form. The optional call-by-value implementation layer $t{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v$ is T-Val–T-Vec-Cons, beginning with $$\frac{\phantom{X}}{v{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{Val},$$ $$\frac{\begin{array}{c}f{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{\lambda }^{ϵ,\mathsf{runtime}}(x:A).b\\ a{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{v}_a\\ b[v_a/x]{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{f{}^{ϵ,\mathsf{runtime}}a{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{App}-\mathrm{R},$$ $$\frac{\begin{array}{c}f{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{\lambda }^{ϵ,\mathsf{erased}}(x:A).b\\ b[a/x]{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{f{}^{ϵ,\mathsf{erased}}a{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{App}-\mathrm{E}.$$ It contains T-Pair, T-Fst, and T-Snd with the exact premises $$\frac{\begin{array}{c}a{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{v}_a\\ b{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{v}_b\end{array}}{(a,b){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}(v_a,v_b)}\mathrm{T}-\mathrm{Pair}$$ $$\frac{s{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}(v_a,v_b)}{{\mathsf{pr}}_1(s){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{v}_a}\mathrm{T}-\mathrm{Fst}\frac{s{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}(v_a,v_b)}{{\mathsf{pr}}_2(s){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{v}_b}\mathrm{T}-\mathrm{Snd}.$$ For field mark ${\kappa }_i$, put ${\hat{a}}_i=v_i$ with premise $a_i{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{v}_i$ when it is runtime, and put ${\hat{a}}_i=a_i$ when it is erased. Then $$\frac{(a_i{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{v}_i{)}_{{\kappa }_i=\mathsf{runtime}}}{c(\overrightarrow{a}){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}c(\hat{\overrightarrow{a}})}\mathrm{T}-\mathrm{Con}.$$ $$\frac{\begin{array}{c}e{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{c}_k(\hat{\overrightarrow{a}})\\ e_k[\hat{\overrightarrow{a}}/{\overrightarrow{x}}_k]{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{\mathsf{case}e\mathsf{of}\{c_j({\overrightarrow{x}}_j)\Rightarrow e_j{\}}_j{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{Case}.$$ The Boolean rules are $$\frac{\begin{array}{c}b{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\mathsf{tt}\\ e_t{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{{\mathsf{ind}}_{\mathbf{2}}(x.C;e_t,e_f,b){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{Bool}-\mathrm{T}.$$ $$\frac{\begin{array}{c}b{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\mathsf{ff}\\ e_f{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{{\mathsf{ind}}_{\mathbf{2}}(x.C;e_t,e_f,b){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{Bool}-\mathrm{F}.$$ Put $$N_C(e_0,e_s;m):=I_C(e_0;n^{{\varrho }_n}.r^{{\varrho }_r}.e_s;m).$$ The natural-number rules are $$\frac{\begin{array}{c}m{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\mathsf{0}\\ e_0{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{N_C(e_0,e_s;m){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{Nat}-\mathrm{Z}$$ $$\frac{\begin{array}{c}m{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\mathsf{suc}(v_n)\\ N_C(e_0,e_s;v_n){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{v}_r\\ e_s[v_n/n,v_r/r]{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{N_C(e_0,e_s;m){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{Nat}-\mathrm{S}.$$ Identity elimination has the rule $$\frac{\begin{array}{c}{e}_q{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{\mathsf{refl}}_{v_q}\\ e_r[a/z]{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{{\mathsf{J}}_{A;a;b}(x.y.p.C;z^{{\varrho }_z}.e_r;e_q){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{J}.$$ The vector rules are $$\frac{\begin{array}{c}m{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\mathsf{0}\\ ys{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\mathsf{vnil}\\ e_0{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{\mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;m,ys){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{Vec}-\mathrm{Nil}$$ $$\frac{\begin{array}{c}m{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\mathsf{suc}(v_n)\\ ys{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\mathsf{vcons}(v_n,v_a,v_{xs})\\ \mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;v_n,v_{xs}){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}{v}_r\\ e_s[v_n/n,v_a/a,v_{xs}/xs,v_r/r]{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v\end{array}}{\mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;m,ys){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v}\mathrm{T}-\mathrm{Vec}-\mathrm{Cons}.$$ There is no T-Call rule. The implementation card is not the meaning of ${\Downarrow }_{\mathsf{T}}$. The accepted NbE normalizer is extended declaration-by-declaration with the nonrecursive Timpl-data constructor, neutral-eliminator, and Block-comp cases. It satisfies $$t{\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}v⟹\mathrm{nf}(t)=\mathrm{nf}(v)\text{and}t{\Downarrow }_{\mathsf{T}}\mathrm{nf}(v),$$ whereas $t{\Downarrow }_{\mathsf{T}}n$ always returns $n=\mathrm{nf}(t)$. Soundness, completeness, stability, substitution, and the implementation bridge are lemma 124.3. The function ${\mathsf{prep}}_{\mathrm{\Delta }}(\overrightarrow{a})$ processes a dependent tuple in telescope order. It normalizes a runtime component as demanded subevaluation and canonicalizes an erased component statically with the same typed normalizer; both results are substituted into later components. No runtime CBV frame forces an erased component. Its clauses are The big-step rules are $$\frac{\begin{array}{c}{\delta }_{\mathsf{co}}(f_i)=({\mathrm{\Delta }}_i;t;e_t)\\ {\mathsf{prep}}_{{\mathrm{\Delta }}_i}(\overrightarrow{a})={\overrightarrow{a}}_v\\ t[{\overrightarrow{a}}_v/\overrightarrow{x}]{\Downarrow }_{\mathsf{T}}v\end{array}}{\mathsf{head}(f_i\overrightarrow{a})\Downarrow v}\mathrm{Co}-\mathrm{Head}-\mathrm{Producer},$$ $$\frac{\begin{array}{c}{\delta }_{\mathsf{co}}(f_i)=({\mathrm{\Delta }}_i;\mathsf{head}(g\overrightarrow{u});e_t)\\ {\mathsf{prep}}_{{\mathrm{\Delta }}_i}(\overrightarrow{a})={\overrightarrow{a}}_v\\ {\mathsf{prep}}_{{\mathrm{\Delta }}_g}(\overrightarrow{u}[{\overrightarrow{a}}_v/\overrightarrow{x}])=\overrightarrow{b}\\ \mathsf{head}(g\overrightarrow{b})\Downarrow v\end{array}}{\mathsf{head}(f_i\overrightarrow{a})\Downarrow v}\mathrm{Co}-\mathrm{Head}-\mathrm{Alias},$$ $$\frac{\begin{array}{c}{\delta }_{\mathsf{co}}(f_i)=({\mathrm{\Delta }}_i;e_h;g\overrightarrow{u})\\ {\mathsf{prep}}_{{\mathrm{\Delta }}_i}(\overrightarrow{a})={\overrightarrow{a}}_v\\ {\mathsf{prep}}_{{\mathrm{\Delta }}_g}(\overrightarrow{u}[{\overrightarrow{a}}_v/\overrightarrow{x}])=\overrightarrow{b}\end{array}}{\mathsf{tail}(f_i\overrightarrow{a})\Downarrow g\overrightarrow{b}}\mathrm{Co}-\mathrm{Tail}-\mathrm{Unfold}.$$ A closed well-typed group-free tuple has a unique prepared form by lemma 124.3. Preparation composes with group-free simultaneous substitution and is idempotent on prepared tuples; these are lemma 124.12, lemma 124.13. Those two facts justify alias resolution and the generalized induction step in the source/coiterator simulation. A bare stream call has no eager unfolding rule. Observation words and their path rules are $$o::=\mathsf{head}\mid \mathsf{tail}\cdot o,\frac{\mathsf{head}(s)\Downarrow v}{s{\Downarrow }_{\mathsf{head}}v},$$ and $$\frac{\mathsf{tail}(s)\Downarrow s^{\prime }{s}^{\prime }{\Downarrow }_{o}v}{s{\Downarrow }_{\mathsf{tail}\cdot o}v}.$$ Coiterator elaboration computes by $$\mathsf{head}(\mathsf{coiter}(h,t,s)){⇝}_{0}h(s),\mathsf{tail}(\mathsf{coiter}(h,t,s)){⇝}_0\mathsf{coiter}(h,t,t(s)).$$ Its normalizer-defined state-strict evaluation rules are $$\frac{\begin{array}{c}s{\Downarrow }_{\mathsf{T}}{s}_v\\ h(s_v){\Downarrow }_{\mathsf{T}}v\end{array}}{\mathsf{head}(\mathsf{coiter}(h,t,s))\Downarrow v}\mathrm{Coiter}-\mathrm{Head}$$ and $$\frac{\begin{array}{c}s{\Downarrow }_{\mathsf{T}}{s}_v\\ t(s_v){\Downarrow }_{\mathsf{T}}{s}_v^{\prime }\end{array}}{\mathsf{tail}(\mathsf{coiter}(h,t,s))\Downarrow \mathsf{coiter}(h,t,s_v^{\prime })}\mathrm{Coiter}-\mathrm{Tail}.$$

Dependent copattern frontiers

For a row map ${\hat{\rho }}_r:{\mathrm{\Theta }}_r\to \mathrm{\Delta }$, static acceptance checks Closed right sides use $w::=v\mid d^{\prime }\overrightarrow{a}$ and $$\frac{\begin{array}{c}e\text{ contains no call to the copattern group}\\ e{\Downarrow }_{\mathsf{T}}v\end{array}}{e{\Downarrow }_{\mathsf{C}}v}\mathrm{Copat}-\mathrm{Result}-\mathrm{Val},$$ $$\frac{\begin{array}{c}{d}^{\prime }:({\mathrm{\Delta }}^{\prime })\to R\overrightarrow{p}{\overrightarrow{ı}}^{\prime }\\ (b_l{\Downarrow }_{\mathsf{T}}{a}_l{)}_{l\in {\mathrm{\Delta }}^{\prime }}\end{array}}{d^{\prime }{@}_{{\mathrm{\Delta }}^{\prime }}\overrightarrow{b}{\Downarrow }_{\mathsf{C}}{d}^{\prime }{@}_{{\mathrm{\Delta }}^{\prime }}\overrightarrow{a}}\mathrm{Copat}-\mathrm{Result}-\mathrm{Rec}.$$ The least matching row for one demanded field is selected only at a closed well-typed ready tuple, using the matching relation of definition 121.6: Longer source paths are generated only through a recursive field: $$\frac{\begin{array}{c}j\in N\\ s{\Downarrow }_{{\pi }_j}{s}^{\prime }\\ s^{\prime }{\Downarrow }_{o}v\end{array}}{s{\Downarrow }_{{\pi }_j\cdot o}v}\mathrm{Copat}-\mathrm{Path}-\mathrm{Step}.$$ An unrelated record-valued nonrecursive field ends a path in this card. The intermediate case-tree relation, also restricted to closed ready tuples, is generated by $$\frac{\begin{array}{c}{a}_x{\Downarrow }_{\mathsf{T}}{c}_k(\overrightarrow{v})\\ Q_k[\overrightarrow{v}/{\overrightarrow{y}}_k]\Downarrow w\end{array}}{\mathsf{split}(x;\{c_l({\overrightarrow{y}}_l)\Rightarrow Q_l{\}}_l)[\overrightarrow{a}]\Downarrow w}\mathrm{Tree}-\mathrm{Split},\frac{e\sigma {\Downarrow }_{\mathsf{C}}w}{\mathsf{leaf}(r,\sigma ,e)\Downarrow w}\mathrm{Tree}-\mathrm{Leaf}.$$ For the tree $Q_d$ generated for declaration $d$, recursive paths use $$\frac{\begin{array}{c}j\in N\\ Q_d(\overrightarrow{a}){\Downarrow }_{{\pi }_j}{d}^{\prime }\overrightarrow{b}\\ Q_{d^{\prime }}(\overrightarrow{b}){\Downarrow }_{o}v\end{array}}{Q_d(\overrightarrow{a}){\Downarrow }_{{\pi }_j\cdot o}v}\mathrm{Tree}-\mathrm{Path}-\mathrm{Step}.$$ At field ${\pi }_j$, a typed frontier records all earlier field terms: $$\mathrm{\Theta }\mid z:R\overrightarrow{p}\overrightarrow{i}\mid {\pi }_1(z)=u_1,\dots ,{\pi }_{j-1}(z)=u_{j-1}⊢{\pi }_j(z):A_j[\overrightarrow{u}/\overrightarrow{\pi }].$$ Input splits transport this whole telescope by their dependency-preserving substitution. A complete field spine becomes one sequential Rec-Corec method tuple in the same order. Set $$k_{\mathcal{G}}:=max(\mathsf{lev}({\mathrm{\Delta }}_i),\underset{d\in \mathcal{G}}{max}\mathsf{lev}({\mathrm{\Delta }}_d(\overrightarrow{ı}))).$$ The compiler generates the indexed Timpl-data family $${\mathsf{State}}_{\mathcal{G}}:(\overrightarrow{ı}:{\mathrm{\Delta }}_i)\to {\mathcal{U}}_{k_{\mathcal{G}}},{\mathsf{in}}_d:(\overrightarrow{ı}:{\mathrm{\Delta }}_i)(\overrightarrow{a}:{\mathrm{\Delta }}_d(\overrightarrow{ı}))\to {\mathsf{State}}_{\mathcal{G}}(\overrightarrow{ı}).$$ The maximum is the universe constraint supplied to the level solver. It covers every index and constructor telescope, and the family occurs in none of them, so Timpl-data formation and positivity accept the block. Abbreviate this family by $S$. A recursive leaf $d^{\prime }{@}_{{\mathrm{\Delta }}_{d^{\prime }}({\overrightarrow{ı}}_j)}\overrightarrow{b}$ translates to ${\mathsf{in}}_{d^{\prime }}({\overrightarrow{ı}}_j,\Vert \overrightarrow{b}\Vert ):S{\overrightarrow{ı}}_j$. The Rec-Corec extension is checked transactionally. First place the method-independent declaration $${\mathsf{corec}}_R:(\overrightarrow{ı}:{\mathrm{\Delta }}_i)(s:S\overrightarrow{ı})\to R\overrightarrow{p}\overrightarrow{ı}$$ in a provisional signature. After methods $h_1,\dots ,h_{j-1}$ have checked, define their actual outputs and decoded fields in the context $(\overrightarrow{ı}:{\mathrm{\Delta }}_i)(s:S\overrightarrow{ı})$: Write $${\sigma }_j:=[{\overline{v}}_1,\dots ,{\overline{v}}_{j-1}/{\pi }_1(z_s),\dots ,{\pi }_{j-1}(z_s)].$$ Thus every self occurrence is instantiated by the generated record, and later dependent fields see the record generated from each actual recursive method output, not the state itself. The sequential check is $$\frac{\phantom{X}}{{\mathrm{\Sigma }}^{+}⊢{\mathsf{methods}}_S():{\mathrm{\Phi }}_{\le 0}}\mathrm{Corec}-\mathrm{Meth}-\mathrm{Nil}.$$ Previously checked method terms are substituted literally. Their beta rules are available, but no coprojection equation is available during method checking. Once the finite sequential judgment succeeds, the constant and the following equations are committed together: for a nonrecursive and a recursive field respectively. A recursive method returns a state, never a record; substitution of ${\overline{v}}_l$ is what types a later field that mentions that recursive projection. The transaction has the displayed Rec-Corec rule form $$\frac{\begin{array}{c}\mathrm{\Sigma }⊢R\mathsf{card}\mathsf{record}:\mathrm{\Phi }\\ \mathrm{\Sigma }⊢S:({\mathrm{\Delta }}_i)\to {\mathcal{U}}_k\\ {\mathrm{\Sigma }}^{+}⊢{\mathsf{methods}}_S(h_1,\dots ,h_m):\mathrm{\Phi }\end{array}}{\mathrm{\Sigma },{\mathsf{corec}}_R,(E_j{)}_{1\le j\le m}\mathsf{signature}}\mathrm{Rec}-\mathrm{Corec},$$ where ${\mathrm{\Sigma }}^{+}$ contains the provisional method-independent corecursor and $E_j$ is the corresponding displayed equation. No conclusion is committed unless every method premise checks.

Consider the legal unindexed fields The earlier projection $\mathsf{label}:R\to \mathbf{2}$ is already in scope when the flag type is formed. Translation gives $${\overline{v}}_2={\mathsf{corec}}_R(h_{2}s),A_3^{\ast }[h_1,h_2]={\mathsf{Id}}_{\mathbf{2}}(\mathsf{label}({\mathsf{corec}}_R(h_{2}s)),\mathsf{tt}).$$

The compiled declaration has the exact outer form $$\Vert Q_d\Vert =\lambda \overrightarrow{ı}.\lambda \overrightarrow{a}.{\mathsf{corec}}_R\overrightarrow{ı}({\mathsf{in}}_d(\overrightarrow{ı},\overrightarrow{a})).$$ For an applied compiled declaration, the deterministic nonempty relation $q{⟹}_{\mathsf{in}}c$ contracts only these outer beta-redexes and stops at the displayed primitive corecursor. It never selects an input branch or row, uses Block-comp, contracts a corecursor projection, or enters a method body. Field selection chooses a method first; that method then runs its own translated input-split tree. The bridge into the distinct target observation is $$\frac{\begin{array}{c}q{⟹}_{\mathsf{in}}c\\ c{{\Downarrow }_{\mathsf{CC}}}_{o}v\end{array}}{q{{\Downarrow }_{\mathsf{CC}}}_{o}v}\mathrm{Core}-\mathrm{Prepare}.$$ For a closed target object $c={\mathsf{corec}}_R\overrightarrow{ı}s$, abbreviate $c_j(s^{\prime })={\mathsf{corec}}_R{\overrightarrow{ı}}_j{s}^{\prime }$. Then its recursive-field rule is narrow enough to display with the value-field rule: $$\frac{\begin{array}{c}j\notin N\\ {\pi }_j(c){⇝}_{0}e\\ e{\Downarrow }_{\mathsf{T}}v\end{array}}{c{{\Downarrow }_{\mathsf{CC}}}_{{\pi }_j}v}\mathrm{Core}-\mathrm{Field}-\mathrm{Val},$$ $$\frac{\begin{array}{c}j\in N\\ {\pi }_j(c){⇝}_0{\mathsf{corec}}_R{\overrightarrow{ı}}_j(h_j\overrightarrow{ı}s)\\ h_j\overrightarrow{ı}s{\Downarrow }_{\mathsf{T}}{s}^{\prime }\end{array}}{c{{\Downarrow }_{\mathsf{CC}}}_{{\pi }_j}{c}_j(s^{\prime })}\mathrm{Core}-\mathrm{Field}-\mathrm{Rec},$$ and Core-Path-Step composes such an observation with a shorter target path only when $j\in N$.

Runtime erasure

The exact first-order source phrases are those of definition 126.3: variables, annotated abstractions and applications, dependent pairs and projections, reflexivity, Boolean, natural, identity, and vector elimination, declared constructors and cases, and saturated recursive calls. Recursive declarations are not first class. The relevance judgments begin with

$\mathrm{\Gamma }⊢e:A$

$\mathrm{\Gamma }⊢e\mathsf{erased}$

$x^{\mathsf{runtime}}:A\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x\mathsf{runtime}$

$\mathrm{\Gamma },x^{\mathsf{runtime}}:A⊢b\mathsf{runtime}$

$\mathrm{\Gamma }⊢{\lambda }^{ϵ,\mathsf{runtime}}(x:A).b\mathsf{runtime}$

$\mathrm{\Gamma }⊢f\mathsf{runtime}$$\mathrm{\Gamma }⊢a\mathsf{runtime}$

$\mathrm{\Gamma }⊢f{}^{ϵ,\mathsf{runtime}}a\mathsf{runtime}$

$\mathrm{\Gamma },x^{\mathsf{erased}}:A⊢b\mathsf{runtime}$$\mathrm{\Gamma }⊢a\mathsf{erased}$

$\mathrm{\Gamma }⊢{\lambda }^{{ϵ}^{\prime },\mathsf{erased}}(x:A).b{}^{ϵ,\mathsf{erased}}a\mathsf{runtime}$

Rule Rel-App-E accepts only a visible administrative redex; a variable-headed erased application is rejected. Rules Rel-Con, Rel-Case, and Rel-Call require constructor fields, branches, and saturated call inputs at the relevance recorded by the accepted declaration. Dependent pairs, projections, and retained reflexivity are checked by $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢a\mathsf{runtime}\\ \mathrm{\Gamma }⊢b\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢(a,b)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Pair}\frac{\mathrm{\Gamma }⊢s\mathsf{runtime}}{\mathrm{\Gamma }⊢{\mathsf{pr}}_1(s)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Fst}$$ $$\frac{\mathrm{\Gamma }⊢s\mathsf{runtime}}{\mathrm{\Gamma }⊢{\mathsf{pr}}_2(s)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Snd}\frac{\mathrm{\Gamma }⊢a:A}{\mathrm{\Gamma }⊢{\mathsf{refl}}_a\mathsf{runtime}}\mathrm{Rel}-\mathrm{Refl}.$$ The primitive eliminator rules are $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢b\mathsf{runtime}\\ \mathrm{\Gamma }⊢e_t\mathsf{runtime}\\ \mathrm{\Gamma }⊢e_f\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbf{2}}(x.C;e_t,e_f,b)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Bool}-\mathrm{Elim},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e_0\mathsf{runtime}\\ \mathrm{\Gamma },n^{{\varrho }_n}:\mathbb{N},r^{{\varrho }_r}:C(n)⊢e_s\mathsf{runtime}\\ \mathrm{\Gamma }⊢m\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢I_C(e_0;n^{{\varrho }_n}.r^{{\varrho }_r}.e_s;m)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Nat}-\mathrm{Elim},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma },z^{{\varrho }_z}:A⊢e_r\mathsf{runtime}\\ \mathrm{\Gamma }⊢a{\varrho }_z\\ \mathrm{\Gamma }⊢e_q\mathsf{erased}\end{array}}{\mathrm{\Gamma }⊢{\mathsf{J}}_{A;a;b}(x.y.p.C;z^{{\varrho }_z}.e_r;e_q)\mathsf{runtime}}\mathrm{Rel}-\mathrm{J},$$ Put $$\mathcal{V}:=\mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;m,ys).$$ Put also $${\mathrm{\Gamma }}_{\mathcal{V}}:=\mathrm{\Gamma },n^{{\varrho }_n}:\mathbb{N},a^{{\varrho }_a}:A,x{s}^{\mathsf{runtime}}:\mathsf{Vec}(A,n),r^{{\varrho }_r}:P(n,xs).$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e_0\mathsf{runtime}\\ {\mathrm{\Gamma }}_{\mathcal{V}}⊢e_s\mathsf{runtime}\\ \mathrm{\Gamma }⊢m{\varrho }_m\\ \mathrm{\Gamma }⊢ys\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢\mathcal{V}\mathsf{runtime}}\mathrm{Rel}-\mathrm{Vec}-\mathrm{Elim}.$$ The proof and motive of Rel-J are static. Its endpoint $a$ is retained exactly when the branch uses $z$. A runtime vector index forces the predecessor constructor-field mark ${\kappa }_n$ to be runtime, and the structural vector child is always runtime. A runtime branch-use mark ${\varrho }_n$ or ${\varrho }_a$ respectively requires the constructor-field mark ${\kappa }_n$ or ${\kappa }_a$ to be runtime; an erased branch may ignore a retained field. Every binder whose declared type is judgmentally a universe is erased because Texec has no universe or source-type representation. A data-valued index may be runtime only when its value forms occur in the source runtime grammar and target representation.

The source call-by-value relation $e\Downarrow v$ of definition 126.5 is relevance directed. For a marked argument $a_i$, put ${\hat{a}}_i=v_i$ when the mark is runtime and $a_i\Downarrow v_i$, and put ${\hat{a}}_i=a_i$ with no evaluation premise when the mark is erased. Source and Texec share the glyph, but their disjoint grammars select disjoint rule cards. The complete source card begins $$\frac{\phantom{X}}{v\Downarrow v}\mathrm{S}-\mathrm{Val}\frac{\begin{array}{c}f\Downarrow {\lambda }^{ϵ,\mathsf{runtime}}(x:A).b\\ a\Downarrow v_a\\ b[v_a/x]\Downarrow v\end{array}}{f{}^{ϵ,\mathsf{runtime}}a\Downarrow v}\mathrm{S}-\mathrm{App}-\mathrm{R},$$ $$\frac{\begin{array}{c}f\Downarrow {\lambda }^{ϵ,\mathsf{erased}}(x:A).b\\ b[a/x]\Downarrow v\end{array}}{f{}^{ϵ,\mathsf{erased}}a\Downarrow v}\mathrm{S}-\mathrm{App}-\mathrm{E},$$ $$\frac{\begin{array}{c}a\Downarrow v_a\\ b\Downarrow v_b\end{array}}{(a,b)\Downarrow (v_a,v_b)}\mathrm{S}-\mathrm{Pair}\frac{s\Downarrow (v_a,v_b)}{{\mathsf{pr}}_1(s)\Downarrow v_a}\mathrm{S}-\mathrm{Fst}\frac{s\Downarrow (v_a,v_b)}{{\mathsf{pr}}_2(s)\Downarrow v_b}\mathrm{S}-\mathrm{Snd},$$ $$\frac{(a_i\Downarrow v_i{)}_{{\kappa }_i=\mathsf{runtime}}}{c(a_1,\dots ,a_n)\Downarrow c({\hat{a}}_1,\dots ,{\hat{a}}_n)}\mathrm{S}-\mathrm{Con},$$ $$\frac{\begin{array}{c}e\Downarrow c_k(\hat{\overrightarrow{a}})\\ e_k[\hat{\overrightarrow{a}}/{\overrightarrow{x}}_k]\Downarrow v\end{array}}{\mathsf{case}e\mathsf{of}\{c_j({\overrightarrow{x}}_j)\Rightarrow e_j{\}}_j\Downarrow v}\mathrm{S}-\mathrm{Case},$$ $$\frac{\begin{array}{c}b\Downarrow \mathsf{tt}\\ e_t\Downarrow v\end{array}}{{\mathsf{ind}}_{\mathbf{2}}(x.C;e_t,e_f,b)\Downarrow v}\mathrm{S}-\mathrm{Bool}-\mathrm{T}\frac{\begin{array}{c}b\Downarrow \mathsf{ff}\\ e_f\Downarrow v\end{array}}{{\mathsf{ind}}_{\mathbf{2}}(x.C;e_t,e_f,b)\Downarrow v}\mathrm{S}-\mathrm{Bool}-\mathrm{F},$$ Abbreviate $$\mathcal{N}(q):=I_C(e_0;n^{{\varrho }_n}.r^{{\varrho }_r}.e_s;q).$$ $$\frac{\begin{array}{c}m\Downarrow \mathsf{0}\\ e_0\Downarrow v\end{array}}{\mathcal{N}(m)\Downarrow v}\mathrm{S}-\mathrm{Nat}-\mathrm{Z},$$ $$\frac{\begin{array}{c}m\Downarrow \mathsf{suc}(v_n)\\ \mathcal{N}(v_n)\Downarrow v_r\\ e_s[v_n/n,v_r/r]\Downarrow v\end{array}}{\mathcal{N}(m)\Downarrow v}\mathrm{S}-\mathrm{Nat}-\mathrm{S},$$ $$\frac{\begin{array}{c}{e}_q\Downarrow {\mathsf{refl}}_{v_q}\\ e_r[a/z]\Downarrow v\end{array}}{{\mathsf{J}}_{A;a;b}(x.y.p.C;z^{{\varrho }_z}.e_r;e_q)\Downarrow v}\mathrm{S}-\mathrm{J},$$ $$\frac{\begin{array}{c}m\Downarrow \mathsf{0}\\ ys\Downarrow \mathsf{vnil}\\ e_0\Downarrow v\end{array}}{\mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;m,ys)\Downarrow v}\mathrm{S}-\mathrm{Vec}-\mathrm{Nil},$$ $$\frac{\begin{array}{c}m\Downarrow \mathsf{suc}(v_n)\\ ys\Downarrow \mathsf{vcons}(v_n,v_a,v_{xs})\\ \mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;v_n,v_{xs})\Downarrow v_r\\ e_s[v_n/n,v_a/a,v_{xs}/xs,v_r/r]\Downarrow v\end{array}}{\mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;m,ys)\Downarrow v}\mathrm{S}-\mathrm{Vec}-\mathrm{Cons},$$ $$\frac{\begin{array}{c}(y_j\Downarrow u_j{)}_{{\sigma }_j=\mathsf{runtime}}\\ (a_i\Downarrow v_i{)}_{{\varrho }_i=\mathsf{runtime}}\\ b_f[\hat{\overrightarrow{y}}/\overrightarrow{y},\hat{\overrightarrow{a}}/\overrightarrow{x}]\Downarrow v\\ {\delta }_s(f)=({\overrightarrow{y}}^{\overrightarrow{\sigma }};{\overrightarrow{x}}^{\overrightarrow{\varrho }};b_f)\end{array}}{f⟨\overrightarrow{y}⟩(\overrightarrow{a})\Downarrow v}\mathrm{S}-\mathrm{Call}.$$ The relation is partial on raw syntax: neutral or mismatched scrutinees and wrong-arity calls have no rule. Forward simulation assumes a source derivation. Erased arguments are checked static syntax substituted on the source side and are evaluated by neither source nor target.

Runtime binders survive and erased binders disappear: Pairs, projections, retained reflexivity, Boolean elimination, and identity elimination erase by The identity clause is structural on the checked branch derivation; marked substitution proves that it equals $|e_r[a/z]|$. Thus a proof retained by a $\mathrm{\Sigma }$-component or constructor is not deleted; it is represented by $C_{\mathsf{refl}}$. Constructors retain runtime fields in declaration order. A target case pattern retains a binder exactly when the corresponding constructor-field mark ${\kappa }_i$ is runtime, even when its independent branch-use mark ${\varrho }_i$ is erased; admissibility requires runtime branch use to imply runtime field retention. Recursive closures retain their tag and runtime environment. For ${\delta }_s(f)=({\overrightarrow{y}}^{\overrightarrow{\sigma }};{\overrightarrow{x}}^{\overrightarrow{\varrho }};b_f)$, compilation creates $${\delta }_t(f)=(\overrightarrow{y}{|}_{\overrightarrow{\sigma }=\mathsf{runtime}};\overrightarrow{x}{|}_{\overrightarrow{\varrho }=\mathsf{runtime}};|b_f|).$$ A saturated call to one is $\mathsf{call}(\mathsf{clos}(f,\overrightarrow{w}),\overrightarrow{t})$.

Every primitive natural or vector eliminator occurrence $o$ receives a stable tag ${\nu }_N(o)$ or ${\nu }_V(o)$. The natural tag stores the ordered runtime lexical slots $\overrightarrow{y}$, one scrutinee parameter $m$, and the body $$\mathsf{case}m\mathsf{of}\{C_{\mathsf{0}}\Rightarrow |e_0|,C_{\mathsf{suc}}(n)\Rightarrow |e_s{|}^{\mathrm{♮}}\},$$ where, when the recursive hypothesis is runtime, $|e_s{|}^{\mathrm{♮}}$ is the administrative beta-redex $$(\lambda r.|e_s|)\mathsf{call}(\mathsf{clos}({\nu }_N(o),\overrightarrow{y}),n).$$ This forces the recursive call to a value before installing it in the branch, matching source call by value. The vector tag stores its ordered slots, optional runtime index, and vector scrutinee; its successor branch analogously applies $\lambda r.|e_s|$ to the recursive $\mathsf{call}(\mathsf{clos}({\nu }_V(o),\overrightarrow{z}),[n{]}_{{\varrho }_m},xs)$. Stable occurrence tags and fixed lexical slots make runtime substitution fill slots without regenerating tags.

Source evaluation is sound for judgmental equality: $$\mathrm{\Gamma }⊢e:Ae\Downarrow v⟹\mathrm{\Gamma }⊢e\equiv v:A.$$ The rule induction uses computation plus substitution congruence in every dependent case; in particular it converts application results along $a\equiv v_a$, second projections along the evaluated first component, eliminator motives along evaluated indices and scrutinees, and identity branches along their endpoint equalities. Hence source evaluation preserves Timpl typing. It also preserves runtime relevance by a second induction using marked substitution; that statement supplies the relevance premise required at every runtime substitution in forward simulation.

Texec cases have pairwise distinct branch tags. Texec evaluation is deterministic left-to-right call by value. Its complete rule card begins with $$\frac{\phantom{X}}{w\Downarrow w}\mathrm{E}-\mathrm{Val}\frac{\begin{array}{c}{t}_1\Downarrow \lambda x.t\\ t_2\Downarrow w_2\\ t[w_2/x]\Downarrow w\end{array}}{t_1{t}_2\Downarrow w}\mathrm{E}-\mathrm{App}.$$ Constructor blocks and closures evaluate their fields from left to right: $$\frac{(t_i\Downarrow w_i{)}_{1\le i\le n}}{C_k(t_1,\dots ,t_n)\Downarrow C_k(w_1,\dots ,w_n)}\mathrm{E}-\mathrm{Con}\frac{(t_i\Downarrow w_i{)}_i}{\mathsf{clos}(f,\overrightarrow{t})\Downarrow \mathsf{clos}(f,\overrightarrow{w})}\mathrm{E}-\mathrm{Clos}.$$ The remaining two rules are $$\frac{\begin{array}{c}t\Downarrow C_k(\overrightarrow{w})\\ t_k[\overrightarrow{w}/{\overrightarrow{x}}_k]\Downarrow w\end{array}}{\mathsf{case}t\mathsf{of}\{C_j({\overrightarrow{x}}_j)\Rightarrow t_j{\}}_j\Downarrow w}\mathrm{E}-\mathrm{Case}$$ $$\frac{\begin{array}{c}{\delta }_t(f)=(\overrightarrow{y};\overrightarrow{x};t_f)\\ t\Downarrow \mathsf{clos}(f,\overrightarrow{w})\\ (t_i\Downarrow w_i{)}_i\\ t_f[\overrightarrow{w}/\overrightarrow{y}][{\overrightarrow{w}}_i/\overrightarrow{x}]\Downarrow w\end{array}}{\mathsf{call}(t,\overrightarrow{t})\Downarrow w}\mathrm{E}-\mathrm{Call}.$$ Texec is untyped, so the reference invariant is target well-formedness plus the value representation relation, not a target typing judgment. A configuration with no applicable rule is stuck. Representation well-formedness excludes malformed stored arities; forward simulation, under a source evaluation derivation, constructs the matching dynamic rule sequence and excludes wrong value shapes.

Co-erasure uses the runtime-first-order card of definition 126.15. Every retained field of the element and state data types is recursively data-valued. No retained field has $\mathrm{\Pi }$-type. Each generated map is one outer state lambda. Its body contains only variables, data constructors, pairs, reflexivity, datatype cases, and first-order instances of the four primitive eliminators. There is no internal application or named call. For such a map $g$, $$g(\sigma ){\Downarrow }_{\mathsf{T}}n⟹\mathrm{\exists }!v.g(\sigma )\Downarrow v\wedge \mathrm{nf}(v)=n\wedge |v|=|n|.$$ This is lemma 126.18; the restriction is what excludes a retained lambda whose CBV body and NbE normal body have different target syntax.

For co-erasure, fresh nullary tags satisfy $${\delta }_t(h_{\ast })=(s;\cdot ;|h(s)|),$$ $${\delta }_t(t_{\ast })=(s;\cdot ;(\lambda s^{\prime }.C_{\mathsf{stream}}(\mathsf{clos}(h_{\ast },s^{\prime }),\mathsf{clos}(t_{\ast },s^{\prime })))|t(s)|).$$ Thus the tail tag computes the next state once and returns the next stream block; the ordinary compiled tag of $t:S\to S$ would return only a state. Finite target observation is the separate judgment $\mathsf{Obs}(q,o,w)$, generated by $$\frac{\mathsf{call}(h)\Downarrow w}{\mathsf{Obs}(C_{\mathsf{stream}}(h,k),\mathsf{head},w)}\mathrm{Obs}-\mathrm{Head}$$ and $$\frac{\begin{array}{c}\mathsf{call}(k)\Downarrow C_{\mathsf{stream}}(h^{\prime },k^{\prime })\\ \mathsf{Obs}(C_{\mathsf{stream}}(h^{\prime },k^{\prime }),o,w)\end{array}}{\mathsf{Obs}(C_{\mathsf{stream}}(h,k),\mathsf{tail}\cdot o,w)}\mathrm{Obs}-\mathrm{Tail}.$$ It is not an unlisted Texec term former.

System Fi index erasure

System Fi extends $F_{\omega }$ by index-arrow kinds, index abstraction and application, and index polymorphism. The extra clauses are Terms are unchanged. The exact typing consequence is $$\frac{\mathrm{\Delta }⊢\mathrm{\Gamma }\mathrm{\Delta };\mathrm{\Gamma }⊢t:A}{{\mathrm{\Delta }}^{\circ };({\mathrm{\Delta }}^{\bullet },\mathrm{\Gamma }{)}^{\circ }{⊢}_{F_{\omega }}t:A^{\circ }}.$$ Here ${\mathrm{\Delta }}^{\bullet }$ moves index bindings to the target term context; it drops out when the term contains no free index variable.