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