let b be Int-Location; :: thesis: for I, J being MacroInstruction of SCM+FSA holds UsedILoc (if>0 (b,I,J)) = ({b} \/ (UsedILoc I)) \/ (UsedILoc J)
let I, J be MacroInstruction of SCM+FSA ; :: thesis: UsedILoc (if>0 (b,I,J)) = ({b} \/ (UsedILoc I)) \/ (UsedILoc J)
set I5 = Stop SCM+FSA;
set a = b;
set I1 = b >0_goto ((card J) + 3);
set I3 = Goto ((card I) + 1);
thus UsedILoc (if>0 (b,I,J)) = UsedILoc (((((b >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))
.= (UsedILoc ((((b >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I)) \/ {} by Th3, SF_MASTR:27
.= (UsedILoc (((b >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1)))) \/ (UsedILoc I) by SF_MASTR:27
.= ((UsedILoc ((b >0_goto ((card J) + 3)) ";" J)) \/ (UsedILoc (Goto ((card I) + 1)))) \/ (UsedILoc I) by SF_MASTR:27
.= ((UsedILoc ((b >0_goto ((card J) + 3)) ";" J)) \/ {}) \/ (UsedILoc I) by Th5
.= ((UsedIntLoc (b >0_goto ((card J) + 3))) \/ (UsedILoc J)) \/ (UsedILoc I) by SF_MASTR:29
.= ({b} \/ (UsedILoc J)) \/ (UsedILoc I) by SF_MASTR:16
.= ({b} \/ (UsedILoc I)) \/ (UsedILoc J) by XBOOLE_1:4 ; :: thesis: verum