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
now :: thesis: for a being Int_position holds (Exec (i,s)) . a = s . a
let a be Int_position; :: thesis: (Exec (i,s)) . b1 = s . b1
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;
suppose InsCode i = 0 ; :: thesis: (Exec (i,s)) . b1 = s . b1
hence (Exec (i,s)) . a = s . a by SCMPDS_2:86; :: thesis: verum
end;
suppose InsCode i = 14 ; :: thesis: (Exec (i,s)) . b1 = s . b1
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;
suppose InsCode i = 4 ; :: thesis: (Exec (i,s)) . b1 = s . b1
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;
suppose InsCode i = 5 ; :: thesis: (Exec (i,s)) . b1 = s . b1
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;
suppose InsCode i = 6 ; :: thesis: (Exec (i,s)) . b1 = s . b1
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;
end;
end;
hence DataPart (Exec (i,s)) = DataPart s by SCMPDS_4:8; :: thesis: verum