let I be Program of {INT,(INT *)}; :: 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 (Reloc ((ProgramPart I),k)) by COMPOS_1:116
.= UsedIntLoc (Shift ((ProgramPart I),k)) by Th28
.= UsedIntLoc (ProgramPart I) by Th26 ;
hence UsedIntLoc I = UsedIntLoc (ProgramPart (Relocated (I,k))) by RELAT_1:209; :: thesis: verum