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