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

now

let a be Int_position ; :: thesis: (Exec (i,s)) . b₁ = s . b₁

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

suppose InsCode i = 0 ; :: thesis: (Exec (i,s)) . b₁ = s . b₁

then ex k1 being Integer st i = goto k1 by SCMPDS_2:35;
hence (Exec (i,s)) . a = s . a by SCMPDS_2:66; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: (Exec (i,s)) . b₁ = s . b₁

then ex b being Int_position ex k1, k2 being Integer st i = (b,k1) <>0_goto k2 by SCMPDS_2:39;
hence (Exec (i,s)) . a = s . a by SCMPDS_2:67; :: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: (Exec (i,s)) . b₁ = s . b₁

then ex b being Int_position ex k1, k2 being Integer st i = (b,k1) <=0_goto k2 by SCMPDS_2:40;
hence (Exec (i,s)) . a = s . a by SCMPDS_2:68; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: (Exec (i,s)) . b₁ = s . b₁

then ex b being Int_position ex k1, k2 being Integer st i = (b,k1) >=0_goto k2 by SCMPDS_2:41;
hence (Exec (i,s)) . a = s . a by SCMPDS_2:69; :: thesis: verum

end;

end;

end;

hence DataPart (Exec (i,s)) = DataPart s by SCMPDS_4:23; :: thesis: verum