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 st IC S in dom p holds
dom (NPP p) = {(IC S)} \/ (dom (DataPart p))
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S st IC S in dom p holds
dom (NPP p) = {(IC S)} \/ (dom (DataPart p))
let p be PartState of S; :: thesis: ( IC S in dom p implies dom (NPP p) = {(IC S)} \/ (dom (DataPart p)) )
A: dom (Start-At (IC p),S) = {(IC S)} by FUNCOP_1:19;
assume IC S in dom p ; :: thesis: dom (NPP p) = {(IC S)} \/ (dom (DataPart p))
then p = ((Start-At (IC p),S) +* (ProgramPart p)) +* (DataPart p) by Th108;
then B: dom p = (dom ((Start-At (IC p),S) +* (ProgramPart p))) \/ (dom (DataPart p)) by FUNCT_4:def 1
.= ({(IC S)} \/ (dom (ProgramPart p))) \/ (dom (DataPart p)) by A, FUNCT_4:def 1
.= (dom (ProgramPart p)) \/ ({(IC S)} \/ (dom (DataPart p))) by XBOOLE_1:4 ;
C: {(IC S)} misses dom (ProgramPart p) by Th103;
dom (DataPart p) misses dom (ProgramPart p) by Th104;
then {(IC S)} \/ (dom (DataPart p)) misses dom (ProgramPart p) by C, XBOOLE_1:70;
then (dom p) \ (dom (ProgramPart p)) = {(IC S)} \/ (dom (DataPart p)) by B, XBOOLE_1:88;
hence dom (NPP p) = {(IC S)} \/ (dom (DataPart p)) by RELAT_1:213; :: thesis: verum