Incorrect handling of IF statements in pt.6 of DO proofs

[harrytallbelt]

When proving a DO statement, we toss off all the inner loops of a loop.
This leads to IF statements proving problems, because we lose the conditions,
provided by the inner loop guards negations:
For example consider a loop body

x := -1;
do x < 0 -> ... od;
if x < 0 -> abort | ... fi

By throwing the inner loop out, we lose the knowledge that x will never be < 0 at IF.

We already have problems of this sort, for example proving matrix_search
with an incorrect inner loop initialisation command j := 1 yields not only the
correct error, but also errors in loop finalisation IF statement.