A non-uniformly C-productive sequence & non-constructive disjunctions

Let φ be an acceptable programming system/numbering of the partial computable functions: ℕ = {0; 1; 2; …} →ℕ, where, for p ∈ ℕ N, φ_p is the partial computable function computed by program p of the φ-system and W_p = domain(φ_p). Wp is, then, the computably enumerable (c.e.) set accepted by p. The first author taught in a class a recursion theorem proof employing a pair of cases that, for each q, {x | φ_x = φ_q} is not computably enumerable. The particular pair of cases employed was: domain(φ_q) is infinite vs. finite - incidentally, by Rice's Theorem, a non-constructive disjunction. Some student asked why the proof involved an analysis by cases. The answer given straightaway to the student was that his teacher didn't know how else to do it. The present paper provides, among other things, a better answer: any proof that, for each q, {x | φ_x = φ_q} is not c.e. provably must involve some such non-constructiveness. Furthermore, completely characterized are all the possible such pairs of (index set based) cases that will work. Along the way, relevantly explored are uniform lifts of the concept completely productive (abbr: c-productive) sets to sequences of sets. The c-productive sets are the effectively non-c.e. sets. A set sequence S_q, q ∈ ℕ, is said to be uniformly c-productive iff there is a computable f so that, for all q, x, f(q, x) is a counterexample to S_q = W_x. Relevance: a completely constructive proof that each S_q is not c.e. would entail the Sqs forming a uniformly c-productive sequence. Relevantly shown, then, is that the sequence {x | φ_x = φ_q}, q ∈ ℕ, is not uniformly c-productive | and this even though, of course, the set {‹q, x›| φ_x = φ_q} is c-productive. For some results we provide upper and/or lower bounds for them as to position in the Arithmetical Hierarchy of the Law of Excluded Middle needed in addition to Heyting Arithmetic. Results are also obtained for similar problems, including for run-time bounded programming systems and other subrecursive systems. Proof methods include recursion theorems.