:: deftheorem Def7 defines unique-halt COMPOS_1:def 15 :
for S being COM-Struct
for F being non empty preProgram of S holds
( F is unique-halt iff for f being Nat st F . f = halt S & f in dom F holds
f = LastLoc F );