let aa, bb, cc be Int-Location; 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 ; ( 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} )
; 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; verum