ch:recursive-functions: ch:recursive-functions

In the first call, , so coordinate one is the decisive strict coordinate; the later increase is irrelevant and the call passes. In the second call, coordinate one is equal. If $n=0$, coordinate two is also equal and the call fails because no coordinate is strict. If $n=\mathsf{suc}k$, then , so coordinate two is decisive and the call passes. In the third call the proposed first coordinate $\mathsf{suc}(\mathsf{suc}m)$ is not smaller than the source coordinate $\mathsf{suc}m$; the lexicographic premise fails before the second coordinate is inspected.

The selected successor row gives $$\mathsf{even}(\mathsf{suc}n)\stackrel{R-Call}{{⇝}_0}\mathsf{odd}(n).$$ Write $F_S$ for the compiled well-founded definition on ${\mathsf{State}}_S$. At program granularity the corresponding target contraction is $$F_S({\mathsf{in}}_{\mathsf{even}}(\mathsf{suc}n))\stackrel{C-Call}{{⇝}_0}{F}_S({\mathsf{in}}_{\mathsf{odd}}(n)).$$ To expose the raw proof arguments, write $W_S[x;p]$ for the internal accessibility worker at $p:{\mathsf{Acc}}_{R_S}(x)$. The accepted proof at the source state has the form $\mathsf{acc}({\alpha }_{\mathsf{even},\mathsf{suc}n})$, where ${\alpha }_{\mathsf{even},\mathsf{suc}n}(y,p)$ is the stored accessibility proof for the predecessor $p:y{R}_S{\mathsf{in}}_{\mathsf{even}}(\mathsf{suc}n)$. Let ${\mathsf{E}}_S$ denote the generated state eliminator, and abbreviate $$p_{\mathsf{suc}}:={\mathsf{child}}_{\mathsf{suc}}(n,\mathsf{suc}n),k_{\alpha }:=\lambda y.\lambda p.W_S[y;{\alpha }_{\mathsf{even},\mathsf{suc}n}(y,p)].$$ The complete administrative prefix is Here $\overrightarrow{b}$ is the finite tuple of generated state branches, and its even-successor component is the displayed worker. The final line is what the program-level notation $F_S({\mathsf{in}}_{\mathsf{odd}}(n))$ denotes inside this selected branch; its accessibility argument is frozen evidence. The named ${\mathsf{DChild}}_{\mathbb{N}}$ proof is exactly ${\mathsf{child}}_{\mathsf{suc}}(n,\mathsf{suc}n)$. Thus the displayed sequence contains the outer beta contractions, generated state-block equation, accessibility recursor redex, WF-$\beta$, and all administrative beta contractions licensed by C-Call.

Use ${\mathsf{State}}_S$ with constructors ${\mathsf{in}}_{\mathsf{even}}(n)$ and ${\mathsf{in}}_{\mathsf{odd}}(n)$. Its relation has the two predecessor families $${\mathsf{in}}_{\mathsf{odd}}(n)R_S{\mathsf{in}}_{\mathsf{even}}(\mathsf{suc}n),{\mathsf{in}}_{\mathsf{even}}(n)R_S{\mathsf{in}}_{\mathsf{odd}}(\mathsf{suc}n).$$ Both are witnessed by ${\mathsf{child}}_{\mathsf{suc}}(n,\mathsf{suc}n)$. With $k$ the recursive hypothesis, the four step bodies are $$\mathsf{tt},k({\mathsf{in}}_{\mathsf{odd}}(n),{\mathsf{child}}_{\mathsf{suc}}),\mathsf{ff},k({\mathsf{in}}_{\mathsf{even}}(n),{\mathsf{child}}_{\mathsf{suc}}),$$ in the order even-zero, even-successor, odd-zero, odd-successor. Writing $F_S$ for the compiled recursor, its calculation is The first two steps consume the two displayed $R_S$-predecessor proofs; the last selects the even-zero body.

The changed clause emits the self-edge $${\mathsf{in}}_{\mathsf{odd}}(\mathsf{suc}n)⟶{\mathsf{in}}_{\mathsf{odd}}(\mathsf{suc}n).$$ The call supplies $\mathsf{suc}n$ again at the named position. By definition 123.3, that term is not a direct constructor child of itself, so no predecessor certificate exists. At $n=0$, source evaluation repeats $$\mathsf{odd}(\mathsf{suc}0){⇝}_0\mathsf{odd}(\mathsf{suc}0){⇝}_0\mathsf{odd}(\mathsf{suc}0){⇝}_0\cdots .$$ The failed certificate and the infinite trace expose the same unguarded self-edge.