theorem :: COMPOS_2:9

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