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 holds IC 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 holds IC 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 holds IC S in dom (Relocated g,k)
let g be FinPartState of S; :: thesis: IC S in dom (Relocated g,k)
A1: Relocated g,k = (Start-At ((IC g) + k,S),S) +* ((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g)) by FUNCT_4:15;
dom (Start-At ((IC g) + k,S),S) = {(IC S)} by FUNCOP_1:19;
then IC S in dom (Start-At ((IC g) + k,S),S) by TARSKI:def 1;
hence IC S in dom (Relocated g,k) by A1, FUNCT_4:13; :: thesis: verum