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 s being State of S holds (NPP s) | {(IC )} = s | {(IC )}
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S holds (NPP s) | {(IC )} = s | {(IC )}
let s be State of S; :: thesis: (NPP s) | {(IC )} = s | {(IC )}
A: {(IC )} c= (Data-Locations S) \/ {(IC )} by XBOOLE_1:7;
thus (NPP s) | {(IC )} = (s | ((Data-Locations S) \/ {(IC )})) | {(IC )} by LmAA
.= s | {(IC )} by A, RELAT_1:103 ; :: thesis: verum