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