ch:well-founded-recursion: ch:well-founded-recursion

Fix $q:aRa$. Define $F:{\mathsf{Acc}}_R(a)\to \mathbf{0}$ by structural induction on its accessibility-certificate argument. In its sole case, $$F({\mathsf{acc}}_a(h)):=F(haq).$$ The displayed recursive call is on the immediate accessibility proof $haq:{\mathsf{Acc}}_R(a)$ stored by the constructor. Thus a hypothetical $p:{\mathsf{Acc}}_R(a)$ gives $F(p):\mathbf{0}$. This is the proof-dependent eliminator of definition 82.4, with a motive over the certificate at the fixed index $a$. Its nondependent specialization with $P(x):=\mathbf{0}$ would demand a step producing $\mathbf{0}$ at every $x:A$; the single proof $q:aRa$ cannot supply those other cases. The construction does not inspect or decide $R$; it uses $q$ only at the fixed index.

Define $\rho (a,b)=\mu (a)+\nu (b)$. If and , monotonicity and transitivity of addition give Hence the relation is contained in and is well founded by theorem 82.14: an accessibility proof for the larger measure relation restricts to one for the smaller relation. It is also contained in the lexicographic relation because its first coordinate decreases. The containment can be strict: a lexicographic predecessor may decrease $\mu$ while increasing $\nu$, whereas the relation in the exercise requires both coordinates to decrease.

The complete calculation is Thus the second-coordinate measure sequence is .

Partitioning the tail gives $|l|+|r|=|xs|$. Therefore These are the two certificates for the recursive calls on $l$ and $r$. If the pivot is not removed and the partition equation instead accounts for the entire input, one side may have the full input length and the other length zero. The equation then yields only a non-strict inequality for that side, so it cannot justify the corresponding recursive call.

For $p\equiv {\mathsf{acc}}_a(h)$, the constructor field has type $$h:\prod _{b:A}bRa\to {\mathsf{Acc}}_R(b).$$ The induction hypothesis applied to $hbr$ gives a result in $P(b)$. After abstraction, the step receives $$k:=\lambda b.\lambda r.{\mathsf{accind}}_P(s,b,hbr):\prod _{b:A}bRa\to P(b).$$ Taking $P(a):=\mathbb{N}$ gives $s(a,k):\mathbb{N}$, and the constructor computation rule is $${\mathsf{wfrec}}_{R,P}(s,a,{\mathsf{acc}}_a(h))\equiv s(a,\lambda b.\lambda r.{\mathsf{wfrec}}_{R,P}(s,b,hbr)).$$ Every recursive call is therefore indexed by both a predecessor $b$ and its proof $r:bRa$.

Put when either $a^{\prime }Ra$, or $a^{\prime }=a$ and $b^{\prime }Sb$, or $a^{\prime }=a$, $b^{\prime }=b$, and $c^{\prime }Tc$. Induct first on the $R$-accessibility of $a$, with all $b,c$ quantified. Inside that case, induct on the $S$-accessibility of $b$, with all $c$ quantified; inside that case, induct on the $T$-accessibility of $c$. For a predecessor, the first disjunct uses the outer induction hypothesis and leaves $b^{\prime },c^{\prime }$ unrestricted. The second uses the middle hypothesis and leaves $c^{\prime }$ unrestricted after transporting along $a^{\prime }=a$. The third uses the inner hypothesis after transporting along $a^{\prime }=a$ and $b^{\prime }=b$. These three clauses form the predecessor function for ${\mathsf{acc}}_{(a,b,c)}$.