let s be State of SCM+FSA ; :: thesis: for i being Instruction of SCM+FSA st InsCode i in {0 ,6,7,8} holds
DataPart (Exec i,s) = DataPart s
let i be Instruction of SCM+FSA ; :: thesis: ( InsCode i in {0 ,6,7,8} implies DataPart (Exec i,s) = DataPart s )
assume A1: InsCode i in {0 ,6,7,8} ; :: thesis: DataPart (Exec i,s) = DataPart s

now

let a be Int-Location ; :: thesis: for f being FinSeq-Location holds
( (Exec i,s) . b₂ = s . b₂ & (Exec i,s) . b₃ = s . b₃ )
let f be FinSeq-Location ; :: thesis: ( (Exec i,s) . b₁ = s . b₁ & (Exec i,s) . b₂ = s . b₂ )

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

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

then i = halt SCM+FSA by SCMFSA_2:122;
hence ( (Exec i,s) . a = s . a & (Exec i,s) . f = s . f ) by AMI_1:def 8; :: thesis: verum

end;

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

then consider lb being Instruction-Location of SCM+FSA such that
A2: i = goto lb by SCMFSA_2:59;
thus ( (Exec i,s) . a = s . a & (Exec i,s) . f = s . f ) by A2, SCMFSA_2:95; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: ( (Exec i,s) . b₁ = s . b₁ & (Exec i,s) . b₂ = s . b₂ )

then consider lb being Instruction-Location of SCM+FSA , b being Int-Location such that
A3: i = b =0_goto lb by SCMFSA_2:60;
thus ( (Exec i,s) . a = s . a & (Exec i,s) . f = s . f ) by A3, SCMFSA_2:96; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: ( (Exec i,s) . b₁ = s . b₁ & (Exec i,s) . b₂ = s . b₂ )

then consider lb being Instruction-Location of SCM+FSA , b being Int-Location such that
A4: i = b >0_goto lb by SCMFSA_2:61;
thus ( (Exec i,s) . a = s . a & (Exec i,s) . f = s . f ) by A4, SCMFSA_2:97; :: thesis: verum

end;

end;

end;

hence DataPart (Exec i,s) = DataPart s by SCMFSA6A:38; :: thesis: verum