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 NAT ,N
for g being FinPartState of S 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 NAT ,N
for g being FinPartState of S 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 NAT ,N; :: thesis: for g being FinPartState of S st S is realistic holds
IC (Relocated g,k) = (IC g) + k
let g be FinPartState of S; :: 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, Th48;
then ( not IC S in dom (IncAddr (Shift (ProgramPart g),k),k) & not IC S in dom (DataPart g) ) by A1, AMI_1:100, AMI_1:101;
then A3: not IC S in dom ((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g)) by FUNCT_4:13;
IC S in dom (Relocated g,k) by Th51;
hence IC (Relocated g,k) = (Relocated g,k) . (IC S) by AMI_1:def 43
.= (Start-At ((IC g) + k)) . (IC S) by A2, A3, FUNCT_4:12
.= (IC g) + k by FUNCOP_1:87 ;
:: thesis: verum