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
for q being data-only FinPartState of S st IC S in dom g holds
Relocated (g +* q),k = (Relocated g,k) +* q
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
for q being data-only FinPartState of S st IC S in dom g holds
Relocated (g +* q),k = (Relocated g,k) +* q
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
for q being data-only FinPartState of S st IC S in dom g holds
Relocated (g +* q),k = (Relocated g,k) +* q
let g be FinPartState of S; :: thesis: for q being data-only FinPartState of S st IC S in dom g holds
Relocated (g +* q),k = (Relocated g,k) +* q
let q be data-only FinPartState of S; :: thesis: ( IC S in dom g implies Relocated (g +* q),k = (Relocated g,k) +* q )
assume IC S in dom g ; :: thesis: Relocated (g +* q),k = (Relocated g,k) +* q
then A2: IC S in (dom g) \/ (dom q) by XBOOLE_0:def 3;
set I = NAT ;
set B = Data-Locations S;
A3: dom q c= Data-Locations S by AMI_1:139;
then A4: not IC S in dom q by Lm10;
A5: IC (g +* q) = (g +* q) . (IC S)
.= g . (IC S) by A2, A4, FUNCT_4:def 1
.= IC g ;
NAT misses Data-Locations S by Lm9;
then dom q misses NAT by A3, XBOOLE_1:63;
then A6: ProgramPart (g +* q) = ProgramPart g by FUNCT_4:76;
DataPart (g +* q) = (g | (Data-Locations S)) +* (q | (Data-Locations S)) by FUNCT_4:75
.= (DataPart g) +* q by A3, RELAT_1:97 ;
hence Relocated (g +* q),k = (Relocated g,k) +* q by A5, A6, FUNCT_4:15; :: thesis: verum