let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedIntLoc (Times a,I) = (UsedIntLoc I) \/ {a,(intloc 0 )}
let I be Program of SCM+FSA ; :: thesis: UsedIntLoc (Times a,I) = (UsedIntLoc I) \/ {a,(intloc 0 )}
set g1 = Goto (insloc 2);
set SF = SubFrom a,(intloc 0 );
set if0 = if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )));
thus UsedIntLoc (Times a,I) = ({a} \/ (UsedIntLoc (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) \/ {} by Th29, SCMFSA9A:9
.= {a} \/ (UsedIntLoc (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) by Th30
.= {a} \/ (({a} \/ (UsedIntLoc (Goto (insloc 2)))) \/ (UsedIntLoc (I ';' (SubFrom a,(intloc 0 ))))) by Th29
.= {a} \/ (({a} \/ {} ) \/ (UsedIntLoc (I ';' (SubFrom a,(intloc 0 ))))) by SCMFSA9A:11
.= ({a} \/ {a}) \/ (UsedIntLoc (I ';' (SubFrom a,(intloc 0 )))) by XBOOLE_1:4
.= ((UsedIntLoc I) \/ (UsedIntLoc (SubFrom a,(intloc 0 )))) \/ {a} by SF_MASTR:34
.= ((UsedIntLoc I) \/ {a,(intloc 0 )}) \/ {a} by SF_MASTR:18
.= (UsedIntLoc I) \/ ({a} \/ {a,(intloc 0 )}) by XBOOLE_1:4
.= (UsedIntLoc I) \/ {a,a,(intloc 0 )} by ENUMSET1:42
.= (UsedIntLoc I) \/ {a,(intloc 0 )} by ENUMSET1:70 ; :: thesis: verum