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

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