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 :: thesis: for a being Int-Location
for f being FinSeq-Location holds
( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f )

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:95;
hence ( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f ) by EXTPRO_1:def 3; :: thesis: verum

end;

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

then ex lb being Nat st i = goto lb by SCMFSA_2:35;
hence ( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f ) by SCMFSA_2:69; :: thesis: verum

end;

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

then ex lb being Nat ex b being Int-Location st i = b =0_goto lb by SCMFSA_2:36;
hence ( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f ) by SCMFSA_2:70; :: thesis: verum

end;

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

then ex lb being Nat ex b being Int-Location st i = b >0_goto lb by SCMFSA_2:37;
hence ( (Exec (i,s)) . a = s . a & (Exec (i,s)) . f = s . f ) by SCMFSA_2:71; :: thesis: verum

end;

end;

end;

hence DataPart (Exec (i,s)) = DataPart s by SCMFSA_M:2; :: thesis: verum