In Hromkovič's Algorithmics for Hard Problems (2nd edition) there is this theorem (2.3.3.3, page 117):
There is a (decidable) decision problem $P$ such that for every algorithm $A$ that solves $P$ there is another algorithm $A'$ that also solves $P$ and additionally fulfills
$\qquad \forall^\infty n \in \mathbb{N}. \mathrm{Time}_{A'}(n) = \log_2 \mathrm{Time}_A(n)$
$\mathrm{Time}_A(n)$ is the worst-case runtime of $A$ on inputs of size $n$ and $\forall^\infty$ means "for all but finitely many".
A proof is not given and we have no idea how to go about this; it is quite counter-intuitive, actually. How can the theorem be proven?