let b be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds UsedI*Loc (times (b,I)) = UsedI*Loc I
let I be MacroInstruction of SCM+FSA ; :: thesis: UsedI*Loc (times (b,I)) = UsedI*Loc I
set a = b;
set aux = 1 -stRWNotIn ({b} \/ (UsedILoc I));
thus UsedI*Loc (times (b,I)) = (UsedInt*Loc ((1 -stRWNotIn ({b} \/ (UsedILoc I))) := b)) \/ (UsedI*Loc (while>0 ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0))))))) by SF_MASTR:45
.= {} \/ (UsedI*Loc (while>0 ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0))))))) by SF_MASTR:32
.= UsedI*Loc (I ";" (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0)))) by SCMFSA9A:25
.= (UsedI*Loc I) \/ (UsedInt*Loc (SubFrom ((1 -stRWNotIn ({b} \/ (UsedILoc I))),(intloc 0)))) by SF_MASTR:46
.= (UsedI*Loc I) \/ {} by SF_MASTR:32
.= UsedI*Loc I ; :: thesis: verum