let aa, bb, cc be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds {aa,bb,cc} \/ (UsedILoc I) c= UsedILoc (for-up (aa,bb,cc,I))
let I be MacroInstruction of SCM+FSA ; :: thesis: {aa,bb,cc} \/ (UsedILoc I) c= UsedILoc (for-up (aa,bb,cc,I))
set aux = 1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I));
set i0 = (1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))) := cc;
set i1 = SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb);
set i2 = AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0));
set i3 = aa := bb;
set I4 = while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),((I ";" (AddTo (aa,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)))));
A1: UsedILoc (((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (aa := bb)) = (UsedILoc ((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:30
.= ((UsedILoc (((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb)))) \/ (UsedIntLoc (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:30
.= (((UsedIntLoc ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))) := cc)) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb)))) \/ (UsedIntLoc (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:31
.= (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),cc} \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb)))) \/ (UsedIntLoc (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:14
.= (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb}) \/ (UsedIntLoc (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:14
.= (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb}) \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)}) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:14
.= (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb}) \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)}) \/ {aa,bb} by SF_MASTR:14 ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {aa,bb,cc} \/ (UsedILoc I) or x in UsedILoc (for-up (aa,bb,cc,I)) )
A2: UsedILoc (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),((I ";" (AddTo (aa,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)))))) = {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I)))} \/ (UsedILoc ((I ";" (AddTo (aa,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0))))) by SCMFSA9A:24
.= {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I)))} \/ ((UsedILoc (I ";" (AddTo (aa,(intloc 0))))) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0))))) by SF_MASTR:30
.= {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I)))} \/ (((UsedILoc I) \/ (UsedIntLoc (AddTo (aa,(intloc 0))))) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0))))) by SF_MASTR:30
.= {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I)))} \/ ((UsedILoc I) \/ ((UsedIntLoc (AddTo (aa,(intloc 0)))) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)))))) by XBOOLE_1:4
.= (UsedILoc I) \/ ({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I)))} \/ ((UsedIntLoc (AddTo (aa,(intloc 0)))) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)))))) by XBOOLE_1:4 ;
assume x in {aa,bb,cc} \/ (UsedILoc I) ; :: thesis: x in UsedILoc (for-up (aa,bb,cc,I))
then A3: ( x in {aa,bb,cc} or x in UsedILoc I ) by XBOOLE_0:def 3;
A4: UsedILoc (for-up (aa,bb,cc,I)) = (UsedILoc (((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (aa := bb))) \/ (UsedILoc (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),((I ";" (AddTo (aa,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0))))))) by SF_MASTR:27;
per cases ( x = aa or x = bb or x = cc or x in UsedILoc I ) by A3, ENUMSET1:def 1;
suppose x = aa ; :: thesis: x in UsedILoc (for-up (aa,bb,cc,I))
then x in {aa,bb} by TARSKI:def 2;
then x in UsedILoc (((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (aa := bb)) by A1, XBOOLE_0:def 3;
hence x in UsedILoc (for-up (aa,bb,cc,I)) by A4, XBOOLE_0:def 3; :: thesis: verum
end;
suppose x = bb ; :: thesis: x in UsedILoc (for-up (aa,bb,cc,I))
then x in {aa,bb} by TARSKI:def 2;
then x in UsedILoc (((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))) := cc) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb))) ";" (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)))) ";" (aa := bb)) by A1, XBOOLE_0:def 3;
hence x in UsedILoc (for-up (aa,bb,cc,I)) by A4, XBOOLE_0:def 3; :: thesis: verum
end;
suppose x = cc ; :: thesis: x in UsedILoc (for-up (aa,bb,cc,I))
then x in {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),cc} by TARSKI:def 2;
then x in {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb} by XBOOLE_0:def 3;
then x in ({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb}) \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)} by XBOOLE_0:def 3;
then x in (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),bb}) \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)}) \/ {aa,bb} by XBOOLE_0:def 3;
hence x in UsedILoc (for-up (aa,bb,cc,I)) by A1, A4, XBOOLE_0:def 3; :: thesis: verum
end;
suppose x in UsedILoc I ; :: thesis: x in UsedILoc (for-up (aa,bb,cc,I))
then x in UsedILoc (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),((I ";" (AddTo (aa,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedILoc I))),(intloc 0)))))) by A2, XBOOLE_0:def 3;
hence x in UsedILoc (for-up (aa,bb,cc,I)) by A4, XBOOLE_0:def 3; :: thesis: verum
end;
end;