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
not swap f,aa,bb destroysdestroy cc
let f be FinSeq-Location ; :: thesis: ( cc <> 1 -stRWNotIn {aa,bb} & cc <> 2 -ndRWNotIn {aa,bb} implies not swap f,aa,bb destroysdestroy 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: not swap f,aa,bb destroysdestroy cc
then A1: ( not (1 -stRWNotIn {aa,bb}) := f,aa destroysdestroy cc & not (2 -ndRWNotIn {aa,bb}) := f,bb destroysdestroy cc ) by SCMFSA7B:20;
not f,aa := (2 -ndRWNotIn {aa,bb}) destroysdestroy cc by SCMFSA7B:21;
then not (((1 -stRWNotIn {aa,bb}) := f,aa) ';' ((2 -ndRWNotIn {aa,bb}) := f,bb)) ';' (f,aa := (2 -ndRWNotIn {aa,bb})) destroysdestroy cc by A1, SCMFSA8C:83, SCMFSA8C:84;
hence not swap f,aa,bb destroysdestroy cc by SCMFSA7B:21, SCMFSA8C:83; :: thesis: verum