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 IC S in dom (Relocated 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 IC S in dom (Relocated g,k)
let g be FinPartState of S; :: thesis: for k being Element of NAT holds IC S in dom (Relocated g,k)
let k be Element of NAT ; :: thesis: IC S in dom (Relocated g,k)
( Relocated g,k = (IncrIC (NPP g),k) +* (Reloc (ProgramPart g),k) & IC S in dom (IncrIC (NPP g),k) ) by COMPOS_1:53;
hence IC S in dom (Relocated g,k) by FUNCT_4:13; :: thesis: verum