let s1, s2 be State of SCMPDS; :: thesis: ( ( for a being Int_position holds s1 . a = s2 . a ) implies Initialize s1 = Initialize s2 )

assume for a being Int_position holds s1 . a = s2 . a ; :: thesis: Initialize s1 = Initialize s2

then DataPart s1 = DataPart s2 by SCMPDS_4:8;

hence Initialize s1 = Initialize s2 by MEMSTR_0:80; :: thesis: verum

assume for a being Int_position holds s1 . a = s2 . a ; :: thesis: Initialize s1 = Initialize s2

then DataPart s1 = DataPart s2 by SCMPDS_4:8;

hence Initialize s1 = Initialize s2 by MEMSTR_0:80; :: thesis: verum