# Proof by padding: $\textsf{TIME}(t_1(n)) = \textsf{TIME}(t_2(n)) \implies \textsf{TIME}(t_1(f(n))) = \textsf{TIME}(t_2(f(n)))$

I've been given the task of proving the statement in the title, which I found out it should be called the translational lemma by means of a padding argument; $$f$$, $$t_1$$ and $$t_2$$ are three nondecreasing time-constructible functions in $$\mathbb{N} \to \mathbb{N}$$.

After much effort, I think I have an idea of how and why such a technique would be useful in proving complexity related statements: in a sense it "shifts" the time complexity of one language (or a given machine deciding it) into the input length of the "padded" language (or the machine specifically designed to decide it), which in turn makes it simpler(?), as in less time-consuming w.r.t. its input length.

I get the usual proof for the statement $$P = NP \implies EXP = NEXP$$ as it is found at page 57 in the Arora-Barak book and in Wikipedia's page about the padding argument; however I'm unable to concretely apply it to the presented statement. My proof tries to mimic the proof cited above, but stops in the middle:

Suppose $$L \in \textsf{TIME}(t_2(f(n))$$, thus there is a DTM $$M_{2, f}$$ deciding it. Define the following language:

$$L_{PAD} := \{\langle x \| \diamond^{t_2(f(|x|))} \rangle: x \in L\}$$

I claim that $$L_{PAD} \in \textsf{TIME}(t_2(|x|))$$.

Proof: Define $$M_2$$: On input $$y$$

check if $$y \equiv x \| \diamond^{t_2(f(|x|))}$$ for some $$x$$ (Time: $$O(|y|) \approx O(n + {t_2(f(|x|))})$$)

if not, reject (Time: $$O(1)$$)

else simulate $$M_{2, f}$$ (Time: $$O(t_2(f(|x|)))$$)

At this point though, I feel that the conclusion is that $$M_2$$ decides $$L_{PAD}$$ in linear time, as all the steps done by it are upper bounded by at most $$O(n + {t_2(f(|x|))})$$. I just can't manage to keep $$t_2$$ in, let alone keeping it while getting rid of $$f$$. I can see I'm doing it wrong, but no idea why.

I'm looking for anything that would help me on the Web, but the only proofs by padding that I find are done on specific cases, where the functions are actually defined, instead of being just generic, nondecreasing, and time-constructible. The only document I found with the same exact statement is this one at page 14, but it just states it as a lemma without proving it.

Did I get the padding idea correctly? What am I missing?