theorem Th21: :: COMPOS_2:21

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