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
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 S in dom p holds
NPP p = (DataPart p) +* (Start-At (IC p),S)
let p be PartState of S; :: thesis: ( IC S in dom p implies NPP p = (DataPart p) +* (Start-At (IC p),S) )
A: dom (Start-At (IC p),S) = {(IC S)} by FUNCOP_1:19;
then M1: dom (DataPart p) misses dom (Start-At (IC p),S) by Th102;
M2: dom (Start-At (IC p),S) misses dom (ProgramPart p) by A, Th103;
M5: dom (DataPart p) misses dom (ProgramPart p) by Th104;
dom ((Start-At (IC p),S) +* (ProgramPart p)) = (dom (Start-At (IC p),S)) \/ (dom (ProgramPart p)) by FUNCT_4:def 1;
then M3: dom ((Start-At (IC p),S) +* (ProgramPart p)) misses dom (DataPart p) by M1, M5, XBOOLE_1:70;
X1: (DataPart p) +* (Start-At (IC p),S) = (DataPart p) \/ (Start-At (IC p),S) by FUNCT_4:32, M1;
assume IC S 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 Th108;
then B: p = ((Start-At (IC p),S) +* (ProgramPart p)) \/ (DataPart p) by M3, FUNCT_4:32
.= ((Start-At (IC p),S) \/ (ProgramPart p)) \/ (DataPart p) by M2, FUNCT_4:32
.= (ProgramPart p) \/ ((Start-At (IC p),S) \/ (DataPart p)) by XBOOLE_1:4 ;
C: Start-At (IC p),S misses ProgramPart p by M2, RELAT_1:214;
M5: dom (DataPart p) misses dom (ProgramPart p) by Th104;
DataPart p misses ProgramPart p by M5, RELAT_1:214;
then (Start-At (IC p),S) \/ (DataPart p) misses ProgramPart p by C, XBOOLE_1:70;
then p \ (ProgramPart p) = (Start-At (IC p),S) \/ (DataPart p) by B, XBOOLE_1:88;
hence NPP p = (DataPart p) +* (Start-At (IC p),S) by X1; :: thesis: verum