now

let s be State of SCM+FSA ; :: thesis: for o being Object of SCM+FSA
for I being Instruction of SCM+FSA st InsCode I = InsCode (halt SCM+FSA ) & o <> IC SCM+FSA holds
(Exec I,s) . o = s . o
let o be Object of SCM+FSA ; :: thesis: for I being Instruction of SCM+FSA st InsCode I = InsCode (halt SCM+FSA ) & o <> IC SCM+FSA holds
(Exec I,s) . o = s . o
let I be Instruction of SCM+FSA ; :: thesis: ( InsCode I = InsCode (halt SCM+FSA ) & o <> IC SCM+FSA implies (Exec I,s) . o = s . o )
assume that
A1: InsCode I = InsCode (halt SCM+FSA ) and
o <> IC SCM+FSA ; :: thesis: (Exec I,s) . o = s . o
I = halt SCM+FSA by A1, SCMFSA_2:122, SCMFSA_2:124;
hence (Exec I,s) . o = s . o by AMI_1:def 8; :: thesis: verum

end;

hence for b₁ being InsType of SCM+FSA st b₁ = InsCode (halt SCM+FSA ) holds
b₁ is jump-only by AMISTD_1:def 3; :: thesis: verum