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