:: deftheorem Def6 defines halt-ending COMPOS_1:def 14 :
for S being COM-Struct
for F being non empty preProgram of S holds
( F is halt-ending iff F . (LastLoc F) = halt S );