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 halting standard homogeneous regular J/A-independent AMI-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 halting standard homogeneous regular J/A-independent AMI-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 COMPOS_1:12;
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 COMPOS_1:54
.= (IC g) + k by A3, COMPOS_1:72 ; :: thesis: verum