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
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 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
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 NAT ,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 A2: IC S in dom g ; :: thesis: Relocated (g +* q),k = (Relocated g,k) +* q
then A3: IC S in (dom g) \/ (dom q) by XBOOLE_0:def 3;
set I = NAT ;
set B = Data-Locations S;
A4: dom q c= Data-Locations S by AMI_1:139;
then A5: not IC S in dom q by Lm2;
IC S in dom (g +* q) by A3, FUNCT_4:def 1;
then A6: IC (g +* q) = (g +* q) . (IC S) by AMI_1:def 43
.= g . (IC S) by A3, A5, FUNCT_4:def 1
.= IC g by A2, AMI_1:def 43 ;
NAT misses Data-Locations S by Lm3;
then dom q misses NAT by A4, XBOOLE_1:63;
then A7: ProgramPart (g +* q) = ProgramPart g by FUNCT_4:76;
A8: DataPart (g +* q) = (g | (Data-Locations S)) +* (q | (Data-Locations S)) by FUNCT_4:75
.= (DataPart g) +* q by A4, RELAT_1:97 ;
thus Relocated (g +* q),k = (Relocated g,k) +* q by A6, A7, A8, FUNCT_4:15; :: thesis: verum