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