let a be Int-Location ; :: thesis: for I being Program of {INT,(INT *)} holds UsedIntLoc (Times (a,I)) = (UsedIntLoc I) \/ {a,(intloc 0)}
let I be Program of {INT,(INT *)}; :: thesis: UsedIntLoc (Times (a,I)) = (UsedIntLoc I) \/ {a,(intloc 0)}
set g1 = Goto 2;
set SF = SubFrom (a,(intloc 0));
set if0 = if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))));
thus UsedIntLoc (Times (a,I)) = ({a} \/ (UsedIntLoc (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))))) \/ {} by Th29, SCMFSA9A:9
.= {a} \/ (UsedIntLoc (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) by Th30
.= {a} \/ (({a} \/ (UsedIntLoc (Goto 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