let a be read-write Int-Location ; :: thesis: for aa, bb, cc being Int-Location
for I being Program of SCM+FSA st a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) & not I destroysdestroy aa holds
not for-up a,bb,cc,I destroysdestroy aa
let aa, bb, cc be Int-Location ; :: thesis: for I being Program of SCM+FSA st a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) & not I destroysdestroy aa holds
not for-up a,bb,cc,I destroysdestroy aa
let I be Program of SCM+FSA ; :: thesis: ( a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) & not I destroysdestroy aa implies not for-up a,bb,cc,I destroysdestroy aa )
assume that
A1: a <> aa and
A2: aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) and
A3: not I destroysdestroy aa ; :: thesis: not for-up a,bb,cc,I destroysdestroy 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 ) destroysdestroy aa by A2, SCMFSA7B:13;
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 destroysdestroy aa & not SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb destroysdestroy aa ) by A2, SCMFSA7B:12, SCMFSA7B:14;
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 )) destroysdestroy aa by A4, SCMFSA8C:83, SCMFSA8C:84;
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) destroysdestroy aa by A1, SCMFSA7B:12, SCMFSA8C:83;
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 )) destroysdestroy aa by A1, A3, SCMFSA7B:13, SCMFSA8C:83;
then not (I ';' (AddTo a,(intloc 0 ))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0 )) destroysdestroy aa by A2, SCMFSA7B:14, SCMFSA8C:83;
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 ))) destroysdestroy aa by Th14;
hence not for-up a,bb,cc,I destroysdestroy aa by A5, SCMFSA8C:81; :: thesis: verum