let b be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds UsedILoc (Times (b,I)) = {b,(intloc 0)} \/ (UsedILoc I)
let I be MacroInstruction of SCM+FSA ; :: thesis: UsedILoc (Times (b,I)) = {b,(intloc 0)} \/ (UsedILoc I)
thus UsedILoc (Times (b,I)) = {b} \/ (UsedILoc (I ";" (SubFrom (b,(intloc 0))))) by Th24
.= {b} \/ ((UsedILoc I) \/ (UsedIntLoc (SubFrom (b,(intloc 0))))) by SF_MASTR:30
.= {b} \/ ((UsedILoc I) \/ {b,(intloc 0)}) by SF_MASTR:14
.= ({b} \/ {b,(intloc 0)}) \/ (UsedILoc I) by XBOOLE_1:4
.= {b,(intloc 0)} \/ (UsedILoc I) by ZFMISC_1:9 ; :: thesis: verum