let I, J be Program of SCM+FSA; :: thesis: for k being 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 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) ;
k -' (card I) = k - (card I) by A1, XREAL_1:233;
then k -' (card I) < (card J) - 0 by A2, XREAL_1:21;
then A3: k -' (card I) in dom J by AFINSQ_1:66;
let i be Instruction of SCM+FSA; :: thesis: ( i = J . (k -' (card I)) implies (I ";" J) . k = IncAddr (i,(card I)) )
assume A4: i = J . (k -' (card I)) ; :: thesis: (I ";" J) . k = IncAddr (i,(card I))
A5: (k -' (card I)) + (card I) = (k - (card I)) + (card I) by A1, XREAL_1:233
.= k ;
then k in { (m + (card I)) where m is Nat : m in dom J } by A3;
then k in dom (Reloc (J,(card I))) by COMPOS_1:33;
hence (I ";" J) . k = (Reloc (J,(card I))) . k by SCMFSA6A:40
.= IncAddr (i,(card I)) by A4, A3, A5, COMPOS_1:35 ;
:: thesis: verum