theorem :: COMPOS_2:4

for S being with_non_trivial_Instructions COM-Struct
for i being No-StopCode Instruction of S
for J, K being MacroInstruction of S holds (i ';' J) ';' K = i ';' (J ';' K) by COMPOS_1:29;