theorem :: COMPOS_1:67

for S being COM-Struct
for i being Instruction of S holds rng (Macro i) = {i,(halt S)}