I'm confused by this proof and I don't buy it, especially since the definitions, including that of "parsing," are too imprecise to warrant some reduction proof. You also don't need reduction to show the existence of an example, which is what you're essentially trying to do. You seem to be making the claim that when you have code

  BEGIN {
    x();
    sub foo { }
  }
[download]

then foo() will be declared only when x() terminates.

  for(;;) { }
  int x;
[download]

and asking whether "x" will ever be declared, which says absolutely nothing about how this program is parsed (and it's parsed fine).

Cheers.