ch:dependent-copattern-elaboration: ch:dependent-copattern-elaboration

Writing $z:\mathsf{Orbit}(q,a)$, the frontiers and leaf types are $$z:\mathsf{Orbit}(q,a)⊢\mathsf{next}(z):A,u_1=q(a):A.$$ Put ${\mathrm{\Gamma }}_2:=z:\mathsf{Orbit}(q,a),\mathsf{next}(z)=q(a)$. Then $${\mathrm{\Gamma }}_2⊢\mathsf{step}(z):{\mathsf{Id}}_A(q(a),q(a)),u_2={\mathsf{refl}}_{q(a)}.$$ For the final field the frontier and leaf are ${\mathrm{\Gamma }}_3:={\mathrm{\Gamma }}_2,\mathsf{step}(z)={\mathsf{refl}}_{q(a)}$, with $${\mathrm{\Gamma }}_3⊢\mathsf{tail}(z):\mathsf{Orbit}(q,q(a)),u_3=\mathsf{iterate}(q,q(a)).$$ The tail leaf applies the state substitution $[q(a)/a]$ to the record index. The step leaf instead substitutes the stored next term for the earlier projection in its identity type.

Here $N=\{2\}$. The first method has $A_1^{\ast }[]=\mathbf{2}$. The recursive-field clause gives $A_2^{\ast }[h_1]=S$, actual output $v_2=h_{2}s:S$, and ${\overline{v}}_2={\mathsf{corec}}_R(h_{2}s):R$. Substitution of that decoded field into the third declaration gives $$A_3^{\ast }[h_1,h_2]={\mathsf{Id}}_{\mathbf{2}}(\mathsf{label}({\mathsf{corec}}_R(h_{2}s)),\mathsf{tt}).$$ If the state $h_{2}s$ replaces ${\overline{v}}_2$, the required application judgment is $h_{2}s:S⊢\mathsf{label}(h_{2}s):\mathbf{2}$, but the earlier generated projection has type $\mathsf{label}:R\to \mathbf{2}$ and requires $h_{2}s:R$. Since the corecursor card assumes no conversion $S\equiv R$, that judgment is not derivable.

The Tcop-tree is the coprojection spine $\mathsf{next}$, $\mathsf{step}$, $\mathsf{tail}$, with the three frontiers displayed in the preceding solution and leaves $q(a)$, ${\mathsf{refl}}_{q(a)}$, and $\mathsf{iterate}(q,q(a))$. Translation generates the indexed family and tagged constructor $${\mathsf{State}}_{\mathcal{G}}:(b:A)\to {\mathcal{U}}_i,{\mathsf{in}}_{\mathsf{iterate}}:(b:A)\to {\mathsf{State}}_{\mathcal{G}}(b),$$ where $i=\mathsf{lev}(b:A)$ is the maximum prescribed by the generated state-block rule. The sequential methods are $$h_1(a,s)=q(a),h_2(a,s)={\mathsf{refl}}_{q(a)},h_3(a,s)={\mathsf{in}}_{\mathsf{iterate}}(q(a)).$$ After $h_1$ has checked, the second codomain is $${\mathsf{Id}}_A(h_1(a,s),q(a))\equiv {\mathsf{Id}}_A(q(a),q(a))$$ by ordinary reduction of the previously checked method term. Thus $h_2$ checks before the corecursor and its coprojection equations are committed. The third method checks at ${\mathsf{State}}_{\mathcal{G}}(q(a))$. The source leaf $\mathsf{iterate}(q,q(a))$ is recovered as $$\mathsf{corec}(q(a)){\mathsf{in}}_{\mathsf{iterate}}(q(a)).$$ The recursive field carries only the tagged state at the moved index, never a record. The empty declaration fiber contributes no extra constructor argument; the generated index $b:A$ remains explicit.

Two tail observations change the index from $a$ to $q(a)$ and then to $q(q(a))$. The final next observation returns $q(q(q(a)))$; for successor at zero this is three.

With $\mathsf{step}$ declared first, its result type still contains $\mathsf{next}(z)$, but the record telescope has not introduced the projection $\mathsf{next}$. That occurrence is the first ill-scoped term. The dependency graph has the edge $\mathsf{next}\to \mathsf{step}$. Every dependency-preserving field order is a topological order of this graph, so next must precede step. Consequently no such permutation can put step first.