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

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