let aa, bb be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not while>0 (bb,I) destroys aa
let I be MacroInstruction of SCM+FSA ; :: thesis: ( not I destroys aa implies not while>0 (bb,I) destroys aa )
set F = if>0 (bb,(I ';' (goto 0)));
assume not I destroys aa ; :: thesis: not while>0 (bb,I) destroys aa
then A1: not if>0 (bb,(I ';' (goto 0))) destroys aa by Lm3;
not goto 0 destroys aa ;
hence not while>0 (bb,I) destroys aa by A1, SCMFSA8A:42; :: thesis: verum