let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for I being MacroInstruction of S
for k being Nat holds
( k < LastLoc I iff k in dom (CutLastLoc I) )
let I be MacroInstruction of S; :: thesis: for k being Nat holds
( k < LastLoc I iff k in dom (CutLastLoc I) )
let k be Nat; :: thesis: ( k < LastLoc I iff k in dom (CutLastLoc I) )
card I > 0 ;
then A1: card I >= 0 + 1 by NAT_1:13;
card (CutLastLoc I) = (card I) - 1 by VALUED_1:38
.= (card I) -' 1 by A1, XREAL_1:233
.= LastLoc I by AFINSQ_1:70 ;
hence ( k < LastLoc I iff k in dom (CutLastLoc I) ) by AFINSQ_1:86; :: thesis: verum