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