let S be with_non_trivial_Instructions COM-Struct ; :: thesis: 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
let I be unique-halt Program of S; :: thesis: for J being halt-ending Program of S st CutLastLoc I c= J holds
CutLastLoc I c= CutLastLoc J
let J be halt-ending Program of S; :: thesis: ( CutLastLoc I c= J implies CutLastLoc I c= CutLastLoc J )
assume A1: CutLastLoc I c= J ; :: thesis: CutLastLoc I c= CutLastLoc J
A2: not halt S in rng (CutLastLoc I) by COMPOS_1:def 11;
J . (LastLoc J) = halt S by COMPOS_1:def 14;
hence CutLastLoc I c= CutLastLoc J by A2, A1, Lm1; :: thesis: verum