let s1, s2 be State of SCMPDS; :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 & ProgramPart s1 = ProgramPart s2 implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: DataPart s1 = DataPart s2 and
A3: ProgramPart s1 = ProgramPart s2 ; :: thesis: s1 = s2
A4: dom s2 = ({(IC SCMPDS)} \/ SCM-Data-Loc) \/ NAT by SCMPDS_4:19;
A5: dom s1 = ({(IC SCMPDS)} \/ SCM-Data-Loc) \/ NAT by SCMPDS_4:19;
then s1 | {(IC SCMPDS)} = s2 | {(IC SCMPDS)} by A1, A4, GRFUNC_1:90;
then s1 | ({(IC SCMPDS)} \/ SCM-Data-Loc) = s2 | ({(IC SCMPDS)} \/ SCM-Data-Loc) by A2, RELAT_1:185, SCMPDS_2:100;
then s1 | (({(IC SCMPDS)} \/ SCM-Data-Loc) \/ NAT) = s2 | (({(IC SCMPDS)} \/ SCM-Data-Loc) \/ NAT) by A3, RELAT_1:185;
hence s1 = s2 | (dom s2) by A5, A4, RELAT_1:97
.= s2 by RELAT_1:97 ;
:: thesis: verum