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

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