let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for g being FinPartState of S
for k being Element of NAT st IC in dom g holds
IC (Relocated (g,k)) = (IC g) + k
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for g being FinPartState of S
for k being Element of NAT st IC in dom g holds
IC (Relocated (g,k)) = (IC g) + k
let g be FinPartState of S; :: thesis: for k being Element of NAT st IC in dom g holds
IC (Relocated (g,k)) = (IC g) + k
let k be Element of NAT ; :: thesis: ( IC in dom g implies IC (Relocated (g,k)) = (IC g) + k )
assume A1: IC in dom g ; :: thesis: IC (Relocated (g,k)) = (IC g) + k
ProgramPart (Relocated (g,k)) = Reloc ((ProgramPart g),k) by Th116;
then A2: not IC in dom (Reloc ((ProgramPart g),k)) by Th12;
thus IC (Relocated (g,k)) = (Relocated (g,k)) . (IC )
.= IC (IncIC ((NPP g),k)) by A2, FUNCT_4:12
.= (IC (NPP g)) + k by Th54
.= (IC g) + k by A1, Th72 ; :: thesis: verum