let aa, bb be Int-Location; :: thesis: for f being FinSeq-Location holds {aa,bb} c= UsedILoc (swap (f,aa,bb))
let f be FinSeq-Location ; :: thesis: {aa,bb} c= UsedILoc (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: UsedILoc (swap (f,aa,bb)) = (UsedILoc ((((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:30
.= ((UsedILoc (((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:30
.= (((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:31
.= (({(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:17
.= (({(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:17
.= (({(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:17
.= (({(1 -stRWNotIn {aa,bb}),aa} \/ {(2 -ndRWNotIn {aa,bb}),bb}) \/ {(2 -ndRWNotIn {aa,bb}),aa}) \/ {(1 -stRWNotIn {aa,bb}),bb} by SF_MASTR:17 ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {aa,bb} or x in UsedILoc (swap (f,aa,bb)) )
assume A2: x in {aa,bb} ; :: thesis: x in UsedILoc (swap (f,aa,bb))
per cases ( x = aa or x = bb ) by A2, TARSKI:def 2;
suppose x = aa ; :: thesis: x in UsedILoc (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 UsedILoc (swap (f,aa,bb)) by A1, XBOOLE_0:def 3; :: thesis: verum
end;
suppose x = bb ; :: thesis: x in UsedILoc (swap (f,aa,bb))
then x in {(1 -stRWNotIn {aa,bb}),bb} by TARSKI:def 2;
hence x in UsedILoc (swap (f,aa,bb)) by A1, XBOOLE_0:def 3; :: thesis: verum
end;
end;