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 that
A1: IC s1 = IC s2 and
A2: DataPart s1 = DataPart s2 ; :: thesis: ( IC (Exec i,s1) = IC (Exec i,s2) & DataPart (Exec i,s1) = DataPart (Exec i,s2) )
s1,s2 equal_outside NAT by A1, A2, 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