let aa, bb be Int-Location; :: thesis: for I, J being MacroInstruction of SCM+FSA holds UsedILoc (if>0 (aa,bb,I,J)) = ({aa,bb} \/ (UsedILoc I)) \/ (UsedILoc J)
let I, J be MacroInstruction of SCM+FSA ; :: thesis: UsedILoc (if>0 (aa,bb,I,J)) = ({aa,bb} \/ (UsedILoc I)) \/ (UsedILoc J)
set a = aa;
thus UsedILoc (if>0 (aa,bb,I,J)) = UsedILoc ((SubFrom (aa,bb)) ";" (if>0 (aa,I,J))) by SCMFSA8B:def 5
.= (UsedIntLoc (SubFrom (aa,bb))) \/ (UsedILoc (if>0 (aa,I,J))) by SF_MASTR:29
.= {aa,bb} \/ (UsedILoc (if>0 (aa,I,J))) by SF_MASTR:14
.= {aa,bb} \/ (({aa} \/ (UsedILoc I)) \/ (UsedILoc J)) by SCMFSA9A:9
.= {aa,bb} \/ ({aa} \/ ((UsedILoc I) \/ (UsedILoc J))) by XBOOLE_1:4
.= ({aa,bb} \/ {aa}) \/ ((UsedILoc I) \/ (UsedILoc J)) by XBOOLE_1:4
.= {aa,bb} \/ ((UsedILoc I) \/ (UsedILoc J)) by ZFMISC_1:9
.= ({aa,bb} \/ (UsedILoc I)) \/ (UsedILoc J) by XBOOLE_1:4 ; :: thesis: verum