let k be Element of NAT ; :: thesis: for p being FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)
let p be FinPartState of SCM ; :: thesis: for s1, s2 being State of SCM st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)
let s1, s2 be State of SCM ; :: thesis: ( p c= s1 & Relocated p,k c= s2 implies p c= s1 +* (DataPart s2) )
assume that
A1: p c= s1 and
A2: Relocated p,k c= s2 ; :: thesis: p c= s1 +* (DataPart s2)
set s3 = DataPart s2;
reconsider s = s1 +* (DataPart s2) as State of SCM ;
A3: dom p c= ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by AMI_5:23, RELAT_1:def 18;

A4: now

SCM-Data-Loc = (dom s2) /\ SCM-Data-Loc by AMI_5:27, XBOOLE_1:28;
then A5: dom (DataPart s2) = SCM-Data-Loc by AMI_3:72, RELAT_1:90;
let x be set ; :: thesis: ( x in dom p implies p . b₁ = s . b₁ )
assume A6: x in dom p ; :: thesis: p . b₁ = s . b₁
A7: ( x in {(IC SCM )} \/ SCM-Data-Loc or x in NAT ) by A3, A6, XBOOLE_0:def 3;

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

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

A9: 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;

x = IC SCM by A8, TARSKI:def 1;
then s1 . x = s . x by A5, A9, FUNCT_4:12;
hence p . x = s . x by A1, A6, GRFUNC_1:8; :: thesis: verum

end;

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

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

end;

suppose A16: 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 AMI_3:72, RELAT_1:90;
then x in SCM-Data-Loc by XBOOLE_0:def 4;
hence contradiction by A16, 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, A6, GRFUNC_1:8; :: thesis: verum

end;

end;

end;

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