for s1, s2 being State of SCMPDS st s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) holds
s1 = s2