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