let p be FinPartState of ; :: 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
ProgramPart (Relocated p,k) = IncAddr (Shift (ProgramPart p),k),k by Th22;
then A1: not IC SCM in dom (IncAddr (Shift (ProgramPart p),k),k) by AMI_1:101;
not IC SCM in dom (DataPart p) by AMI_1:100;
then A2: ( Relocated p,k = (Start-At ((IC p) + k)) +* ((IncAddr (Shift (ProgramPart p),k),k) +* (DataPart p)) & not IC SCM in dom ((IncAddr (Shift (ProgramPart p),k),k) +* (DataPart p)) ) by A1, FUNCT_4:13, FUNCT_4:15;
IC SCM in dom (Relocated p,k) by Th25;
hence IC (Relocated p,k) = (Relocated p,k) . (IC SCM ) by AMI_1:def 43
.= (Start-At ((IC p) + k)) . (IC SCM ) by A2, FUNCT_4:12
.= (IC p) + k by FUNCOP_1:87 ;
:: thesis: verum