let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for J, I being MacroInstruction of S
for j being Nat st j <= LastLoc J holds
(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
let J, I 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 Z0: j <= LastLoc J ; :: thesis: (I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
set k = (LastLoc I) + j;
F: LastLoc I = (card I) -' 1 by AFINSQ_1:70;
X: j <= (card J) - 1 by Z0, Th29;
(card J) - 1 < card J by XREAL_1:44;
then j < card J by X, XXREAL_0:2;
then D: j in dom J by NAT_1:44;
then C: j in dom (IncAddr (J,(LastLoc I))) by COMPOS_1:def 21;
E: (LastLoc I) + j in dom (Reloc (J,(LastLoc I))) by D, 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 E, F, FUNCT_4:13
.= (IncAddr (J,(LastLoc I))) . j by C, VALUED_1:def 12
.= IncAddr ((J /. j),(LastLoc I)) by D, COMPOS_1:def 21 ;
hence (I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I)) ; :: thesis: verum