let aa, bb be Int-Location ; :: thesis: for f being FinSeq-Location holds {aa,bb} c= UsedIntLoc (swap f,aa,bb)
let f be FinSeq-Location ; :: thesis: {aa,bb} c= UsedIntLoc (swap f,aa,bb)
set a = aa;
set b = bb;
set aux1 = 1 -stRWNotIn {aa,bb};
set aux2 = 2 -ndRWNotIn {aa,bb};
set i0 = (1 -stRWNotIn {aa,bb}) := f,aa;
set i1 = (2 -ndRWNotIn {aa,bb}) := f,bb;
set i2 = f,aa := (2 -ndRWNotIn {aa,bb});
set i3 = f,bb := (1 -stRWNotIn {aa,bb});
A1: UsedIntLoc (swap f,aa,bb) = (UsedIntLoc ((((1 -stRWNotIn {aa,bb}) := f,aa) ';' ((2 -ndRWNotIn {aa,bb}) := f,bb)) ';' (f,aa := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc (f,bb := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:34
.= ((UsedIntLoc (((1 -stRWNotIn {aa,bb}) := f,aa) ';' ((2 -ndRWNotIn {aa,bb}) := f,bb))) \/ (UsedIntLoc (f,aa := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc (f,bb := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:34
.= (((UsedIntLoc ((1 -stRWNotIn {aa,bb}) := f,aa)) \/ (UsedIntLoc ((2 -ndRWNotIn {aa,bb}) := f,bb))) \/ (UsedIntLoc (f,aa := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc (f,bb := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:35
.= (({(1 -stRWNotIn {aa,bb}),aa} \/ (UsedIntLoc ((2 -ndRWNotIn {aa,bb}) := f,bb))) \/ (UsedIntLoc (f,aa := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc (f,bb := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:21
.= (({(1 -stRWNotIn {aa,bb}),aa} \/ {(2 -ndRWNotIn {aa,bb}),bb}) \/ (UsedIntLoc (f,aa := (2 -ndRWNotIn {aa,bb})))) \/ (UsedIntLoc (f,bb := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:21
.= (({(1 -stRWNotIn {aa,bb}),aa} \/ {(2 -ndRWNotIn {aa,bb}),bb}) \/ {(2 -ndRWNotIn {aa,bb}),aa}) \/ (UsedIntLoc (f,bb := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:21
.= (({(1 -stRWNotIn {aa,bb}),aa} \/ {(2 -ndRWNotIn {aa,bb}),bb}) \/ {(2 -ndRWNotIn {aa,bb}),aa}) \/ {(1 -stRWNotIn {aa,bb}),bb} by SF_MASTR:21 ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {aa,bb} or x in UsedIntLoc (swap f,aa,bb) )
assume A2: x in {aa,bb} ; :: thesis: x in UsedIntLoc (swap f,aa,bb)

per cases ( x = aa or x = bb ) by A2, TARSKI:def 2;

suppose x = aa ; :: thesis: x in UsedIntLoc (swap f,aa,bb)

then x in {(2 -ndRWNotIn {aa,bb}),aa} by TARSKI:def 2;
then x in ({(1 -stRWNotIn {aa,bb}),aa} \/ {(2 -ndRWNotIn {aa,bb}),bb}) \/ {(2 -ndRWNotIn {aa,bb}),aa} by XBOOLE_0:def 3;
hence x in UsedIntLoc (swap f,aa,bb) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = bb ; :: thesis: x in UsedIntLoc (swap f,aa,bb)

then x in {(1 -stRWNotIn {aa,bb}),bb} by TARSKI:def 2;
hence x in UsedIntLoc (swap f,aa,bb) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;