Because the DFA follows edges, not logic. If free appears twice along any sequence of edges, the compiler rejects it.
If the compiler rejects things that have free appear twice on branching control flow paths but aren't actually broken due to dynamic control flow (like your looping example given elsewhere) then that's a false positive, isn't it?
And people thought '0% negatives' was meaning 'no false positives'.
The D implementation, in contrast, uses a well-defined rule outlined above, and it works predictably and reliably (absent implementation bugs, rather than ad hoc rule shortcomings).
Another way of putting it is that the rules of the language are changed to make 0%/100% results workable. The compiler never says "there may be a problem here". It passes or is rejected. If it is passes, it is memory safe.
Given these more precise definitions, the analogous theorem would be that there is no type system (or static analysis) for use-after-free which is both sound and complete.
for (i = 0; i < 10; ++i);
However, such a construct is a hard error in D. Whether you meant it or not, it is not allowed. This is what I meant.
A construct in D that would pass is:
for (i = 0; i < 10; ++i) { }