CFG universality is undecidable

Choose the explicit finite configuration alphabet allowed by [L2], and encode a candidate history as $C_0\mathrm{\#}{C}_1^R\mathrm{\#}{C}_2\mathrm{\#}{C}_3^R\mathrm{\#}\cdots ,$ alternating ordinary and reversed configuration words. Let $B_{M,w}$ be the set of words that are not accepting histories in this encoding. Malformed words and words with the wrong initial or accepting endpoint form regular languages. For an alleged adjacent pair $C_i,C_{i+1}$, a pushdown automaton nondeterministically chooses that pair, pushes the first configuration, and compares it with the oppositely oriented second configuration while allowing exactly one of the finitely many local windows prescribed by a transition of $M$. It accepts when no legal window explains the pair. Taking separate machines for the two parities and their finite union handles every adjacent pair. Thus histories containing an illegal transition form a context-free language, and so does their union with the two regular error languages. The construction is effective in the finite transition table, hence produces a CFG $G_{M,w}$ with $L(G_{M,w})=B_{M,w}$.

By the definition of $B_{M,w}$, the grammar $G_{M,w}$ is universal exactly when there is no accepting computation history of $M$ on $w$. Using [L1], this is equivalent to $L(G_{M,w})={\mathrm{\Sigma }}^{\ast }⟺⟨M,w⟩\mathrm{\notin }{A}_{TM}\mathrm{.}$

The construction of $G_{M,w}$ is effective by step 1.1. If CFG universality were decidable, then step 2.1 would decide $\overline{A_{TM}}$, and hence decide $A_{TM}$ by complementing the answer. That contradicts [L3].

Therefore CFG universality is undecidable.