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 holds ProgramPart (Relocated g,k) = Reloc (ProgramPart 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 holds ProgramPart (Relocated g,k) = Reloc (ProgramPart g),k
let g be FinPartState of S; :: thesis: for k being Element of NAT holds ProgramPart (Relocated g,k) = Reloc (ProgramPart g),k
let k be Element of NAT ; :: thesis: ProgramPart (Relocated g,k) = Reloc (ProgramPart g),k
thus ProgramPart (Relocated g,k) = ((IncrIC (NPP g),k) | NAT ) +* ((Reloc (ProgramPart g),k) | NAT ) by FUNCT_4:75
.= {} +* ((Reloc (ProgramPart g),k) | NAT ) by COMPOS_1:def 29
.= (Reloc (ProgramPart g),k) | NAT by FUNCT_4:21
.= Reloc (ProgramPart g),k by RELAT_1:209 ; :: thesis: verum