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 st S is realistic holds
IC (Relocated g,k) = (IC g) + k,S
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 st S is realistic holds
IC (Relocated g,k) = (IC g) + k,S
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 st S is realistic holds
IC (Relocated g,k) = (IC g) + k,S
let g be FinPartState of S; :: thesis: ( S is realistic implies IC (Relocated g,k) = (IC g) + k,S )
assume A1: S is realistic ; :: thesis: IC (Relocated g,k) = (IC g) + k,S
A2: Relocated g,k = (Start-At ((IC g) + k,S),S) +* ((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g)) by FUNCT_4:15;
ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k by A1, Th69;
then A3: not IC S in dom (IncAddr (Shift (ProgramPart g),k),k) by A1, AMI_1:101;
not IC S in dom (DataPart g) by AMI_1:100;
then A4: not IC S in dom ((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g)) by A3, FUNCT_4:13;
thus IC (Relocated g,k) = (Relocated g,k) . (IC S)
.= (Start-At ((IC g) + k,S),S) . (IC S) by A2, A4, FUNCT_4:12
.= (IC g) + k,S by FUNCOP_1:87 ; :: thesis: verum