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 a = b;
set I1 = b =0_goto (insloc ((card J) + 3));
set I3 = Goto (insloc ((card I) + 1));
set I5 = Stop SCM+FSA ;
thus UsedIntLoc (if=0 b,I,J) = UsedIntLoc (((((b =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) by SCMFSA8B:def 1
.= (UsedIntLoc ((((b =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) \/ {} by Th9, SF_MASTR:31
.= (UsedIntLoc (((b =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1))))) \/ (UsedIntLoc I) by SF_MASTR:31
.= ((UsedIntLoc ((b =0_goto (insloc ((card J) + 3))) ';' J)) \/ (UsedIntLoc (Goto (insloc ((card I) + 1))))) \/ (UsedIntLoc I) by SF_MASTR:31
.= ((UsedIntLoc ((b =0_goto (insloc ((card J) + 3))) ';' J)) \/ {} ) \/ (UsedIntLoc I) by Th11
.= ((UsedIntLoc (b =0_goto (insloc ((card J) + 3)))) \/ (UsedIntLoc J)) \/ (UsedIntLoc I) by SF_MASTR:33
.= ({b} \/ (UsedIntLoc J)) \/ (UsedIntLoc I) by SF_MASTR:20
.= ({b} \/ (UsedIntLoc I)) \/ (UsedIntLoc J) by XBOOLE_1:4 ; :: thesis: verum