let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for g being FinPartState of S
for il being Element of NAT st S is realistic holds
( il in dom g iff il + k,S in dom (Relocated g,k) )
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for g being FinPartState of S
for il being Element of NAT st S is realistic holds
( il in dom g iff il + k,S in dom (Relocated g,k) )
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for g being FinPartState of S
for il being Element of NAT st S is realistic holds
( il in dom g iff il + k,S in dom (Relocated g,k) )
let g be FinPartState of S; :: thesis: for il being Element of NAT st S is realistic holds
( il in dom g iff il + k,S in dom (Relocated g,k) )
let il be Element of NAT ; :: thesis: ( S is realistic implies ( il in dom g iff il + k,S in dom (Relocated g,k) ) )
assume A1: S is realistic ; :: thesis: ( il in dom g iff il + k,S in dom (Relocated g,k) )
consider m being natural number such that
A2: il = il. S,m by AMISTD_1:26;
A3: il + k,S = il. S,(m + k) by A2, AMISTD_1:def 13;
A4: dom (ProgramPart (Relocated g,k)) = { (il. S,(j + k)) where j is Element of NAT : il. S,j in dom (ProgramPart g) } by A1, Th70;
ProgramPart (Relocated g,k) c= Relocated g,k by RELAT_1:88;
then A5: dom (ProgramPart (Relocated g,k)) c= dom (Relocated g,k) by GRFUNC_1:8;
A6: m is Element of NAT by ORDINAL1:def 13;

hereby :: thesis: ( il + k,S in dom (Relocated g,k) implies il in dom g )

assume il in dom g ; :: thesis: il + k,S in dom (Relocated g,k)
then il. S,m in dom (ProgramPart g) by A2, AMI_1:106;
then il + k,S in dom (ProgramPart (Relocated g,k)) by A3, A4, A6;
hence il + k,S in dom (Relocated g,k) by A5; :: thesis: verum

end;

assume il + k,S in dom (Relocated g,k) ; :: thesis: il in dom g
then il + k,S in dom (ProgramPart (Relocated g,k)) by AMI_1:106;
then consider j being Element of NAT such that
A7: il + k,S = il. S,(j + k) and
A8: il. S,j in dom (ProgramPart g) by A4;
ProgramPart g c= g by RELAT_1:88;
then A9: dom (ProgramPart g) c= dom g by GRFUNC_1:8;
m + k = j + k by A3, A7, AMISTD_1:25;
hence il in dom g by A2, A8, A9; :: thesis: verum