let s be data-only FinPartState of SCM ; :: thesis: for p being FinPartState of SCM
for k being Element of NAT st IC SCM in dom p holds
Relocated (p +* s),k = (Relocated p,k) +* s
let p be FinPartState of SCM ; :: thesis: for k being Element of NAT st IC SCM in dom p holds
Relocated (p +* s),k = (Relocated p,k) +* s
let k be Element of NAT ; :: thesis: ( IC SCM in dom p implies Relocated (p +* s),k = (Relocated p,k) +* s )
A1: dom s c= SCM-Data-Loc by AMI_1:139, AMI_3:72;
then dom s misses NAT by AMI_2:29, XBOOLE_1:63;
then A2: ProgramPart (p +* s) = ProgramPart p by FUNCT_4:76;
not IC SCM in SCM-Data-Loc

proof

assume IC SCM in SCM-Data-Loc ; :: thesis: contradiction
then IC SCM is Data-Location by AMI_3:def 2;
hence contradiction by AMI_5:20; :: thesis: verum

end;

then A3: not IC SCM in dom s by A1;
assume IC SCM in dom p ; :: thesis: Relocated (p +* s),k = (Relocated p,k) +* s
then A5: IC SCM in (dom p) \/ (dom s) by XBOOLE_0:def 3;
A6: IC (p +* s) = (p +* s) . (IC SCM )
.= p . (IC SCM ) by A5, A3, FUNCT_4:def 1
.= IC p ;
DataPart (p +* s) = (DataPart p) +* (DataPart s) by FUNCT_4:75
.= (DataPart p) +* s by A1, AMI_3:72, RELAT_1:97 ;
hence Relocated (p +* s),k = (Relocated p,k) +* s by A6, A2, FUNCT_4:15; :: thesis: verum