let aa, bb be Int-Location ; :: thesis: for f being FinSeq-Location holds UsedInt*Loc (swap f,aa,bb) = {f}
let f be FinSeq-Location ; :: thesis: UsedInt*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 UsedInt*Loc (swap f,aa,bb) = (UsedInt*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:50
.= (UsedInt*Loc ((((1 -stRWNotIn {aa,bb}) := f,aa) ';' ((2 -ndRWNotIn {aa,bb}) := f,bb)) ';' (f,aa := (2 -ndRWNotIn {aa,bb})))) \/ {f} by SF_MASTR:37
.= ((UsedInt*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:50
.= ((UsedInt*Loc (((1 -stRWNotIn {aa,bb}) := f,aa) ';' ((2 -ndRWNotIn {aa,bb}) := f,bb))) \/ {f}) \/ {f} by SF_MASTR:37
.= (((UsedInt*Loc ((1 -stRWNotIn {aa,bb}) := f,aa)) \/ (UsedInt*Loc ((2 -ndRWNotIn {aa,bb}) := f,bb))) \/ {f}) \/ {f} by SF_MASTR:51
.= (({f} \/ (UsedInt*Loc ((2 -ndRWNotIn {aa,bb}) := f,bb))) \/ {f}) \/ {f} by SF_MASTR:37
.= ({f} \/ {f}) \/ {f} by SF_MASTR:37
.= {f} ; :: thesis: verum