theorem Th43: :: COMPOS_1:59

for S being COM-Struct
for i being Instruction of S holds (Macro i) . 1 = halt S