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