let I be Program of SCM+FSA ; :: thesis: for k being Element of NAT holds UsedInt*Loc I = UsedInt*Loc (ProgramPart (Relocated I,k))
let k be Element of NAT ; :: thesis: UsedInt*Loc I = UsedInt*Loc (ProgramPart (Relocated I,k))
UsedInt*Loc (ProgramPart (Relocated I,k)) = UsedInt*Loc (IncAddr [(Shift (ProgramPart I),k)],k) by SCMFSA_5:2
.= UsedInt*Loc (Shift (ProgramPart I),k) by Th44
.= UsedInt*Loc [(ProgramPart I)] by Th42 ;
hence UsedInt*Loc I = UsedInt*Loc (ProgramPart (Relocated I,k)) by AMI_1:105; :: thesis: verum