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 S 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 S 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 S in dom g holds
IC (Relocated (g,k)) = (IC g) + k
let k be Element of NAT ; :: thesis: ( IC S in dom g implies IC (Relocated (g,k)) = (IC g) + k )
assume A3: IC S in dom g ; :: thesis: IC (Relocated (g,k)) = (IC g) + k
ProgramPart (Relocated (g,k)) = Reloc ((ProgramPart g),k) by Th69;
then A1: not IC S in dom (Reloc ((ProgramPart g),k)) by Th12;
thus IC (Relocated (g,k)) = (Relocated (g,k)) . (IC S)
.= IC (IncrIC ((NPP g),k)) by A1, FUNCT_4:12
.= (IC (NPP g)) + k by Th54
.= (IC g) + k by A3, Th72 ; :: thesis: verum