:: deftheorem defines ';' COMPOS_2:def 2 :
for S being with_non_trivial_Instructions COM-Struct
for I being MacroInstruction of S
for j being No-StopCode Instruction of S holds I ';' j = I ';' (Macro j);