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