let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for j being No-StopCode Instruction of S
for I being MacroInstruction of S holds (I ';' j) . (LastLoc I) = IncAddr (j,(LastLoc I))
let j be No-StopCode Instruction of S; :: thesis: for I being MacroInstruction of S holds (I ';' j) . (LastLoc I) = IncAddr (j,(LastLoc I))
let I be MacroInstruction of S; :: thesis: (I ';' j) . (LastLoc I) = IncAddr (j,(LastLoc I))
A1: 0 <= LastLoc (Macro j) ;
0 in dom (Macro j) by COMPOS_1:57;
then A2: (Macro j) /. 0 = (Macro j) . 0 by PARTFUN1:def 6
.= j by COMPOS_1:58 ;
thus (I ';' j) . (LastLoc I) = (I ';' (Macro j)) . ((LastLoc I) + 0)
.= IncAddr (((Macro j) /. 0),(LastLoc I)) by A1, Th43
.= IncAddr (j,(LastLoc I)) by A2 ; :: thesis: verum