Page 258

		(b) , and

		(c) for all with and , we have that .

		We refer to  s  as an OATxtEx-locking sequence for M on L.

		Proof (of Proposition 11.15): Define

		, and

		.

		11.17 Claim .

		Proof: We first note that by the s-m-n theorem (Theorem 2.1) there are recursive functions g0 and g1 such that for all i and j:

		Consider the following oracle scientist (with oracle X).

		Program for MX on  s  If for some and some nonempty , then output 0 and halt. Otherwise: Let i and D be such that If then output g0(i) else output g1(i, j), where j is the canonical index of D.

		End Program

		We leave it as an exercise to show that MB TxtEx-identifies .

		11.18 Claim .

		Proof: Suppose by way of contradiction that there is an M that OCTxtEx-identifies. We show that

		Suppose i is such that Ai is finite. Then by our definition of , Thus, by Lemma 11.16 there is an OCTxtEx-locking sequence for M on .