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

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