let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for p being PartState of S st IC in dom p holds
NPP p = (Start-At ((IC p),S)) +* (DataPart p)
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for p being PartState of S st IC in dom p holds
NPP p = (Start-At ((IC p),S)) +* (DataPart p)
let p be PartState of S; :: thesis: ( IC in dom p implies NPP p = (Start-At ((IC p),S)) +* (DataPart p) )
assume A1: IC in dom p ; :: thesis: NPP p = (Start-At ((IC p),S)) +* (DataPart p)
A2: dom (DataPart p) misses dom (ProgramPart p) by Th15;
A3: dom (Start-At ((IC p),S)) misses dom (ProgramPart p) by Th130;
dom ((Start-At ((IC p),S)) +* (DataPart p)) = (dom (Start-At ((IC p),S))) \/ (dom (DataPart p)) by FUNCT_4:def 1;
then A4: dom ((Start-At ((IC p),S)) +* (DataPart p)) misses dom (ProgramPart p) by A2, A3, XBOOLE_1:70;
p = ((Start-At ((IC p),S)) +* (ProgramPart p)) +* (DataPart p) by A1, Th18
.= ((Start-At ((IC p),S)) +* (DataPart p)) +* (ProgramPart p) by A2, FUNCT_4:126 ;
hence NPP p = (((Start-At ((IC p),S)) +* (DataPart p)) +* (ProgramPart p)) \ (ProgramPart p)
.= (Start-At ((IC p),S)) +* (DataPart p) by A4, FUNCT_4:127 ;
:: thesis: verum