User:IssaRice/Computability and logic/First graph principle using a semirecursive relation

This is about proposition 7.17 (first graph principle) in Boolos, Burgess, Jeffrey's Computability and Logic.

The proof in the book defines two functions as follows:

$g(x)={\begin{cases}{\text{the least }}w{\text{ such that}}\\\quad \exists y<w\;\exists z<w\;Sxyz&{\text{if such a }}w{\text{ exists}}\\{\text{undefined}}&{\text{otherwise}}\end{cases}}$

$h(x,w)={\begin{cases}{\text{the least }}y<w{\text{ such that}}\\\quad \exists z<w\;Sxyz&{\text{if such a }}y{\text{ exists}}\\{\text{undefined}}&{\text{otherwise}}\end{cases}}$