let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for p being FinPartState of S
for s1, s2 being State of S st NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
NPP p c= s1 +* (DataPart s2)
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for k being Element of NAT
for p being FinPartState of S
for s1, s2 being State of S st NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
NPP p c= s1 +* (DataPart s2)
let k be Element of NAT ; :: thesis: for p being FinPartState of S
for s1, s2 being State of S st NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
NPP p c= s1 +* (DataPart s2)
let p be FinPartState of S; :: thesis: for s1, s2 being State of S st NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
NPP p c= s1 +* (DataPart s2)
let s1, s2 be State of S; :: thesis: ( NPP p c= s1 & NPP (Relocated (p,k)) c= s2 implies NPP p c= s1 +* (DataPart s2) )
assume that
A1: NPP p c= s1 and
A2: NPP (Relocated (p,k)) c= s2 ; :: thesis: NPP p c= s1 +* (DataPart s2)
z: dom (NPP p) c= dom p by RELAT_1:25;
set s3 = DataPart s2;
reconsider s = s1 +* (DataPart s2) as State of S ;
A3: dom p c= the carrier of S by RELAT_1:def 18;
then A4: dom p c= ({(IC )} \/ (Data-Locations S)) \/ NAT by Th160;

A5: now

Data-Locations S = (dom s2) /\ (Data-Locations S) by Th49, XBOOLE_1:28;
then A6: dom (DataPart s2) = Data-Locations S by RELAT_1:90;
let x be set ; :: thesis: ( x in dom (NPP p) implies (NPP p) . b₁ = s . b₁ )
assume A7: x in dom (NPP p) ; :: thesis: (NPP p) . b₁ = s . b₁
B7: x in dom p by z, A7;
A8: ( x in {(IC )} \/ (Data-Locations S) or x in NAT ) by A4, B7, XBOOLE_0:def 3;

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

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

A10: not IC in Data-Locations S by Th56;
x = IC by A9, TARSKI:def 1;
then s1 . x = s . x by A6, A10, FUNCT_4:12;
hence (NPP p) . x = s . x by A1, A7, GRFUNC_1:8; :: thesis: verum

end;

suppose A11: x in Data-Locations S ; :: thesis: (NPP p) . b₁ = s . b₁

set DPp = DataPart p;
x in (dom p) /\ (Data-Locations S) by A11, B7, XBOOLE_0:def 4;
then A12: x in dom (DataPart p) by RELAT_1:90;
YY: DataPart p = DataPart (Relocated (p,k)) by Th115;
DataPart p c= NPP (Relocated (p,k)) by YY, Th169;
then A13: 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) /\ (Data-Locations S) by A11, A12, XBOOLE_0:def 4;
then A14: x in dom (DataPart s2) by RELAT_1:90;
DataPart p c= NPP p by Th169;
then A15: (DataPart p) . x = (NPP p) . x by A12, GRFUNC_1:8;
A16: s2 . x = (DataPart s2) . x by A11, FUNCT_1:72;
(DataPart p) . x = s2 . x by A12, A13, GRFUNC_1:8;
hence (NPP p) . x = s . x by A15, A16, A14, FUNCT_4:14; :: thesis: verum

end;

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

dom (DataPart s2) misses NAT by Th137;
then not x in dom (DataPart s2) by A17, XBOOLE_0:3;
then s1 . x = s . x by FUNCT_4:12;
hence (NPP p) . x = s . x by A1, A7, GRFUNC_1:8; :: thesis: verum

end;

end;

end;

dom p c= dom s by A3, PARTFUN1:def 4;
then dom (NPP p) c= dom s by z, XBOOLE_1:1;
hence NPP p c= s1 +* (DataPart s2) by A5, GRFUNC_1:8; :: thesis: verum