let k be natural number ; :: thesis: for N being 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 st S is realistic holds
IC (Relocated g,k) = (IC g) + k
let N be 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 st S is realistic holds
IC (Relocated g,k) = (IC 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 st S is realistic holds
IC (Relocated g,k) = (IC g) + k
let g be FinPartState of ; :: thesis: ( S is realistic implies IC (Relocated g,k) = (IC g) + k )
assume A1: S is realistic ; :: thesis: IC (Relocated g,k) = (IC g) + k
A2: Relocated g,k = (Start-At ((IC g) + k)) +* ((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;
IC S in dom (Relocated g,k) by Th72;
hence IC (Relocated g,k) = (Relocated g,k) . (IC S) by AMI_1:def 43
.= (Start-At ((IC g) + k)) . (IC S) by A2, A4, FUNCT_4:12
.= (IC g) + k by FUNCOP_1:87 ;
:: thesis: verum