theorem :: COMPOS_2:61

for S being with_non_trivial_Instructions COM-Struct
for i being No-StopCode Instruction of S st i is ins-loc-free holds
Macro i is closed