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 st IC in dom p holds
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 st IC in dom p holds
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 st IC in dom p holds
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: ( IC in dom p implies 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) )
assume ZD: IC in dom p ; :: 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)
set s3 = DataPart s2;
reconsider s = s1 +* (DataPart s2) as State of S ;
A3: dom (NPP p) c= the carrier of S by RELAT_1:def 18;
then A4: dom (NPP 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₁
A8: ( x in {(IC )} \/ (Data-Locations S) or x in NAT ) by A4, A7, 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 (NPP p);
ProgramPart (NPP p) = ProgramPart (p \ (ProgramPart p))
.= {} by RELAT_1:216 ;
then YY: NPP p = (NPP p) \ (ProgramPart (NPP p))
.= NPP (NPP p) ;
IC in dom (NPP p) by ZD, Lm179;
then XX: NPP (Relocated ((NPP p),k)) = IncIC ((NPP (NPP p)),k) by LmXX
.= IncIC ((NPP p),k) by YY
.= NPP (Relocated (p,k)) by LmXX, ZD ;
x in (dom (NPP p)) /\ (Data-Locations S) by A7, A11, XBOOLE_0:def 4;
then A12: x in dom (DataPart (NPP p)) by RELAT_1:90;
DataPart (NPP p) = DataPart (Relocated ((NPP p),k)) by Th115;
then DataPart (NPP p) c= NPP (Relocated (p,k)) by Lm169, XX;
then A13: DataPart (NPP p) c= s2 by A2, XBOOLE_1:1;
then dom (DataPart (NPP 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 (NPP p) c= NPP p by RELAT_1:88;
then A15: (DataPart (NPP p)) . x = (NPP p) . x by A12, GRFUNC_1:8;
A16: s2 . x = (DataPart s2) . x by A11, FUNCT_1:72;
(DataPart (NPP 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 (NPP p) c= dom s by A3, PARTFUN1:def 4;
hence NPP p c= s1 +* (DataPart s2) by A5, GRFUNC_1:8; :: thesis: verum