let b be Int-Location ; for I being Program of SCM+FSA holds {b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I))
let I be Program of SCM+FSA; {b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I))
set a = b;
set aux = 1 -stRWNotIn ({b} \/ (UsedIntLoc I));
UsedIntLoc (times (b,I)) =
(UsedIntLoc ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))) := b)) \/ (UsedIntLoc (while>0 ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(I ';' (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))))))
by SF_MASTR:29
.=
{(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc (while>0 ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(I ';' (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))))))
by SF_MASTR:14
.=
{(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ ({(1 -stRWNotIn ({b} \/ (UsedIntLoc I)))} \/ (UsedIntLoc (I ';' (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0))))))
by SCMFSA9A:24
.=
({(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ {(1 -stRWNotIn ({b} \/ (UsedIntLoc I)))}) \/ (UsedIntLoc (I ';' (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))))
by XBOOLE_1:4
.=
{(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc (I ';' (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))))
by ZFMISC_1:9
.=
{(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ ((UsedIntLoc I) \/ (UsedIntLoc (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))))
by SF_MASTR:30
.=
{(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ ((UsedIntLoc I) \/ {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)})
by SF_MASTR:14
.=
({(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I)) \/ {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)}
by XBOOLE_1:4
;
then A1:
{(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I))
by XBOOLE_1:7;
UsedIntLoc I c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I)
by XBOOLE_1:7;
then A2:
UsedIntLoc I c= UsedIntLoc (times (b,I))
by A1, XBOOLE_1:1;
( {b} c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} & {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) )
by XBOOLE_1:7, ZFMISC_1:7;
then
{b} c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I)
by XBOOLE_1:1;
then
{b} c= UsedIntLoc (times (b,I))
by A1, XBOOLE_1:1;
hence
{b} \/ (UsedIntLoc I) c= UsedIntLoc (times (b,I))
by A2, XBOOLE_1:8; verum