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
ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),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 st S is realistic holds
ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),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 st S is realistic holds
ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k
let g be FinPartState of S; :: thesis: ( S is realistic implies ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k )
assume A1: S is realistic ; :: thesis: ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k
set I = NAT ;
set B = the carrier of S \ ({(IC S)} \/ NAT );
set X = (Start-At ((IC g) + k,S),S) | NAT ;
set f = IncAddr (Shift (ProgramPart g),k),k;
consider x being Element of dom ((Start-At ((IC g) + k,S),S) | NAT );

A2: now

assume (Start-At ((IC g) + k,S),S) | NAT <> {} ; :: thesis: contradiction
then dom ((Start-At ((IC g) + k,S),S) | NAT ) <> {} ;
then x in dom ((Start-At ((IC g) + k,S),S) | NAT ) ;
then A3: x in (dom (Start-At ((IC g) + k,S),S)) /\ NAT by RELAT_1:90;
then x in NAT by XBOOLE_0:def 4;
then reconsider x = x as Element of NAT ;
x in dom (Start-At ((IC g) + k,S),S) by A3, XBOOLE_0:def 4;
then x in {(IC S)} by FUNCOP_1:19;
then x = IC S by TARSKI:def 1;
hence contradiction by A1, AMI_1:48; :: thesis: verum

end;

A4: dom (IncAddr (Shift (ProgramPart g),k),k) c= NAT by RELAT_1:def 18;
A5: dom (DataPart g) c= the carrier of S \ ({(IC S)} \/ NAT ) by RELAT_1:87;
A6: NAT misses the carrier of S \ ({(IC S)} \/ NAT ) by Lm9;
thus ProgramPart (Relocated g,k) = ((Start-At ((IC g) + k,S),S) +* ((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g))) | NAT by FUNCT_4:15
.= ((Start-At ((IC g) + k,S),S) | NAT ) +* (((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g)) | NAT ) by FUNCT_4:75
.= ((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g)) | NAT by A2, FUNCT_4:21
.= IncAddr (Shift (ProgramPart g),k),k by A4, A5, A6, FUNCT_4:81 ; :: thesis: verum