Kleene fixed point theorem for program indices

Compile a binary program q which on $(z,y)$ first computes $s(z,z)$, then evaluates f on that number, obtaining $F(s(z,z))$, then evaluates that index on y. F1 supplies the first terminating subroutine, totality of F the second, and F2 the possibly partial last evaluation. Thus its binary function is $H(z,y)\simeq {\phi }_{F(s(z,z))}(y)$. The finite compiler inserts f literally, so q is obtained effectively from f without running F during code generation.

Compute $e=s(q,q)$. For each y, specialization gives ${\phi }_e(y)\simeq H(q,y)\simeq {\phi }_{F(s(q,q))}(y)={\phi }_{F(e)}(y)$. The first two subcalls in H terminate, so either the last call halts with exactly the asserted value or both sides are undefined. This proves equality of the partial domains as well as values. Computing q and then e is a halting transformation of the given index f; if the promise of totality fails the transformation still produces a number, but the asserted fixed-point conclusion is not inferred.