This proof is from the book "Introduction to Languages and the Theory of Computation" by John C. Martin.
My question is from the pink part at the second page:
It follows in particular that no sequence of moves can cause M to empty its stack.
and further, it talks about $y_x$ that is my second question. I can't understand what $y_x$ is.
I'll appreciate it if someone please describe me the whole proof.