:: deftheorem defines halts_at COMPOS_1:def 13 :
for S being COM-Struct
for s being Instruction-Sequence of S
for l being Nat holds
( s halts_at l iff s . l = halt S );