let a be read-write Int-Location ; :: thesis: for aa, bb, cc being Int-Location
for I being Program of st a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc 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 Program of st a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) & not I destroys aa holds
not for-up (a,bb,cc,I) destroys aa
let I be Program of ; :: thesis: ( a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc 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} \/ (UsedIntLoc I)) and
A3: not I destroys aa ; :: thesis: not for-up (a,bb,cc,I) destroys aa
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I));
set i2 = AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0));
A4: not AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) destroys aa by A2, SCMFSA7B:7;
set i3 = a := bb;
set i1 = SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb);
set i0 = (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc;
set I03 = ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (a := bb);
( not (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc destroys aa & not SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb) destroys aa ) by A2, SCMFSA7B:6, SCMFSA7B:8;
then not (((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) destroys aa by A4, SCMFSA8C:54, SCMFSA8C:55;
then A5: not ((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc 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} \/ (UsedIntLoc I))),(intloc 0)));
set I4 = while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc 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} \/ (UsedIntLoc I))),(intloc 0))) destroys aa by A2, SCMFSA7B:8, SCMFSA8C:54;
then not while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (a,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) destroys aa by Th14;
hence not for-up (a,bb,cc,I) destroys aa by A5, SCMFSA8C:52; :: thesis: verum