:: deftheorem defines Reloc COMPOS_1:def 22 :
for S being COM-Struct
for p being preProgram of S
for k being Nat holds Reloc (p,k) = Shift ((IncAddr (p,k)),k);