let aa, bb be Int-Location; :: thesis: for f being FinSeq-Location holds UsedI*Loc (swap (f,aa,bb)) = {f}
let f be FinSeq-Location ; :: thesis: UsedI*Loc (swap (f,aa,bb)) = {f}
set a = aa;
set b = bb;
set aux1 = 1 -stRWNotIn {aa,bb};
set aux2 = 2 -ndRWNotIn {aa,bb};
thus UsedI*Loc (swap (f,aa,bb)) = (UsedI*Loc ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ";" ((f,aa) := (2 -ndRWNotIn {aa,bb})))) \/ (UsedInt*Loc ((f,bb) := (1 -stRWNotIn {aa,bb}))) by SF_MASTR:46
.= (UsedI*Loc ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ";" ((f,aa) := (2 -ndRWNotIn {aa,bb})))) \/ {f} by SF_MASTR:33
.= ((UsedI*Loc (((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb)))) \/ (UsedInt*Loc ((f,aa) := (2 -ndRWNotIn {aa,bb})))) \/ {f} by SF_MASTR:46
.= ((UsedI*Loc (((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb)))) \/ {f}) \/ {f} by SF_MASTR:33
.= (((UsedInt*Loc ((1 -stRWNotIn {aa,bb}) := (f,aa))) \/ (UsedInt*Loc ((2 -ndRWNotIn {aa,bb}) := (f,bb)))) \/ {f}) \/ {f} by SF_MASTR:47
.= (({f} \/ (UsedInt*Loc ((2 -ndRWNotIn {aa,bb}) := (f,bb)))) \/ {f}) \/ {f} by SF_MASTR:33
.= ({f} \/ {f}) \/ {f} by SF_MASTR:33
.= {f} ; :: thesis: verum