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 AMI_1:105;
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, SCMFSA6A:15;
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 A7: k in dom (ProgramPart (Relocated J,(card I))) by SCMFSA_5:3;
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, SCMFSA_5:7 ;
:: thesis: verum