let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds DataPart p = DataPart (NPP p)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S holds DataPart p = DataPart (NPP p)
let p be PartState of S; :: thesis: DataPart p = DataPart (NPP p)
X: Data-Locations S = ( the carrier of S \ {(IC S)}) \ NAT by XBOOLE_1:41;
( the carrier of S \ NAT) /\ (Data-Locations S) = ( the carrier of S /\ (Data-Locations S)) \ NAT by XBOOLE_1:49
.= (Data-Locations S) \ NAT by XBOOLE_1:28
.= ( the carrier of S \ {(IC S)}) \ (NAT \/ NAT) by X, XBOOLE_1:41
.= Data-Locations S by X ;
hence DataPart p = p | (( the carrier of S \ NAT) /\ (Data-Locations S))
.= (p | ( the carrier of S \ NAT)) | (Data-Locations S) by RELAT_1:100
.= (NPP p) | (Data-Locations S) by Th65
.= DataPart (NPP p) ;
:: thesis: verum