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)) )
NPP s1 = NPP s2 by A1, A2, SCMPDS_6:4;
then NPP (Exec (i,s1)) = NPP (Exec (i,s2)) 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