In Michael Sipser's book, they prove that ALL_CFG = { G | G is a CFG and L(G) = Σ∗ } is undecidable using accepting computation histories and PDAs. My question is how exactly (with details of implementation)does a PDA go on to compare two configurations and figure out that the first properly yields the second.
I know that the computation histories are encoded in a convenient manner (reversing), but I couldn't seem to figure out how and what the PDA really does.