Trying for bare bones here, now.

==========

P = "G is CFG .AND. w is in G with len(w) > 2

^{p}"

Briefer form of P: "If (ANY) w is long enough ..."

Q = "w must split somehow into uvxyz PLUS uv

^{2}xy

^{2}z must also be in G"

Briefer form of Q: "then w pumps."

Theorem's form: P -> Q

Equivalent to this is the contrapositive: ~Q -> ~P

That means you can take w -fails-Q and conclude ~P. You can prove a NEGATIVE.

===========

Now I get a bit tangled up on what we have to do to w sometimes, and I think I may be onto why. It's because you prove that one word is an exception to Q. This one single chosen word doesn't pump, and since the theorem says

*every* word must pump, you've supplied the necessary "exists" to refute that "forall".

Great. But then you go about this "exists" proof in a sort of "forall" kind of way. You only need to find one exception, but to find that exception the (one) word you reckon will fail must fail no matter what arrangement you try. That's what I mean in a Kind Of "forall" way. You have to cover Every possibility.

You're trying to prove a

**single** "exception to the rule", but you have to do that by covering

**all** the cases.

Put that way, there's nothing particularly difficult about it. Maybe when a bit of this kind of confusion kicks in just remember "all-cases is not all-words".

The "forall" is an illusion. It's only KindOf ...

========

The with-length version of the theorem is easier. All it does is give you more ways of proving your exception.