now

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

end;

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