Deterministic time hierarchy theorem

Statement

Existential version

Suppose $f$ is a time-constructible function. Then, there exists a deterministic time complexity class that is strictly larger than $DTIME(f(n))$. The explicit description of this depends on the choice of model of computation that we are using to define $DTIME$.

Explicit version

With a suitable model of computation, we can show that $DTIME(f(n))$ is strictly contained in $DTIME(f(n)\log f(n))$.

Proof

The key idea behind the proof is the diagonalization argument.