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