for S being with_non_trivial_Instructions COM-Struct
for I being unique-halt Program of S
for J being halt-ending Program of S st CutLastLoc I c= J holds
CutLastLoc I c= CutLastLoc J