ch:corecursive-definitions: ch:corecursive-definitions

The prepared tuple is ${\mathsf{prep}}_{n:\mathbb{N}}(0)=(0)$. Hence Co-Tail-Unfold gives $$\mathsf{tail}(\mathsf{from}(0))\Downarrow \mathsf{from}(\mathsf{suc}0).$$ A second preparation and its normalizer-defined group-free premise are Thus Co-Head-Producer gives $$\mathsf{head}(\mathsf{from}(\mathsf{suc}0))\Downarrow \mathsf{suc}0.$$ The head observation rule derives $$\mathsf{from}(\mathsf{suc}0){\Downarrow }_{\mathsf{head}}\mathsf{suc}0.$$ The path-step rule combines this judgment with the tail premise and derives $$\mathsf{from}(0){\Downarrow }_{\mathsf{tail}\cdot \mathsf{head}}1.$$

The two head aliases give the zero edges and the three tail steps give the positive edges: $$f\stackrel{0}{\to }g,g\stackrel{0}{\to }h,f\stackrel{1}{\to }g,g\stackrel{1}{\to }h,h\stackrel{1}{\to }f.$$ The head of $h$ is a producer, so $h$ emits no zero edge. Deleting the positive edges leaves the path $f\to g\to h$. One valid rank is $r(f)=2$, $r(g)=1$, $r(h)=0$; the required inequalities are and .

The two maps are determined by the state constructors: $$h({\mathsf{in}}_e)=0,h({\mathsf{in}}_o)=1,t({\mathsf{in}}_e)={\mathsf{in}}_o,t({\mathsf{in}}_o)={\mathsf{in}}_e.$$ Normalizer stability gives ${\mathsf{in}}_e{\Downarrow }_{\mathsf{T}}{\mathsf{in}}_e$. The generated Block-comp branch contracts $t({\mathsf{in}}_e)$ to ${\mathsf{in}}_o$, and soundness, completeness, and stability give $t({\mathsf{in}}_e){\Downarrow }_{\mathsf{T}}{\mathsf{in}}_o$. Rule Coiter-Tail therefore derives $$\mathsf{tail}(\mathsf{coiter}(h,t,{\mathsf{in}}_e))\Downarrow \mathsf{coiter}(h,t,{\mathsf{in}}_o).$$

Take state $S=\mathbb{N}$, head method $h(n)=n$, and transition $t(n)=\mathsf{suc}n$. Then $\mathsf{from}(n)$ elaborates to $\mathsf{coiter}(h,t,n)$. On the source, $$\mathsf{from}(0){\Downarrow }_{{\mathsf{tail}}^3\mathsf{head}}3$$ by three uses of the tail equation, producing states $1,2,3$, followed by the head equation. On the target, three instances of the second coiterator rule and one head instance give Thus both finite observations return three.

The rank is $r(f)=2$, $r(g)=1$, $r(h)=0$, as computed in exercise 124.2. The only edge leaving $h$ is its tail step $h\stackrel{1}{\to }f$, and every directed cycle must leave $h$, because the zero subgraph $f\to g\to h$ has no edge out of $h$ and any cycle avoiding $h$ would have to return from $g$, which has no edge to $f$. So every cycle uses the positive edge $h\to f$.

For productivity, order demands by the pair consisting of the number of tail symbols in the observation word and the stored rank of the demanded function. A zero edge passes the same demand and strictly decreases the rank; a positive edge discharges one tail symbol, strictly decreasing the first component, after which the rank may reset freely. At $\mathsf{head}$, the demand at $f$ follows two zero edges to $h$ and returns the numeral $0$. At $\mathsf{tail}\cdot o^{\prime }$, one tail step moves to the next function with the strictly shorter demand $o^{\prime }$. Lexicographic induction on the pair therefore answers every finite observation word, in this group always with $0$.