A homogeneous set of some kind Let $f : \mathbb{N}^k \to \mathbb{N}$ be a computable total function such that $f (\vec{x}) > \max \vec{x}$ for all $\vec{x}$. 
Question. Why is there a decidable set $A$ such that $\operatorname{im} {\left. f \right|_{A^k}} = \mathbb{N} \setminus A$?

It feels like there should be an inductive process which gives the solution. Let $A_0 = \mathbb{N} \setminus {\operatorname{im} f}$. If there is such an $A$, then $A_0 \subseteq A$ for sure. Let for each natural number $n$, let $B_n = \mathbb{N} \setminus {\operatorname{im} f \big|_{{A_n}^k}}$ and $A_{n+1} = \mathbb{N} \setminus {\operatorname{im} f \big|_{{B_n}^k}}$. One can then show inductively that
$$A_0 \subseteq A_1 \subseteq A_2 \subseteq \cdots \subseteq B_2 \subseteq B_1 \subseteq B_0$$
Let $A = \bigcup_n A_n$ and $B_\infty = \bigcap_n B_n$. If $\vec{x} \in A^k$, then $\vec{x} \in {A_n}^k$ for some $n$, so $f (\vec{x}) \notin B_n$, hence $\vec{x} \notin B$. On the other hand, if $y \notin B$, then $y \notin B_n$ for some $n$, so there is some $\vec{x} \in {A_n}^k$ such that $f (\vec{x}) = y$, and $\vec{x} \in A^k$. Thus $\operatorname{im} f \big|_{A^k} = \mathbb{N} \setminus B$. So far so good.
Under the hypothesis, it's easy to see that $f$ maps decidable subsets of $\mathbb{N}^k$ to decidable subsets of $\mathbb{N}$. Thus, $A$ is semidecidable, and $B$ is co-semidecidable. If $A = B$ then it follows that $A$ is decidable... but is it true that $A = B$?
 A: We define $A$ as the union $\bigcup_s A_s$ of the finite approximations $A_s$. Start out at stage $0$ with $A_0=\{0\}$. Note that $f[A_0^k]=\{f(0,\ldots,0)\}$, and by assumption $f(0,\ldots,0)>0$, so $A_0$ is disjoint from $f[A_0^k]$. Suppose inductively that $A_s$ is defined and $f[A_s^k]$ is disjoint from $A_s$. Let $n_s$ be the least number not in $f[A_s^k]$ and let $A_{s+1}=A_s\cup\{n_s\}$. By induction, $n_s$ is larger than any element of $A_s$, since otherwise it would have been added at an earlier stage. From this, it follows that $f[A_{s+1}^k]$ is still disjoint from $A_{s+1}$, since any input not using $n_s$ is in $f[A_s^k]$ and hence not in $A_s\cup\{n_s\}$, and any input using $n_s$ is larger than $n_s$ and hence not in $A_{s+1}$. So we maintain the inductive hypothesis. 
Let $A=\bigcup_s A_s$. It follows that $f[A^k]$ is disjoint from $A$, but every element not in $f[A^k]$ was added at the stage when it became the least such element. Thus, $f[A^k]=\mathbb{N}-A$, as desired.
A: We prove by induction on $i$ that $A \cap [i] = B \cap [i]$, where $[i] = \{0,\ldots,i\}$. Since $0 \notin \operatorname{im} f$, we have $0 \in A \cap B$, proving the base case. 
Assume that $A \cap [i-1] = B \cap [i-1] = C$. If $i \in f(C^k)$ then $i \notin B$. Otherwise, $i \in A$. In both cases, $A \subseteq B$ implies $A \cap \{i\} = B \cap \{i\}$.
