:: deftheorem defines halt COMPOS_1:def 10 :
for S being COM-Struct holds halt S = halt the InstructionsF of S;