let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I, J being MacroInstruction of S st CutLastLoc I = CutLastLoc J holds
I = J
let I, J be MacroInstruction of S; :: thesis: ( CutLastLoc I = CutLastLoc J implies I = J )
assume Z: CutLastLoc I = CutLastLoc J ; :: thesis: I = J
(card I) - 1 = card (CutLastLoc J) by Z, 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 Thx
.= J by Z, Thx ;
:: thesis: verum