let aa, bb, cc be Int-Location ; :: thesis: for I being Program of SCM+FSA holds {aa,bb,cc} \/ (UsedIntLoc I) c= UsedIntLoc (for-up aa,bb,cc,I)
let I be Program of SCM+FSA ; :: 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
;
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
;
A3:
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;
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) )
assume
x in {aa,bb,cc} \/ (UsedIntLoc I)
; :: thesis: x in UsedIntLoc (for-up aa,bb,cc,I)
then A4:
( x in {aa,bb,cc} or x in UsedIntLoc I )
by XBOOLE_0:def 3;
per cases
( x = aa or x = bb or x = cc or x in UsedIntLoc I )
by A4, 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 A3, 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 A3, 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, A3, 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 A3, XBOOLE_0:def 3;
:: thesis: verum end;