Proving specific prefixes of regular languages are regular There are particular problems in Kozen that I'm unable to solve, and they seem to be similar to each other. It is showing that sets:

$$ \{x \mid \exists y: |y| = 2^{|x|} \text{ and } xy \in A \}$$
$$ \{x \mid \exists y: |y| = |x|^2 \text{ and } xy \in A \}  $$

are regular for a regular set $A$.
The only method I'm familiar with that is similar is proving that first-halfs or first-thirds or any other linear parts of a regular language are regular (using a 2-NFA). I've tried looking online, but I only found that it's hard to construct NFAs for that. Is there some other way of proving existence?
I also don't understand how we can even compute $|x|^2$ or $2^{|x|}$ for different strings in the language to use that value.
Basically, you do not compute these lengths $2^n$ or $n^2$, but only the from-to computations that the automaton would be able to make on input with this particular lengths.

For the first two problems the automaton computes (in its internal states) the relation $E_\ell = \{ (p,q)\in Q\times Q \mid q\in\delta^*(p,y) \text{ for some $y$ with $|y|=\ell$} \}$ for some value of $\ell$ (which depends on $|x|$).

Then $E_{2\ell}=E^2_\ell$ which helps to solve the first problem. Here $E^2$ is the composition $E\circ E$ of the binary relation $E$ with itself: $E^2 = \{ (p,r) \mid \text{ for some } q\in Q \text{ both } (p,q)\in E \text{ and } (q,r)\in E\}$

I add some details. This is still rather formal, without much intuition. I hope it helps you into the right direction.

Assume we are given a FSA $\mathcal  A= (Q,\Sigma,\delta,q_0,F) $ for language $A$. We will construct an automaton for your first problem.

The new states are of the form $(p,E)$ where $p\in Q$ and $E\subseteq Q\times Q$; i.e., the new state set equals $Q\times{\mathcal P}(Q\times Q)$.
Note that the number of possible relations $E$ is finite, hence adding such a relation to the states of the automaton will still lead to a finite state automaton.
The second component will always contain the relation $E_{2^n}$ where $n$ is the length of the input read.

The initial state equals $(q_0,E_1)$, where $E_1$ is the one-step relation on $Q$, just like defined above.

Now from every $(p,E)$ reading letter $a$ we move to state $(\delta(p,a),E^2)$. Thus, the first component copies the original move in $\mathcal A$, the second component steps from $E_{2^n}$ to $E_{2^n}\circ E_{2^n}=E_{2^{n+1}}$ following the recipe above.

When is a state $(p,E)$ final? When there is a pair $(p,q)\in E$ such that $q\in F$ is final in $\mathcal A$.   

The $n^2$ problem is along similar lines, but actually slightly more involved (I think). It uses the fact that $(n+1)^2 = n^2 + 2n +1$. The automaton stores both $E_{n^2}$ and $E_{n}$ to easily update the square.