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:45
.= {} \/ (UsedInt*Loc (while>0 ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(I ';' (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0))))))) by SF_MASTR:32
.= UsedInt*Loc (I ';' (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))) by SCMFSA9A:25
.= (UsedInt*Loc I) \/ (UsedInt*Loc (SubFrom ((1 -stRWNotIn ({b} \/ (UsedIntLoc I))),(intloc 0)))) by SF_MASTR:46
.= (UsedInt*Loc I) \/ {} by SF_MASTR:32
.= UsedInt*Loc I ; :: thesis: verum