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