let k be natural number ; :: thesis: for R being good Ring
for s1, s2 being State of (SCM R)
for p being autonomic FinPartState of (SCM R) st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)
let R be good Ring; :: thesis: for s1, s2 being State of (SCM R)
for p being autonomic FinPartState of (SCM R) st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)
let s1, s2 be State of (SCM R); :: thesis: for p being autonomic FinPartState of (SCM R) st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)
X: Data-Locations (SCM R) = SCM-Data-Loc by SCMRING2:31;
let p be autonomic FinPartState of (SCM R); :: thesis: ( p c= s1 & Relocated p,k c= s2 implies p c= s1 +* (DataPart s2) )
assume A1: ( p c= s1 & Relocated p,k c= s2 ) ; :: thesis: p c= s1 +* (DataPart s2)
reconsider s = s1 +* (DataPart s2) as State of (SCM R) ;
set s3 = DataPart s2;
A2: dom p c= the carrier of (SCM R) by AMI_1:80;
then A3: dom p c= ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT by Th14;
A4: dom p c= dom s by A2, AMI_1:79;

now

let x be set ; :: thesis: ( x in dom p implies p . b₁ = s . b₁ )
assume A5: x in dom p ; :: thesis: p . b₁ = s . b₁
dom s2 = the carrier of (SCM R) by AMI_1:79
.= SCM-Memory by SCMRING2:def 1 ;
then A6: SCM-Data-Loc = (dom s2) /\ SCM-Data-Loc by XBOOLE_1:28;
A7: ( x in {(IC (SCM R))} \/ SCM-Data-Loc or x in NAT ) by A3, A5, XBOOLE_0:def 3;

per cases ( x in {(IC (SCM R))} or x in SCM-Data-Loc or x in NAT ) by A7, XBOOLE_0:def 3;

suppose x in {(IC (SCM R))} ; :: thesis: p . b₁ = s . b₁

then A8: x = IC (SCM R) by TARSKI:def 1;
not IC (SCM R) in SCM-Data-Loc

proof

assume IC (SCM R) in SCM-Data-Loc ; :: thesis: contradiction
then IC (SCM R) is Data-Location of R by SCMRING2:1;
hence contradiction by SCMRING3:3; :: thesis: verum

end;

then not IC (SCM R) in dom (DataPart s2) by A6, X, RELAT_1:90;
then s1 . x = s . x by A8, FUNCT_4:12;
hence p . x = s . x by A1, A5, GRFUNC_1:8; :: thesis: verum

end;

suppose A9: x in SCM-Data-Loc ; :: thesis: p . b₁ = s . b₁

set DPp = DataPart p;
set DPRp = DataPart (Relocated p,k);
x in (dom p) /\ SCM-Data-Loc by A5, A9, XBOOLE_0:def 4;
then A11: x in dom (DataPart p) by X, RELAT_1:90;
DataPart p c= p by RELAT_1:88;
then A12: (DataPart p) . x = p . x by A11, GRFUNC_1:8;
DataPart p = DataPart (Relocated p,k) by AMISTD_2:68;
then DataPart p c= Relocated p,k by RELAT_1:88;
then A13: DataPart p c= s2 by A1, XBOOLE_1:1;
then A14: (DataPart p) . x = s2 . x by A11, GRFUNC_1:8;
A15: dom (DataPart p) c= dom s2 by A13, GRFUNC_1:8;
A16: s2 . x = (DataPart s2) . x by A9, X, FUNCT_1:72;
x in (dom s2) /\ SCM-Data-Loc by A9, A11, A15, XBOOLE_0:def 4;
then x in dom (DataPart s2) by X, RELAT_1:90;
hence p . x = s . x by A12, A14, A16, FUNCT_4:14; :: thesis: verum

end;

suppose A17: x in NAT ; :: thesis: p . b₁ = s . b₁

now

assume x in dom (DataPart s2) ; :: thesis: contradiction
then x in (dom s2) /\ SCM-Data-Loc by X, RELAT_1:90;
then x in SCM-Data-Loc by XBOOLE_0:def 4;
hence contradiction by A17, AMI_2:29, XBOOLE_0:3; :: thesis: verum

end;

then s1 . x = s . x by FUNCT_4:12;
hence p . x = s . x by A1, A5, GRFUNC_1:8; :: thesis: verum

end;

end;

end;

hence p c= s1 +* (DataPart s2) by A4, GRFUNC_1:8; :: thesis: verum