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 )
assume A1: IC SCM in dom p ; :: thesis: Relocated (p +* s),k = (Relocated p,k) +* s
then A2: IC SCM in (dom p) \/ (dom s) by XBOOLE_0:def 3;
A3: 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;

A4: dom s c= SCM-Data-Loc by AMI_1:139, AMI_3:72;
then A5: not IC SCM in dom s by A3;
IC SCM in dom (p +* s) by A2, FUNCT_4:def 1;
then A6: IC (p +* s) = (p +* s) . (IC SCM ) by AMI_1:def 43
.= p . (IC SCM ) by A2, A5, FUNCT_4:def 1
.= IC p by A1, AMI_1:def 43 ;
dom s misses NAT by A4, AMI_2:29, XBOOLE_1:63;
then A7: ProgramPart (p +* s) = ProgramPart p by FUNCT_4:76;
A8: DataPart (p +* s) = (DataPart p) +* (DataPart s) by FUNCT_4:75
.= (DataPart p) +* s by A4, AMI_3:72, RELAT_1:97 ;
thus Relocated (p +* s),k = (Relocated p,k) +* s by A6, A7, A8, FUNCT_4:15; :: thesis: verum