let I, J be Program of SCM+FSA ; :: thesis: for k being Element of NAT
for i being Instruction of SCM+FSA st k < card J & i = J . (insloc k) holds
(I ';' J) . (insloc ((card I) + k)) = IncAddr i,(card I)
let k be Element of NAT ; :: thesis: for i being Instruction of SCM+FSA st k < card J & i = J . (insloc k) holds
(I ';' J) . (insloc ((card I) + k)) = IncAddr i,(card I)
let i be Instruction of SCM+FSA ; :: thesis: ( k < card J & i = J . (insloc k) implies (I ';' J) . (insloc ((card I) + k)) = IncAddr i,(card I) )
assume that
A1: k < card J and
A2: i = J . (insloc k) ; :: thesis: (I ';' J) . (insloc ((card I) + k)) = IncAddr i,(card I)
set m = (card I) + k;
A3: (card I) + k < (card I) + (card J) by A1, XREAL_1:8;
insloc (((card I) + k) -' (card I)) = insloc k by NAT_D:34;
hence (I ';' J) . (insloc ((card I) + k)) = IncAddr i,(card I) by A2, A3, NAT_1:11, SCMFSA8C:13; :: thesis: verum