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