let cc, aa, bb be Int-Location ; :: thesis: for f being FinSeq-Location st cc <> 1 -stRWNotIn {aa,bb} & cc <> 2 -ndRWNotIn {aa,bb} holds
swap f,aa,bb does_not_destroy cc
let f be FinSeq-Location ; :: thesis: ( cc <> 1 -stRWNotIn {aa,bb} & cc <> 2 -ndRWNotIn {aa,bb} implies swap f,aa,bb does_not_destroy cc )
set a = aa;
set b = bb;
set aux1 = 1 -stRWNotIn {aa,bb};
set aux2 = 2 -ndRWNotIn {aa,bb};
assume ( cc <> 1 -stRWNotIn {aa,bb} & cc <> 2 -ndRWNotIn {aa,bb} ) ; :: thesis: swap f,aa,bb does_not_destroy cc
then A1: ( (1 -stRWNotIn {aa,bb}) := f,aa does_not_destroy cc & (2 -ndRWNotIn {aa,bb}) := f,bb does_not_destroy cc ) by SCMFSA7B:20;
f,aa := (2 -ndRWNotIn {aa,bb}) does_not_destroy cc by SCMFSA7B:21;
then (((1 -stRWNotIn {aa,bb}) := f,aa) ';' ((2 -ndRWNotIn {aa,bb}) := f,bb)) ';' (f,aa := (2 -ndRWNotIn {aa,bb})) does_not_destroy cc by A1, SCMFSA8C:83, SCMFSA8C:84;
hence swap f,aa,bb does_not_destroy cc by SCMFSA7B:21, SCMFSA8C:83; :: thesis: verum