let k be Element of NAT ; :: 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)
A1: Data-Locations (SCM R) = Data-Locations SCM by SCMRING2:31;
set s3 = DataPart s2;
reconsider s = s1 +* (DataPart s2) as State of (SCM R) ;
let p be autonomic FinPartState of (SCM R); :: thesis: ( p c= s1 & Relocated (p,k) c= s2 implies p c= s1 +* (DataPart s2) )
assume that
A2: p c= s1 and
A3: Relocated (p,k) c= s2 ; :: thesis: p c= s1 +* (DataPart s2)
A4: dom p c= the carrier of (SCM R) by RELAT_1:def 18;
then A5: dom p c= ({(IC (SCM R))} \/ (Data-Locations SCM)) \/ NAT by Th1;

A6: now

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

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

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

not IC (SCM R) in Data-Locations SCM

proof

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

end;

then A11: not IC (SCM R) in dom (DataPart s2) by A1, A7, RELAT_1:90;
x = IC (SCM R) by A10, TARSKI:def 1;
then s1 . x = s . x by A11, FUNCT_4:12;
hence p . x = s . x by A2, A8, GRFUNC_1:8; :: thesis: verum

end;

suppose A12: x in Data-Locations SCM ; :: thesis: p . b₁ = s . b₁

set DPRp = DataPart (Relocated (p,k));
set DPp = DataPart p;
x in (dom p) /\ (Data-Locations SCM) by A8, A12, XBOOLE_0:def 4;
then A13: x in dom (DataPart p) by A1, RELAT_1:90;
DataPart p = DataPart (Relocated (p,k)) by COMPOS_1:115;
then DataPart p c= Relocated (p,k) by RELAT_1:88;
then A14: DataPart p c= s2 by A3, XBOOLE_1:1;
then dom (DataPart p) c= dom s2 by GRFUNC_1:8;
then x in (dom s2) /\ (Data-Locations SCM) by A12, A13, XBOOLE_0:def 4;
then A15: x in dom (DataPart s2) by A1, RELAT_1:90;
A16: s2 . x = (DataPart s2) . x by A1, A12, FUNCT_1:72;
DataPart p c= p by RELAT_1:88;
then A17: (DataPart p) . x = p . x by A13, GRFUNC_1:8;
(DataPart p) . x = s2 . x by A13, A14, GRFUNC_1:8;
hence p . x = s . x by A17, A16, A15, FUNCT_4:14; :: thesis: verum

end;

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

now

assume x in dom (DataPart s2) ; :: thesis: contradiction
then x in (dom s2) /\ (Data-Locations SCM) by A1, RELAT_1:90;
then x in Data-Locations SCM by XBOOLE_0:def 4;
hence contradiction by A18, AMI_2:29, AMI_3:72, XBOOLE_0:3; :: thesis: verum

end;

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

end;

end;

end;

dom p c= dom s by A4, PARTFUN1:def 4;
hence p c= s1 +* (DataPart s2) by A6, GRFUNC_1:8; :: thesis: verum