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