let s be State of SCMPDS; :: thesis: 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; :: thesis: ( 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} ; :: thesis: DataPart (Exec (i,s)) = DataPart s

DataPart (Exec (i,s)) = DataPart s

let i be Instruction of SCMPDS; :: thesis: ( 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} ; :: thesis: DataPart (Exec (i,s)) = DataPart s

now :: thesis: for a being Int_position holds (Exec (i,s)) . a = s . a

hence
DataPart (Exec (i,s)) = DataPart s
by SCMPDS_4:8; :: thesis: verumlet a be Int_position; :: thesis: (Exec (i,s)) . b_{1} = s . b_{1}

end;per cases
( InsCode i = 0 or InsCode i = 14 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 )
by A1, ENUMSET1:def 3;

end;

suppose
InsCode i = 14
; :: thesis: (Exec (i,s)) . b_{1} = s . b_{1}

then
ex k1 being Integer st i = goto k1
by SCMPDS_2:26;

hence (Exec (i,s)) . a = s . a by SCMPDS_2:54; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by SCMPDS_2:54; :: thesis: verum

suppose
InsCode i = 4
; :: thesis: (Exec (i,s)) . b_{1} = s . b_{1}

then
ex b being Int_position ex k1, k2 being Integer st i = (b,k1) <>0_goto k2
by SCMPDS_2:30;

hence (Exec (i,s)) . a = s . a by SCMPDS_2:55; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by SCMPDS_2:55; :: thesis: verum

suppose
InsCode i = 5
; :: thesis: (Exec (i,s)) . b_{1} = s . b_{1}

then
ex b being Int_position ex k1, k2 being Integer st i = (b,k1) <=0_goto k2
by SCMPDS_2:31;

hence (Exec (i,s)) . a = s . a by SCMPDS_2:56; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by SCMPDS_2:56; :: thesis: verum

suppose
InsCode i = 6
; :: thesis: (Exec (i,s)) . b_{1} = s . b_{1}

then
ex b being Int_position ex k1, k2 being Integer st i = (b,k1) >=0_goto k2
by SCMPDS_2:32;

hence (Exec (i,s)) . a = s . a by SCMPDS_2:57; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by SCMPDS_2:57; :: thesis: verum