let b be Int-Location ; :: thesis: for I being Program of SCM+FSA holds {b} \/ (UsedIntLoc I) c= UsedIntLoc (times b,I)
let I be Program of SCM+FSA ; :: thesis: {b} \/ (UsedIntLoc I) c= UsedIntLoc (times b,I)
set a = b;
set aux = 1 -stRWNotIn ({b} \/ (UsedIntLoc I));
A1: 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:33
.= {(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:18
.= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ ({(1 -stRWNotIn ({b} \/ (UsedIntLoc I)))} \/ (UsedIntLoc (I ';' (SubFrom (1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0 ))))) by SCMFSA9A:30
.= ({(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:14
.= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ ((UsedIntLoc I) \/ (UsedIntLoc (SubFrom (1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0 )))) by SF_MASTR:34
.= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ ((UsedIntLoc I) \/ {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0 )}) by SF_MASTR:18
.= ({(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I)) \/ {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0 )} by XBOOLE_1:4 ;
A2: {b} c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} by ZFMISC_1:12;
A3: {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) by XBOOLE_1:7;
A4: {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) c= UsedIntLoc (times b,I) by A1, XBOOLE_1:7;
{b} c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) by A2, A3, XBOOLE_1:1;
then A5: {b} c= UsedIntLoc (times b,I) by A4, XBOOLE_1:1;
UsedIntLoc I c= {(1 -stRWNotIn ({b} \/ (UsedIntLoc I))),b} \/ (UsedIntLoc I) by XBOOLE_1:7;
then UsedIntLoc I c= UsedIntLoc (times b,I) by A4, XBOOLE_1:1;
hence {b} \/ (UsedIntLoc I) c= UsedIntLoc (times b,I) by A5, XBOOLE_1:8; :: thesis: verum