So I'm looking at the proof of the ZBC lemma in Odifreddi's Classical Recursion Theory volume 2 page 808 and I don't see why $ 0' \oplus C$ produced computes $B'$ as claimed. The positive requirements try and code 
$$
P^C\_e: \; x \in C^{[e]} \iff (\exists z > x) B^{[e]}(x) \not= B^{[e]}(z)
$$


Now if these requirements always succeeded we would be great. We could read off from $C^{[e]}$ the point at which $B^{[e]}$ achieved its limit and from that compute $W$ which in turn computes $B'$. However, higher priority negative requirements might restrain $P^C\_e$ from acting. These requirements have the form.
$$
N^C\_e : \; (\exists\_\infty s)(\phi^{B\oplus C\_s}\_{e,s}(e)\downarrow) \implies \phi^{B\oplus C}\_{e}(e)\downarrow
$$


However, since $B$ isn't low we can't guarantee that $0'$ can tells us whether or not such a higher priority negative requirement might be falsely resulting in $C^{[e]}(x)=0$ so how do we actually conclude that $B' \leq\_T 0' \oplus C$?




---


While I'm at it am I correct in presuming that the only reason that one can assume we meet the negative requirement for $B$ is that we assumed $C$ meets its own negative requirements above. This almost makes me think the right proof would build them simultaneously so they satisfied a requirement more like 


$$
N^C\_e : \; (\exists\_\infty s)(\phi^{B^{e}\_s\oplus C\_s}\_{e,s}(e)\downarrow) \implies \phi^{B\oplus C}\_{e}(e)\downarrow
$$


where 
$$B^{e}\_s(x) = \begin{cases}
B(x) & \text{ if } x = <i,y> \land i \leq e \\
B\_s(x) & \text{ otherwise }
\end{cases}
$$


That way one could get some kind of induction off the ground where $0'$ would be able to determine if the next negative requirement ever engaged using the knowledge of $B'$ restricted to $e$. Or is there some easier trick I'm missing?




---


Note that the reason I'm interested is that I wanted to see if I could extend the ZBC theorem so that given r.e. set $A$ and set $W$ r.e. in $A$ it produced $B, C$ with $B \oplus C \leq\_T A \oplus W$ and $(B \oplus C)' \equiv\_T 0'\oplus B \oplus C \equiv\_T 0' \oplus W$. So thoughts about that are appreciated as well.



Correct Proof Of ZBC Theorem From Odifreddi? Also Extension Question
A proof of Harrington’s ZBC Lemma can be found in Theorem 2.5 of 


*Hinman, Peter G.; Slaman, Theodore A.*, [**Jump embeddings in the Turing degrees**](http://dx.doi.org/10.2307/2274700), J. Symb. Log. 56, No. 2, 563-591 (1991). [ZBL0745.03036](https://zbmath.org/?q=an:0745.03036).


It [consists](https://math.berkeley.edu/~antonio/papers/GHembpdf.pdf) of a finite injury construction on top of an infinite
injury construction. So it sounds like you're on the right track.


