First, the proof (or my parsing of the proof :) changed since I first responded. If it did not change, then I offer my apologies to abell and blame it on my not consuming enough caffine.

As I read it now, the proof appears to be correct, even if you use an identity function (or something that looks like an identity function for a given x) for f(x) (example, replace all /a+/ with "a" . length($1) . "a" - a win for all /a+/ longer than 3, identity for /^[^a]*$/).

Like I said, a minor nit, which was plugged by abell or originally misread by /me.