A nondeterministic time hierarchy was first proved by Cook and in the strongest form by Seiferas, Fischer and Meyer. Zàk gave a simple proof that we sketched in this post. Here is another.
Theorem: If t1 and t2 are time-constructible functions and t1(n+1)=o(t2(n)) then NTIME(t1(n)) is strictly contained in NTIME(t2(n)).
Let M1,… be an enumeration of nondeterministic Turing machines. We define a nondeterministic machine M that acts as follows on input w=1i01m0y
- If |y|<t1(i+m+2) then accept if Mi accepts both inputs 1i01m0y0 and 1i01m0y1 in t2(|w|) steps.
- If |y|=t1(i+m+2) then accept if Mi rejects input 1i01m0 on the computation path described by y.
This machine uses time O(t2(n)). If NTIME(t1(n))=NTIME(t2(n)) then there is an equivalent machine Mi using time O(t1(n)).
Since t1(n+1)=o(t2(n)) we have for sufficiently large m,
The advantage over Zàk is that you only need t1 steps instead of exponential in t1. On the other hand Zàk can give you a unary language and can be generalized to a broader set of complexity measures.
Rahul Santhanam and I needed and discovered this proof for our recent paper. The proof came out of a failed attempt at an oracle to show that no such relativized proof would be possible.