let b be Int-Location ; :: thesis: for I, J being Program of SCM+FSA holds UsedInt*Loc (if>0 b,I,J) = (UsedInt*Loc I) \/ (UsedInt*Loc J)
let I, J be Program of SCM+FSA ; :: thesis: UsedInt*Loc (if>0 b,I,J) = (UsedInt*Loc I) \/ (UsedInt*Loc J)
set a = b;
set I1 = b >0_goto (insloc ((card J) + 3));
set I3 = Goto (insloc ((card I) + 1));
set I5 = Stop SCM+FSA ;
thus UsedInt*Loc (if>0 b,I,J) = UsedInt*Loc (((((b >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) by SCMFSA8B:def 2
.= (UsedInt*Loc ((((b >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) \/ {} by Th10, SF_MASTR:47
.= (UsedInt*Loc (((b >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1))))) \/ (UsedInt*Loc I) by SF_MASTR:47
.= ((UsedInt*Loc ((b >0_goto (insloc ((card J) + 3))) ';' J)) \/ (UsedInt*Loc (Goto (insloc ((card I) + 1))))) \/ (UsedInt*Loc I) by SF_MASTR:47
.= ((UsedInt*Loc ((b >0_goto (insloc ((card J) + 3))) ';' J)) \/ {} ) \/ (UsedInt*Loc I) by Th12
.= ((UsedInt*Loc (b >0_goto (insloc ((card J) + 3)))) \/ (UsedInt*Loc J)) \/ (UsedInt*Loc I) by SF_MASTR:49
.= ({} \/ (UsedInt*Loc J)) \/ (UsedInt*Loc I) by SF_MASTR:36
.= (UsedInt*Loc I) \/ (UsedInt*Loc J) ; :: thesis: verum