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 )
assume that
A1: cc <> 1 -stRWNotIn {aa,bb} and
A2: cc <> 2 -ndRWNotIn {aa,bb} ; :: thesis: 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};
A3: (1 -stRWNotIn {aa,bb}) := f,aa does_not_destroy cc by A1, SCMFSA7B:20;
A4: (2 -ndRWNotIn {aa,bb}) := f,bb does_not_destroy cc by A2, 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 A3, A4, SCMFSA8C:83, SCMFSA8C:84;
hence swap f,aa,bb does_not_destroy cc by SCMFSA7B:21, SCMFSA8C:83; :: thesis: verum