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 in dom p holds
NPP p = (DataPart p) +* (Start-At ((IC p),S))
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 in dom p holds
NPP p = (DataPart p) +* (Start-At ((IC p),S))
let p be PartState of S; :: thesis: ( IC in dom p implies NPP p = (DataPart p) +* (Start-At ((IC p),S)) )
A1: dom (Start-At ((IC p),S)) = {(IC )} by FUNCOP_1:19;
then A2: dom (DataPart p) misses dom (Start-At ((IC p),S)) by Th11, ZFMISC_1:56;
A3: dom (Start-At ((IC p),S)) misses dom (ProgramPart p) by A1, Th12, ZFMISC_1:56;
A4: dom (DataPart p) misses dom (ProgramPart p) by Th15;
dom ((Start-At ((IC p),S)) +* (ProgramPart p)) = (dom (Start-At ((IC p),S))) \/ (dom (ProgramPart p)) by FUNCT_4:def 1;
then A5: dom ((Start-At ((IC p),S)) +* (ProgramPart p)) misses dom (DataPart p) by A2, A4, XBOOLE_1:70;
A6: (DataPart p) +* (Start-At ((IC p),S)) = (DataPart p) \/ (Start-At ((IC p),S)) by A2, FUNCT_4:32;
assume IC in dom p ; :: thesis: NPP p = (DataPart p) +* (Start-At ((IC p),S))
then p = ((Start-At ((IC p),S)) +* (ProgramPart p)) +* (DataPart p) by Th18;
then A7: p = ((Start-At ((IC p),S)) +* (ProgramPart p)) \/ (DataPart p) by A5, FUNCT_4:32
.= ((Start-At ((IC p),S)) \/ (ProgramPart p)) \/ (DataPart p) by A3, FUNCT_4:32
.= (ProgramPart p) \/ ((Start-At ((IC p),S)) \/ (DataPart p)) by XBOOLE_1:4 ;
A8: Start-At ((IC p),S) misses ProgramPart p by A3, RELAT_1:214;
A9: dom (DataPart p) misses dom (ProgramPart p) by Th15;
DataPart p misses ProgramPart p by A9, RELAT_1:214;
then (Start-At ((IC p),S)) \/ (DataPart p) misses ProgramPart p by A8, XBOOLE_1:70;
hence NPP p = (DataPart p) +* (Start-At ((IC p),S)) by A6, A7, XBOOLE_1:88; :: thesis: verum