Every PDA has an equivalent context-free grammar

By [L1], replace $M$ by an equivalent empty-stack PDA $M^{\mathrm{\prime }}$. Refining its transitions if necessary, we may assume that every move of $M^{\mathrm{\prime }}$ pops one symbol, reads either one input symbol or $\epsilon$, and pushes either nothing, one symbol, or two symbols; a longer push is replaced by a short chain of fresh intermediate states.

Build a grammar $G_M$ whose variables are the fragment symbols $[p,Z,q]$ for states $p,q$ and stack symbols $Z$, and whose start symbol branches over all variables $[q_0,Z_0,q]$. For each normalized transition $(r,\beta )\in \delta (p,a,Z)$ of $M^{\mathrm{\prime }}$ with $a\in \mathrm{\Sigma }\cup \{\epsilon \}$, add the matching productions: if $\beta =\epsilon$, add $[p,Z,r]\to a$; if $\beta =Y$, add $[p,Z,q]\to a[r,Y,q]$ for every state $q$; if $\beta =YW$, add $[p,Z,t]\to a[r,Y,s][s,W,t]$ for every pair of states $s,t$. When $a=\epsilon$, omit that leading terminal.

Every derivation in $G_M$ yields an accepting computation of $M^{\mathrm{\prime }}$ by induction on the derivation tree of a fragment variable $[p,Z,q]$. The production chosen at the root records the first normalized move from state $p$ with top symbol $Z$. If the production is terminal or $\epsilon$, that move already removes $Z$. If it has one fragment variable, the induction hypothesis supplies the computation removing the pushed symbol. If it has two fragment variables, the induction hypotheses supply computations removing the two pushed symbols, and [L3] composes them into one computation removing the original pushed pair. Therefore every word derived from $[p,Z,q]$ lies in that fragment language, and the start productions give $L(G_M)\subseteq N(M^{\mathrm{\prime }})$.

Conversely, consider a fragment computation $(p,w,Z\alpha ){⊢}_{M^{\mathrm{\prime }}}^{\ast }(q,\epsilon ,\alpha )$ and induct on its number of steps. Let its first normalized move be determined by a transition $(r,\beta )\in \delta (p,a,Z)$ with $a\in \mathrm{\Sigma }\cup \{\epsilon \}$ and $\beta \in \{\epsilon ,Y,YW\}$. If $\beta =\epsilon$, that one move already removes $Z$, so step 2.1 contributes the corresponding terminal or $\epsilon$ production. If $\beta =Y$, the remaining computation removes $Y$ above $\alpha$, so the induction hypothesis derives the remaining input from $[r,Y,q]$, and step 2.1 prepends the production $[p,Z,q]\to a[r,Y,q]$ with the leading terminal omitted when $a=\epsilon$. If $\beta =YW$, then [L3] splits the remaining computation at the first moment when $W$ is exposed on top of $\alpha$, yielding a state $s$ and a decomposition of the remaining input into words $u$ and $v$ with $(r,u,YW\alpha ){⊢}_{M^{\mathrm{\prime }}}^{\ast }(s,v,W\alpha )$ and $(s,v,W\alpha ){⊢}_{M^{\mathrm{\prime }}}^{\ast }(q,\epsilon ,\alpha )$. The induction hypothesis derives $u$ from $[r,Y,s]$ and $v$ from $[s,W,q]$, so step 2.1 gives a derivation of $w$ from $[p,Z,q]$. Applying this to start configurations shows $N(M^{\mathrm{\prime }})\subseteq L(G_M)$.

Steps 3.1 and 3.2 give $L(G_M)=N(M^{\mathrm{\prime }})$, and [L1] then yields $L(G_M)=T(M)$.