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

let k be Nat; :: thesis: UsedI*Loc I = UsedI*Loc (Reloc (I,k))

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

UsedI*Loc (Reloc (I,k)) = UsedI*Loc (Reloc (I,k))

.= UsedI*Loc (Shift (I,k)) by Th40, A1

.= UsedI*Loc I by Th38 ;

hence UsedI*Loc I = UsedI*Loc (Reloc (I,k)) ; :: thesis: verum

let k be Nat; :: thesis: UsedI*Loc I = UsedI*Loc (Reloc (I,k))

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

UsedI*Loc (Reloc (I,k)) = UsedI*Loc (Reloc (I,k))

.= UsedI*Loc (Shift (I,k)) by Th40, A1

.= UsedI*Loc I by Th38 ;

hence UsedI*Loc I = UsedI*Loc (Reloc (I,k)) ; :: thesis: verum