theorem :: COMPOS_1:76

for S being COM-Struct
for n being Nat
for i being Instruction of S holds IncAddr ((Macro i),n) = (IncAddr ((Load i),n)) ^ (Stop S)