ch:dependent-partiality: partiality

For $x={▹}^3⟨7⟩$, The convergence derivation is Conv-Return followed by three applications of Conv-Step. A result $\mathsf{later}$ describes only the inspected prefix. Even $\mathsf{done}(7)$ is a proof of convergence rather than a proof about the absence of all values. Hence none of the first three finite observations establishes the universal negation that defines divergence.

Take $x=▹\xi$, where $\xi :A^{\nu }$ is neutral. One unfolding of the left side exposes $$((▹\xi \gg =f)\gg =g)\equiv ▹((\xi \gg =f)\gg =g),$$ whereas the right side exposes $$▹\xi \gg =(\lambda a.f(a)\gg =g)\equiv ▹(\xi \gg =(\lambda a.f(a)\gg =g)).$$ Their guarded subterms are distinct raw syntax; identifying them would assume the associativity being proved. For every $c:C$, bind convergence gives The middle equivalence only reassociates the two existential witnesses and the conjunctions. Pointwise equivalence is exactly ${=}_{\nu }$.

No natural square equals two. For $k=0,1$, ; for $k\ge 2$, monotonicity of multiplication gives . Therefore $P(k)=\mathsf{false}$ for every $k$, so no $m$ can satisfy the $P(m)=\mathsf{true}$ conjunct in the right side of theorem 105.9.

Induct on the fuel $j$. At zero the observer returns $\mathsf{later}$. At $j+1$, the predicate test at the current index is false, so search exposes one $\mathsf{step}$; consuming one unit of fuel reduces the claim to the induction hypothesis at the successor index. Thus every finite observation is $\mathsf{later}$. This proof uses the particular decidable arithmetic predicate; it does not invoke a general decision law for convergence.

For the forward direction of bind convergence, induction on the convergence derivation has two inversions. If the input is $⟨a⟩$, unfold bind and choose $a$; Conv-Return gives input convergence. If the input is $▹x^{\prime }$, inversion of the outer Conv-Step reduces the premise to $(x^{\prime }\gg =f)\Downarrow b$; apply the induction hypothesis and rebuild input convergence with Conv-Step. Conversely, induction on $x\Downarrow a$ uses Conv-Return to unfold bind to $f(a)$, and uses Conv-Step plus the guarded bind equation in the step case.

Now assume $x{=}_{\nu }y$ and $f(a){=}_{\nu }g(a)$ for every $a$. For each $b$, The outer equivalences are bind convergence; the middle one uses the two pointwise equality hypotheses. This is the required congruence at ${=}_{\nu }$.

Define the delayed subtraction program by Use the measure $\mu (m,n)=m+n$. In the first recursive branch, because , including the equality case $m=n$, which takes one step to $(0,n)$. In the second, because . Well-founded induction on $\mu$ therefore supplies a convergence derivation in every input case; each recursive induction hypothesis is lifted once by Conv-Step. For the corpus input, the exact trace is $$(6,4)⟼(2,4)⟼(2,2)⟼(0,2),$$ so the returned two occurs below three guarded steps. Adding an immediate $m=n$ return changes this observation and is not the displayed program.

Determinacy of convergence extracts a unique natural $d$. The subtraction equalities are $\gcd (m,n)=\gcd (m-n,n)$ for and $\gcd (m,n)=\gcd (m,n-m)$ for . The second is obtained from the first by swapping $m$ and $n$. Induction on $m+n$, using the corresponding equality in each strict-order branch, gives $d=\gcd (m,n)$. An accessibility definition packages the well-founded proof as an argument and returns $d:\mathsf{Nat}$ directly. The delayed definition is accepted by guardedness before totality is proved and returns ${\mathsf{Nat}}^{\nu }$; its separate convergence proof is what permits extraction of the same total value.