let I, J be Program of SCM+FSA; :: thesis: for k being Element of NAT st card I <= k & k < (card I) + (card J) holds
for i being Instruction of SCM+FSA st i = J . (k -' (card I)) holds
(I ';' J) . k = IncAddr (i,(card I))
let k be Element of NAT ; :: thesis: ( card I <= k & k < (card I) + (card J) implies for i being Instruction of SCM+FSA st i = J . (k -' (card I)) holds
(I ';' J) . k = IncAddr (i,(card I)) )
assume A1: card I <= k ; :: thesis: ( not k < (card I) + (card J) or for i being Instruction of SCM+FSA st i = J . (k -' (card I)) holds
(I ';' J) . k = IncAddr (i,(card I)) )
assume k < (card I) + (card J) ; :: thesis: for i being Instruction of SCM+FSA st i = J . (k -' (card I)) holds
(I ';' J) . k = IncAddr (i,(card I))
then A2: k + 0 < (card J) + (card I) ;
A3: ProgramPart J = J by RELAT_1:209;
k -' (card I) = k - (card I) by A1, XREAL_1:235;
then k -' (card I) < (card J) - 0 by A2, XREAL_1:23;
then A4: k -' (card I) in dom (ProgramPart J) by A3, AFINSQ_1:70;
let i be Instruction of SCM+FSA; :: thesis: ( i = J . (k -' (card I)) implies (I ';' J) . k = IncAddr (i,(card I)) )
assume A5: i = J . (k -' (card I)) ; :: thesis: (I ';' J) . k = IncAddr (i,(card I))
A6: (k -' (card I)) + (card I) = (k - (card I)) + (card I) by A1, XREAL_1:235
.= k ;
then k in { (m + (card I)) where m is Element of NAT : m in dom (ProgramPart J) } by A4;
then k in dom (Reloc ((ProgramPart J),(card I))) by COMPOS_1:117;
then A7: k in dom (ProgramPart (Relocated (J,(card I)))) by COMPOS_1:116;
hence (I ';' J) . k = (ProgramPart (Relocated (J,(card I)))) . k by FUNCT_4:14
.= (Relocated (J,(card I))) . k by A7, SCMFSA6A:64
.= IncAddr (i,(card I)) by A5, A4, A6, COMPOS_1:122 ;
:: thesis: verum