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