let b be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedInt*Loc (times b,I) = UsedInt*Loc I
let I be Program of SCM+FSA ; :: thesis: UsedInt*Loc (times b,I) = UsedInt*Loc I
set a = b;
set aux = 1 -stRWNotIn ({b} \/ (UsedIntLoc I));
thus UsedInt*Loc (times b,I) = (UsedInt*Loc ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))) := b)) \/ (UsedInt*Loc (while>0 (1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0 ))))) by SF_MASTR:49
.= {} \/ (UsedInt*Loc (while>0 (1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0 ))))) by SF_MASTR:36
.= UsedInt*Loc (I ';' (SubFrom (1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0 ))) by SCMFSA9A:31
.= (UsedInt*Loc I) \/ (UsedInt*Loc (SubFrom (1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0 ))) by SF_MASTR:50
.= (UsedInt*Loc I) \/ {} by SF_MASTR:36
.= UsedInt*Loc I ; :: thesis: verum