let I be Program of ; :: thesis: for k being Nat holds UsedILoc I = UsedILoc (Reloc (I,k))

let k be Nat; :: thesis: UsedILoc I = UsedILoc (Reloc (I,k))

A1: Reloc (I,k) = IncAddr ((Shift (I,k)),k) by COMPOS_1:34;

UsedILoc (Reloc (I,k)) = UsedILoc (Shift (I,k)) by Th24, A1

.= UsedILoc I by Th22 ;

hence UsedILoc I = UsedILoc (Reloc (I,k)) ; :: thesis: verum

let k be Nat; :: thesis: UsedILoc I = UsedILoc (Reloc (I,k))

A1: Reloc (I,k) = IncAddr ((Shift (I,k)),k) by COMPOS_1:34;

UsedILoc (Reloc (I,k)) = UsedILoc (Shift (I,k)) by Th24, A1

.= UsedILoc I by Th22 ;

hence UsedILoc I = UsedILoc (Reloc (I,k)) ; :: thesis: verum