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 p being FinPartState of S
for k being Element of NAT holds NPP (Relocated (p,k)) = IncIC ((NPP p),k)
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 p being FinPartState of S
for k being Element of NAT holds NPP (Relocated (p,k)) = IncIC ((NPP p),k)
let p be FinPartState of S; :: thesis: for k being Element of NAT holds NPP (Relocated (p,k)) = IncIC ((NPP p),k)
let k be Element of NAT ; :: thesis: NPP (Relocated (p,k)) = IncIC ((NPP p),k)
A1: NAT misses the carrier of S \ NAT by XBOOLE_1:79;
A2: (Reloc ((ProgramPart p),k)) | ( the carrier of S \ NAT) = ((Reloc ((ProgramPart p),k)) | NAT) | ( the carrier of S \ NAT) by RELAT_1:209
.= {} by A1, RELAT_1:207 ;
A3: dom (IncIC ((NPP p),k)) c= the carrier of S by RELAT_1:def 18;
A4: the carrier of S \ NAT misses NAT by XBOOLE_1:79;
dom (NPP p) = dom (p | ( the carrier of S \ NAT)) by Th65
.= (dom p) /\ ( the carrier of S \ NAT) by RELAT_1:90 ;
then A5: dom (NPP p) misses NAT by A4, XBOOLE_1:74;
A6: dom (Start-At (((IC (NPP p)) + k),S)) misses NAT by Th26;
dom (IncIC ((NPP p),k)) = (dom (NPP p)) \/ (dom (Start-At (((IC (NPP p)) + k),S))) by FUNCT_4:def 1;
then dom (IncIC ((NPP p),k)) misses NAT by A5, A6, XBOOLE_1:70;
then A7: dom (IncIC ((NPP p),k)) c= the carrier of S \ NAT by A3, XBOOLE_1:86;
thus NPP (Relocated (p,k)) = NPP ((IncIC ((NPP p),k)) +* (Reloc ((ProgramPart p),k)))
.= ((IncIC ((NPP p),k)) +* (Reloc ((ProgramPart p),k))) | ( the carrier of S \ NAT) by Th65
.= ((IncIC ((NPP p),k)) | ( the carrier of S \ NAT)) +* {} by A2, FUNCT_4:75
.= (IncIC ((NPP p),k)) | ( the carrier of S \ NAT) by FUNCT_4:22
.= IncIC ((NPP p),k) by A7, RELAT_1:97 ; :: thesis: verum