theorem :: COMPOS_2:8

for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S holds i ';' j = (Macro i) ';' j ;