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.

Apply Nondeterministic recursive-padding separation to the exact clock $T$ from step 1.1. It gives a binary language $D\in \mathrm{N}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(T)$ under the local all-branch convention, but $D\mathrm{\notin }\mathrm{N}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(a)$ for every total recursive $a\ge n$ with $a(n+1)=o(T(n))$.

Since $T(n)=O(g(n))$, the all-branch $O(T)$ machine from step 2.1 is an all-branch $O(g)$ machine. Hence $D\in \mathrm{N}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(g)$.

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 the total recursive function $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.