let p be FinPartState of SCM ; :: thesis: for k being Element of NAT st IC SCM in dom p holds
IC (Relocated p,k) = (IC p) + k
let k be Element of NAT ; :: thesis: ( IC SCM in dom p implies IC (Relocated p,k) = (IC p) + k )
assume A3: IC SCM in dom p ; :: thesis: IC (Relocated p,k) = (IC p) + k
ProgramPart (Relocated p,k) = Reloc (ProgramPart p),k by AMISTD_2:69;
then A1: not IC SCM in dom (Reloc (ProgramPart p),k) by COMPOS_1:12;
A2: ( Relocated p,k = (IncrIC (NPP p),k) +* (Reloc (ProgramPart p),k) & not IC SCM in dom (Reloc (ProgramPart p),k) ) by A1, FUNCT_4:13, FUNCT_4:15;
thus IC (Relocated p,k) = (Relocated p,k) . (IC SCM )
.= IC (IncrIC (NPP p),k) by A2, FUNCT_4:12
.= (IC (NPP p)) + k by COMPOS_1:54
.= (IC p) + k by A3, COMPOS_1:72 ; :: thesis: verum