The nondeterministic time hierarchy theorem

Construct a deterministic unary-input clock as follows: read its input, compute the binary value $g(n)$ with the fixed constructor, and perform $g(n)$ countdown iterations before halting. A least-significant-bit-first binary counter has linear total decrement cost (the numbers of bit changes form a geometric sum); returning its head after each decrement has the same bound. Thus the clock's actual running time $T(n)$ is $\mathrm{\Theta }(g(n))$ eventually, and can be arranged to be at least $n$ for every $n$. It is an exact running time in the terminology of Seiferas--Fischer--Meyer, even though $g$ was supplied only by an asymptotically bounded binary-output constructor.

Use the first corollary to Seiferas--Fischer--Meyer Theorem 4 (the identity-function case, p. 155): for an exact running time $T$, there is a binary language $D$ accepted within $T$ but outside every acceptance-time class with bound $a$ satisfying $a(n)\ge n$ and $a(n+1)=o(T(n))$. Here acceptance time means the length of a shortest accepting branch, and nonmembers have no accepting branch. This is the external separation result being invoked.

In particular, $D$ has an acceptor with an accepting branch of length at most $T(n)$ on each member. Run that fixed acceptor with the fixed unary clock from step 1.1 on separate tapes, interleaving one transition of each per round, and reject if the clock expires without acceptance. This preserves the language and forces every branch to halt within $O(T(n)+n)=O(g(n))$. The product machine has fixed finite control; this is direct clocking, not a claim of linear universal simulation. Hence $D\in \mathrm{N}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(g)$ under the local all-branch convention.

If $D$ belonged to local $\mathrm{N}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(f)$, a constant integer $C$ would bound its accepting times at every length by $a(n)=\max \{n,Cf(n),C\}$: enlarge $C$ to cover the finitely many exceptional lengths. Since $f(n)\ge n$ eventually, $a(n+1)=O(f(n+1))=o(g(n))=o(T(n))$. This contradicts the exclusion in step 2.1. Thus $D\mathrm{\notin }\mathrm{N}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(f)$.

Nondecreasing $f$ gives $f(n)\le f(n+1)=o(g(n))$, so every all-branch $O(f)$ decider is an all-branch $O(g)$ decider. Together with steps 3.1 and 3.2 this proves the strict inclusion.