PDA fragment variables compose

Assume $x\in [p,Z,r]$ and $y\in [r,Y,q]$, and let $\alpha$ be any stack suffix. Then [L1] gives $(p,x,ZY\alpha ){⊢}_M^{\ast }(r,\epsilon ,Y\alpha )$ and also $(r,y,Y\alpha ){⊢}_M^{\ast }(q,\epsilon ,\alpha )$. Concatenating these two computations yields $(p,xy,ZY\alpha ){⊢}_M^{\ast }(q,\epsilon ,\alpha )$.

Conversely, let $(q,v,\alpha )$ be the first configuration with stack $\alpha$ in a computation starting at $(p,w,ZY\alpha )$. Before that point there is a first configuration whose stack is $Y\alpha$; write it as $(r,yv,Y\alpha )$ and write $w=xyv$, where $x$ is the input prefix consumed before it is reached and $y$ is consumed between the two first-exposure configurations. The computation therefore contains $(p,xyv,ZY\alpha ){⊢}_M^{\ast }(r,yv,Y\alpha ){⊢}_M^{\ast }(q,v,\alpha )$. Neither segment inspects the suffix $\alpha$ before its endpoint. Hence the same transition sequences work above every stack suffix $\beta$, giving $(p,x,Z\beta ){⊢}_M^{\ast }(r,\epsilon ,\beta )$ and $(r,y,Y\beta ){⊢}_M^{\ast }(q,\epsilon ,\beta )$. By [L1], $x\in [p,Z,r]$ and $y\in [r,Y,q]$.

Therefore fragment computations compose exactly by concatenating the consumed words and, conversely, by splitting at the first moment when the lower stacked symbol is exposed.