Editing Time hierarchy theorem (section)

===Proof===
We include here a proof of a weaker result, namely that '''DTIME'''(''f''(''n'')) is a strict subset of '''DTIME'''(''f''(2''n'' + 1)<sup>3</sup>), as it is simpler but illustrates the proof idea. See the bottom of this section for information on how to extend the proof to ''f''(''n'')log''f''(''n'').

To prove this, we first define the language of the encodings of machines and their inputs which cause them to halt within f

: <math> H_f = \left\{ ([M], x)\ |\ M \ \text{accepts}\ x \ \text{in}\ f(|x|) \ \text{steps} \right\}. </math>

Notice here that this is a time-class. It is the set of pairs of machines and inputs to those machines (''M'',''x'') so that the machine ''M'' accepts within ''f''(|''x''|) steps.

Here, ''M'' is a deterministic Turing machine, and ''x'' is its input (the initial contents of its tape). [''M''] denotes an input that encodes the Turing machine ''M''. Let ''m'' be the size of the tuple ([''M''], ''x'').

We know that we can decide membership of ''H<sub>f</sub>'' by way of a deterministic Turing machine ''R'', that simulates ''M'' for ''f''(''x'') steps by first calculating ''f''(|''x''|) and then writing out a row of 0s of that length, and then using this row of 0s as a "clock" or "counter" to simulate ''M'' for at most that many steps. At each step, the simulating machine needs to look through the definition of ''M'' to decide what the next action would be. It is safe to say that this takes at most ''f''(''m'')<sup>3</sup> operations (since it is known that a simulation of a machine of time complexity ''T''(''n'') for can be achieved in time <math>O(T(n)\cdot|M|)</math> on a multitape machine, where |''M''| is the length of the encoding of ''M''), we have that:

: <math> H_f \in \mathsf{TIME}\left(f(m)^3\right). </math>

The rest of the proof will show that

: <math> H_f \notin \mathsf{TIME}\left(f\left( \left\lfloor \frac{m}{2} \right\rfloor \right)\right) </math>

so that if we substitute 2''n'' + 1 for ''m'', we get the desired result. Let us assume that ''H<sub>f</sub>'' is in this time complexity class, and we will reach a contradiction.

If ''H<sub>f</sub>'' is in this time complexity class, then there exists a machine ''K'' which, given some machine description [''M''] and input ''x'', decides whether the tuple ([''M''], ''x'') is in ''H<sub>f</sub>'' within

:<math>\mathsf{TIME}\left(f\left( \left\lfloor \frac{m}{2} \right\rfloor \right)\right). </math>

We use this ''K'' to construct another machine, ''N'', which takes a machine description [''M''] and runs ''K'' on the tuple ([''M''], [''M'']), ie. M is simulated on its own code by ''K'', and then ''N'' accepts if ''K'' rejects, and rejects if ''K'' accepts.

If ''n'' is the length of the input to ''N'', then ''m'' (the length of the input to ''K'') is twice ''n'' plus some delimiter symbol, so ''m'' = 2''n'' + 1. ''N'''s running time is thus

:<math> \mathsf{TIME}\left(f\left( \left\lfloor \frac{m}{2} \right\rfloor \right)\right) = \mathsf{TIME}\left(f\left( \left\lfloor \frac{2n+1}{2} \right\rfloor \right)\right) = \mathsf{TIME}\left(f(n)\right). </math>

Now if we feed [''N''] as input into ''N'<nowiki/>''  and ask the question whether ''N'' accepts its ''N''' description as input, we get:

* If ''N'' accepts' [''N'<nowiki/>'''''<nowiki/>''' ] (which we know it does in at most f(n) operations since K halts on ([''N'' ], [''N'<nowiki/>'''''<nowiki/>''']) in f(n) steps), this means that K rejects ([''N'<nowiki/>''], [''N'<nowiki/>'']), so ([''N''], [''N'<nowiki/>'']) is not in ''H<sub>f</sub>'', and so by the definition of ''H<sub>f</sub>'', this implies that ''N'' does not accept [''N'<nowiki/>''] in ''f''(''n'') steps. Contradiction.

* If N rejects' [''N'<nowiki/>''] (which we know it does in at most f(n) operations), this means that K accepts ([''N'<nowiki/>''], [''N'<nowiki/>'''''<nowiki/>''']), so ([''N'' ], [''N'<nowiki/>'']) is in ''H<sub>f</sub>'', and thus ''N'' does accept [''N'<nowiki/>''] in ''f''(''n'') steps. Contradiction.

We thus conclude that the machine ''K'' does not exist, and so
: <math> H_f \notin \mathsf{TIME}\left(f\left( \left\lfloor \frac{m}{2} \right\rfloor \right)\right). </math>