let b be Int-Location; :: thesis: for I, J being MacroInstruction of SCM+FSA holds UsedI*Loc (if>0 (b,I,J)) = (UsedI*Loc I) \/ (UsedI*Loc J)
let I, J be MacroInstruction of SCM+FSA ; :: thesis: UsedI*Loc (if>0 (b,I,J)) = (UsedI*Loc I) \/ (UsedI*Loc J)
set I5 = Stop SCM+FSA;
set a = b;
set I1 = b >0_goto ((card J) + 3);
set I3 = Goto ((card I) + 1);
thus UsedI*Loc (if>0 (b,I,J)) = UsedI*Loc (((((b >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))
.= (UsedI*Loc ((((b >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I)) \/ {} by Th4, SF_MASTR:43
.= (UsedI*Loc (((b >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1)))) \/ (UsedI*Loc I) by SF_MASTR:43
.= ((UsedI*Loc ((b >0_goto ((card J) + 3)) ";" J)) \/ (UsedI*Loc (Goto ((card I) + 1)))) \/ (UsedI*Loc I) by SF_MASTR:43
.= ((UsedI*Loc ((b >0_goto ((card J) + 3)) ";" J)) \/ {}) \/ (UsedI*Loc I) by Th6
.= ((UsedInt*Loc (b >0_goto ((card J) + 3))) \/ (UsedI*Loc J)) \/ (UsedI*Loc I) by SF_MASTR:45
.= ({} \/ (UsedI*Loc J)) \/ (UsedI*Loc I) by SF_MASTR:32
.= (UsedI*Loc I) \/ (UsedI*Loc J) ; :: thesis: verum