let i be Instruction of SCMPDS ; :: thesis: for s1, s2 being State of SCMPDS st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds
( IC (Exec i,s1) = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )
let s1, s2 be State of SCMPDS ; :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 implies ( IC (Exec i,s1) = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) ) )
assume ( IC s1 = IC s2 & DataPart s1 = DataPart s2 ) ; :: thesis: ( IC (Exec i,s1) = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )
then s1,s2 equal_outside NAT by SCMPDS_6:4;
then Exec i,s1, Exec i,s2 equal_outside NAT by SCMPDS_4:15;
hence ( IC (Exec i,s1) = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) ) by SCMPDS_6:4; :: thesis: verum