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