:: deftheorem defines halt COMPOS_0:def 11 :
for S being with_halt set holds halt S = [0,{},{}];