let S be with_non_trivial_Instructions COM-Struct ; :: thesis: 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; :: thesis: for j being Nat st j <= LastLoc J holds
(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
let j be Nat; :: thesis: ( j <= LastLoc J implies (I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I)) )
assume A1: j <= LastLoc J ; :: thesis: (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)) ; :: thesis: verum