let s be State of SCMPDS; for i being Instruction of SCMPDS st InsCode i in {0,4,5,6,14} holds
DataPart (Exec (i,s)) = DataPart s
let i be Instruction of SCMPDS; ( InsCode i in {0,4,5,6,14} implies DataPart (Exec (i,s)) = DataPart s )
assume A1:
InsCode i in {0,4,5,6,14}
; DataPart (Exec (i,s)) = DataPart s
hence
DataPart (Exec (i,s)) = DataPart s
by SCMPDS_4:8; verum