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