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, q being PartState of S holds dom (DataPart p) misses dom (ProgramPart q)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p, q being PartState of S holds dom (DataPart p) misses dom (ProgramPart q)
let p, q be PartState of S; :: thesis: dom (DataPart p) misses dom (ProgramPart q)
( the carrier of S \ ({(IC S)} \/ NAT) c= the carrier of S \ NAT & dom (DataPart p) c= the carrier of S \ ({(IC S)} \/ NAT) ) by RELAT_1:87, XBOOLE_1:7, XBOOLE_1:34;
then A1: dom (DataPart p) c= the carrier of S \ NAT by XBOOLE_1:1;
dom (ProgramPart q) c= NAT by RELAT_1:87;
hence dom (DataPart p) misses dom (ProgramPart q) by A1, XBOOLE_1:64, XBOOLE_1:79; :: thesis: verum