Theorem: If $A$ and $B$ are regular, then $A \diamond B = \setbuilder{xy}{x \in A, y \in B \tand \abs{x} = \abs{y}}$ is context-free.

---

Proof: There are finite automatons $M_A$ and $M_B$ that recognize $A$ and $B$, respectively. Let the be deterministic, and write $P_A = (Q_A, \Sigma, \delta_A, q_{0A}, F_A)$ and $P_B = (Q_B, \Sigma, \delta_B, q_{0B}, F_B)$.

So, we construct a PDA for $A \diamond B$. The machine will work by progressing through $A$'s machine, pushing a counter on to the stack. Each time it hits one of $M_A$'s accepting states, it will make a non-deterministic guess that its passed the mid-point of the string, and spawn a thread transitioning to the starting state of $M_B$. It will then progress through $B$'s machine, popping the counters off the stack. If the machine is in a final state of $M_B$ when the stack is empty, it transitions to an accept state (of course, if there is more input, the thread that wound up in the accept state will terminate).

Let $P = (Q, \Sigma, \Gamma, \delta, q_0, F, Z_0)$, accepting by final state. Let $Q = Q_A \cup Q_B \cup \set{q_f}$ and $q_0 = q_{0A}$. Let $F = \set{q_f}$. Finally, let $\Gamma = \set{k, Z_0}$.

Now, we define $\delta$ as follows.

$$\delta(q, x, T) = \left\{ \begin{array}{lr} \set{(\delta_A(q, x), kT)} & x \neq \epsilon \tand q \in Q_A \\ \set{(\delta_A(q, x), kT), (q_{0B}, T)} & x = \epsilon \tand q \in F_A \\ \set{(\delta_B(q, x), \epsilon)} & x \neq \epsilon \tand q \in Q_B \\ \set{(\delta_B(q, x), \epsilon), (q_f, T)} & x = \epsilon \tand T = Z_0 \tand q \in F_B \end{array} \right.$$

Where conditions not written result in $\varnothing$. This machine accepts $A \diamond B$, so $A \diamond B$ is context free.