let aa, bb, cc 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) destroys cc
let f be FinSeq-Location ; :: thesis: ( cc <> 1 -stRWNotIn {aa,bb} & cc <> 2 -ndRWNotIn {aa,bb} implies not swap (f,aa,bb) destroys 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) destroys cc
then A1: ( not (1 -stRWNotIn {aa,bb}) := (f,aa) destroys cc & not (2 -ndRWNotIn {aa,bb}) := (f,bb) destroys cc ) by SCMFSA7B:14;
not (f,aa) := (2 -ndRWNotIn {aa,bb}) destroys cc by SCMFSA7B:15;
then not (((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ";" ((f,aa) := (2 -ndRWNotIn {aa,bb})) destroys cc by A1, SCMFSA8C:54, SCMFSA8C:55;
hence not swap (f,aa,bb) destroys cc by SCMFSA7B:15, SCMFSA8C:54; :: thesis: verum