let a be read-write Int-Location; :: thesis: for aa, bb, cc being Int-Location
for I being MacroInstruction of SCM+FSA st a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) & not I destroys aa holds
not for-up (a,bb,cc,I) destroys aa
let aa, bb, cc be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA st a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) & not I destroys aa holds
not for-up (a,bb,cc,I) destroys aa
let I be MacroInstruction of SCM+FSA ; :: thesis: ( a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) & not I destroys aa implies not for-up (a,bb,cc,I) destroys aa )
assume that
A1: a <> aa and
A2: aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) and
A3: not I destroys aa ; :: thesis: not for-up (a,bb,cc,I) destroys aa
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I));
set i2 = AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0));
A4: not AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)) destroys aa by A2, SCMFSA7B:7;
set i3 = a := bb;
set i1 = SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb);
set i0 = (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc;
set I03 = ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (a := bb);
( not (1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc destroys aa & not SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb) destroys aa ) by A2, SCMFSA7B:6, SCMFSA7B:8;
then not (((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0))) destroys aa by A4, SCMFSA8C:54, SCMFSA8C:55;
then A5: not ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (a := bb) destroys aa by A1, SCMFSA7B:6, SCMFSA8C:54;
set IB = (I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)));
set I4 = while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0)))));
not I ";" (AddTo (a,(intloc 0))) destroys aa by A1, A3, SCMFSA7B:7, SCMFSA8C:54;
then not (I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0))) destroys aa by A2, SCMFSA7B:8, SCMFSA8C:54;
then not while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),((I ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I))),(intloc 0))))) destroys aa by SCMFSA8C:92;
hence not for-up (a,bb,cc,I) destroys aa by A5, SCMFSA8C:52; :: thesis: verum