let s1, s2 be State of SCMPDS ; :: thesis: for i being shiftable Instruction of SCMPDS st DataPart s1 = DataPart s2 holds
DataPart (Exec i,s1) = DataPart (Exec i,s2)
let i be shiftable Instruction of SCMPDS ; :: thesis: ( DataPart s1 = DataPart s2 implies DataPart (Exec i,s1) = DataPart (Exec i,s2) )
InsCode i <> 3 by SCMPDS_4:def 13;
hence ( DataPart s1 = DataPart s2 implies DataPart (Exec i,s1) = DataPart (Exec i,s2) ) by Th43; :: thesis: verum