let aa, bb, cc be Int-Location ; :: thesis: for I being Program of {INT,(INT *)} holds {aa,bb,cc} \/ (UsedIntLoc I) c= UsedIntLoc (for-up (aa,bb,cc,I))
let I be Program of {INT,(INT *)}; :: thesis: {aa,bb,cc} \/ (UsedIntLoc I) c= UsedIntLoc (for-up (aa,bb,cc,I))
set aux = 1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I));
set i0 = (1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))) := cc;
set i1 = SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb);
set i2 = AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0));
set i3 = aa := bb;
set I4 = while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))));
A1: UsedIntLoc (((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (aa := bb)) = (UsedIntLoc ((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:34
.= ((UsedIntLoc (((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb)))) \/ (UsedIntLoc (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:34
.= (((UsedIntLoc ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))) := cc)) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb)))) \/ (UsedIntLoc (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:35
.= (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),cc} \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb)))) \/ (UsedIntLoc (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:18
.= (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb}) \/ (UsedIntLoc (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:18
.= (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb}) \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)}) \/ (UsedIntLoc (aa := bb)) by SF_MASTR:18
.= (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb}) \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)}) \/ {aa,bb} by SF_MASTR:18 ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {aa,bb,cc} \/ (UsedIntLoc I) or x in UsedIntLoc (for-up (aa,bb,cc,I)) )
A2: UsedIntLoc (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) = {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I)))} \/ (UsedIntLoc ((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) by SCMFSA9A:30
.= {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I)))} \/ ((UsedIntLoc (I ';' (AddTo (aa,(intloc 0))))) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) by SF_MASTR:34
.= {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I)))} \/ (((UsedIntLoc I) \/ (UsedIntLoc (AddTo (aa,(intloc 0))))) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))) by SF_MASTR:34
.= {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I)))} \/ ((UsedIntLoc I) \/ ((UsedIntLoc (AddTo (aa,(intloc 0)))) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by XBOOLE_1:4
.= (UsedIntLoc I) \/ ({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I)))} \/ ((UsedIntLoc (AddTo (aa,(intloc 0)))) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by XBOOLE_1:4 ;
assume x in {aa,bb,cc} \/ (UsedIntLoc I) ; :: thesis: x in UsedIntLoc (for-up (aa,bb,cc,I))
then A3: ( x in {aa,bb,cc} or x in UsedIntLoc I ) by XBOOLE_0:def 3;
A4: UsedIntLoc (for-up (aa,bb,cc,I)) = (UsedIntLoc (((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (aa := bb))) \/ (UsedIntLoc (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))))) by SF_MASTR:31;

per cases ( x = aa or x = bb or x = cc or x in UsedIntLoc I ) by A3, ENUMSET1:def 1;

suppose x = aa ; :: thesis: x in UsedIntLoc (for-up (aa,bb,cc,I))

then x in {aa,bb} by TARSKI:def 2;
then x in UsedIntLoc (((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (aa := bb)) by A1, XBOOLE_0:def 3;
hence x in UsedIntLoc (for-up (aa,bb,cc,I)) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = bb ; :: thesis: x in UsedIntLoc (for-up (aa,bb,cc,I))

then x in {aa,bb} by TARSKI:def 2;
then x in UsedIntLoc (((((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb))) ';' (AddTo ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))) ';' (aa := bb)) by A1, XBOOLE_0:def 3;
hence x in UsedIntLoc (for-up (aa,bb,cc,I)) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = cc ; :: thesis: x in UsedIntLoc (for-up (aa,bb,cc,I))

then x in {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),cc} by TARSKI:def 2;
then x in {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb} by XBOOLE_0:def 3;
then x in ({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb}) \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)} by XBOOLE_0:def 3;
then x in (({(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),cc} \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),bb}) \/ {(1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)}) \/ {aa,bb} by XBOOLE_0:def 3;
hence x in UsedIntLoc (for-up (aa,bb,cc,I)) by A1, A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in UsedIntLoc I ; :: thesis: x in UsedIntLoc (for-up (aa,bb,cc,I))

then x in UsedIntLoc (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by A2, XBOOLE_0:def 3;
hence x in UsedIntLoc (for-up (aa,bb,cc,I)) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

end;