let p be FinPartState of SCM+FSA ; :: thesis: for k being Element of NAT holds IC (Relocated p,k) = (IC p) + k
let k be Element of NAT ; :: thesis: IC (Relocated p,k) = (IC p) + k
A1: Relocated p,k = (Start-At ((IC p) + k)) +* ((IncAddr [(Shift (ProgramPart p),k)],k) +* (DataPart p)) by FUNCT_4:15;
ProgramPart (Relocated p,k) = IncAddr [(Shift (ProgramPart p),k)],k by Th2;
then ( not IC SCM+FSA in dom (IncAddr [(Shift (ProgramPart p),k)],k) & not IC SCM+FSA in dom (DataPart p) ) by AMI_1:100, AMI_1:101;
then A2: not IC SCM+FSA in dom ((IncAddr [(Shift (ProgramPart p),k)],k) +* (DataPart p)) by FUNCT_4:13;
IC SCM+FSA in dom (Relocated p,k) by Th5;
hence IC (Relocated p,k) = (Relocated p,k) . (IC SCM+FSA ) by AMI_1:def 43
.= (Start-At ((IC p) + k)) . (IC SCM+FSA ) by A1, A2, FUNCT_4:12
.= (IC p) + k by FUNCOP_1:87 ;
:: thesis: verum