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 { }
}
then foo() will be declared only when x() terminates.
But that's like writing this Java code
for(;;) { }
int x;
and asking whether "x" will ever be declared, which says absolutely nothing about how this program is parsed (and it's parsed fine).
Cheers.