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