let I, J be Program of ; :: thesis: for a being Int-Location holds
( UsedIntLoc (if=0 (a,I,J)) = ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) & UsedIntLoc (if>0 (a,I,J)) = ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) )
let a be Int-Location ; :: thesis: ( UsedIntLoc (if=0 (a,I,J)) = ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) & UsedIntLoc (if>0 (a,I,J)) = ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc 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 UsedIntLoc (if=0 (a,I,J)) = UsedIntLoc (((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by SCMFSA8B:def 1
.= (UsedIntLoc ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) \/ {} by SCMFSA9A:3, SF_MASTR:27
.= (UsedIntLoc (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1)))) \/ (UsedIntLoc I) by SF_MASTR:27
.= ((UsedIntLoc ((a =0_goto ((card J) + 3)) ';' J)) \/ (UsedIntLoc (Goto ((card I) + 1)))) \/ (UsedIntLoc I) by SF_MASTR:27
.= ((UsedIntLoc ((a =0_goto ((card J) + 3)) ';' J)) \/ {}) \/ (UsedIntLoc I) by SCMFSA9A:5
.= ((UsedIntLoc (a =0_goto ((card J) + 3))) \/ (UsedIntLoc J)) \/ (UsedIntLoc I) by SF_MASTR:29
.= ({a} \/ (UsedIntLoc J)) \/ (UsedIntLoc I) by SF_MASTR:16
.= ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) by XBOOLE_1:4 ; :: thesis: UsedIntLoc (if>0 (a,I,J)) = ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)
thus UsedIntLoc (if>0 (a,I,J)) = UsedIntLoc (((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by SCMFSA8B:def 2
.= (UsedIntLoc ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) \/ {} by SCMFSA9A:3, SF_MASTR:27
.= (UsedIntLoc (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1)))) \/ (UsedIntLoc I) by SF_MASTR:27
.= ((UsedIntLoc ((a >0_goto ((card J) + 3)) ';' J)) \/ (UsedIntLoc (Goto ((card I) + 1)))) \/ (UsedIntLoc I) by SF_MASTR:27
.= ((UsedIntLoc ((a >0_goto ((card J) + 3)) ';' J)) \/ {}) \/ (UsedIntLoc I) by SCMFSA9A:5
.= ((UsedIntLoc (a >0_goto ((card J) + 3))) \/ (UsedIntLoc J)) \/ (UsedIntLoc I) by SF_MASTR:29
.= ({a} \/ (UsedIntLoc J)) \/ (UsedIntLoc I) by SF_MASTR:16
.= ({a} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) by XBOOLE_1:4 ; :: thesis: verum