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