theorem :: COMPOS_1:74
for S being COM-Struct
for n being Nat
for i being Instruction of S holds Macro (IncAddr (i,n)) = IncAddr ((Macro i),n)