let S be with_non_trivial_Instructions COM-Struct ; for I, J being MacroInstruction of S
for j being Nat st j <= LastLoc J holds
(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
let I, J be MacroInstruction of S; for j being Nat st j <= LastLoc J holds
(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
let j be Nat; ( j <= LastLoc J implies (I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I)) )
assume A1:
j <= LastLoc J
; (I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
set k = (LastLoc I) + j;
A2:
LastLoc I = (card I) -' 1
by AFINSQ_1:70;
A3:
j <= (card J) - 1
by A1, AFINSQ_1:91;
(card J) - 1 < card J
by XREAL_1:44;
then
j < card J
by A3, XXREAL_0:2;
then A4:
j in dom J
by AFINSQ_1:86;
then A5:
j in dom (IncAddr (J,(LastLoc I)))
by COMPOS_1:def 21;
A6:
(LastLoc I) + j in dom (Reloc (J,(LastLoc I)))
by A4, COMPOS_1:46;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
(I ';' J) . ((LastLoc I) + j) =
(Reloc (J,(LastLoc I))) . ((LastLoc I) + j)
by A6, A2, FUNCT_4:13
.=
(IncAddr (J,(LastLoc I))) . j
by A5, VALUED_1:def 12
.=
IncAddr ((J /. j),(LastLoc I))
by A4, COMPOS_1:def 21
;
hence
(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
; verum