Yes. This definition is equivalent to the one about being verifiable in polynomial time, since your non-deterministic TM can just have a different branch for every possible verification "oracle".
> I think the more practical definition is "not polynomial"...lol.
Well, there are non-polynomial algorithms harder than NP. If a solution can't even be verified efficiently, for example.
- If you walk backwards from where the non-deterministic Turing machine halted, the list of taken state machine transitions is polynomial in length (naturally, as the machine stopped in polynomial time).
- Walking that polynomial length list of actually-taken edges forward through the Turing machine constitutes a polynomial time verification of the solution.
This is the essence of the equivalence between being able to solve problems in NP in polynomial time on a (hypothetical) non-deterministic Turing machine and being able to deterministically verify a solution to those problems in polynomial time.
> - Walking that polynomial length list of actually-taken edges forward through the Turing machine constitutes a polynomial time verification of the solution.
These are really great explanations that would've saved me so much trouble in graduate school. Connecting the automata itself to the term "nondeterministic turing machine" is something that is sorely missed is most CS programs I think. It's usually handwaved in automata theory in order to give you enough to head to compilers. Then you run into it again in graduate school algorithms where it is once again handwaved (because not even the professor fully understands it).