:: deftheorem defines Macro COMPOS_1:def 25 :
for S being COM-Struct
for i being Instruction of S holds Macro i = stop (Load i);