for S being with_non_trivial_Instructions COM-Struct
for I being halt-ending Program of S holds I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S))