let t be State of SCMPDS ; :: thesis: for i being Instruction of SCMPDS st InsCode i in {0 ,4,5,6} holds
Dstate t = Dstate (Exec i,t)
let i be Instruction of SCMPDS ; :: thesis: ( InsCode i in {0 ,4,5,6} implies Dstate t = Dstate (Exec i,t) )
assume InsCode i in {0 ,4,5,6} ; :: thesis: Dstate t = Dstate (Exec i,t)
then DataPart (Exec i,t) = DataPart t by SCMPDS_7:20;
hence Dstate t = Dstate (Exec i,t) by Th2; :: thesis: verum