let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for J being MacroInstruction of S
for I being halt-ending Program of S st CutLastLoc I = CutLastLoc J holds
I = J
let J be MacroInstruction of S; :: thesis: for I being halt-ending Program of S st CutLastLoc I = CutLastLoc J holds
I = J
let I be halt-ending Program of S; :: thesis: ( CutLastLoc I = CutLastLoc J implies I = J )
assume A1: CutLastLoc I = CutLastLoc J ; :: thesis: I = J
(card I) - 1 = card (CutLastLoc J) by A1, VALUED_1:38
.= (card J) - 1 by VALUED_1:38 ;
then LastLoc I = (card J) -' 1 by AFINSQ_1:70
.= LastLoc J by AFINSQ_1:70 ;
hence I = (CutLastLoc I) +* ((LastLoc J) .--> (halt S)) by Th20
.= J by A1, Th20 ;
:: thesis: verum