for S being COM-Struct
for F being unique-halt Program of S
for I being Nat st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S