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{array}{c}w\text{ such that}\\ \mathrm{\exists }y<w\mathrm{\exists }z<wSxyz& w\text{ exists}\\ & \end{array}$

$h(x,w)=\{\begin{array}{c}y<w\text{ such that}\\ \mathrm{\exists }z<wSxyz& y\text{ exists}\\ & \end{array}$