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 10;
hence ( DataPart s1 = DataPart s2 implies DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) ) by Th43; :: thesis: verum