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
B1: ProgramPart (Relocated (p,k)) = Reloc ((ProgramPart p),k) by COMPOS_1:116;
A2: ( Relocated (p,k) = (IncrIC ((NPP p),k)) +* (Reloc ((ProgramPart p),k)) & not IC SCM in dom (Reloc ((ProgramPart p),k)) ) by B1, COMPOS_1:12;
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