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