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 DataPart (Relocated g,k) = DataPart g
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 DataPart (Relocated g,k) = DataPart g
let g be FinPartState of S; :: thesis: for k being Element of NAT holds DataPart (Relocated g,k) = DataPart g
let k be Element of NAT ; :: thesis: DataPart (Relocated g,k) = DataPart g
dom (Reloc (ProgramPart g),k) c= NAT by RELAT_1:def 18;
then dom (Reloc (ProgramPart g),k) misses Data-Locations S by COMPOS_1:51, XBOOLE_1:63;
hence DataPart (Relocated g,k) = DataPart (IncrIC (NPP g),k) by FUNCT_4:76
.= DataPart (NPP g) by COMPOS_1:48
.= DataPart g by COMPOS_1:73 ;
:: thesis: verum