NTM's and the halting problem It is often stated that nondeterministic Turing machines cannot recognize any more languages than ordinary Turing machines. In particular, it is stated that there is no NTM that can take as input a DTM/input string and state whether that DTM will halt.

Is this proven, or is this an assumption under the same banner as the Church-Turing thesis?

If it is proven, does anyone have any citations for this in the literature?
A nondeterministic Turing machine can be simulated using a deterministic Turing machine in exponential time (can be shown as a simple exercise). Furthermore, NDTM is a generalization of DTM. So, the computability powers of NDTMs and DTM are equal, in sense of decidability. So, the Halting problem is not decidable by a NDTM. However, their time complexity is different.