let s1, s2 be State of SCMPDS; :: thesis: ( s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) implies s1 = s2 )
set Y = NAT ;
set X = SCM-Data-Loc \/ {(IC )};
A1: ( s1 = s1 | ((Data-Locations ) \/ {(IC )}) & s2 = s2 | ((Data-Locations ) \/ {(IC )}) ) by MEMSTR_0:33;
thus ( s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) implies s1 = s2 ) by A1, SCMPDS_2:84; :: thesis: verum