now :: thesis: for s being State of SCM+FSA
for o being Object of SCM+FSA
for I being Instruction of SCM+FSA st InsCode I = InsCode (halt SCM+FSA) & o in Data-Locations holds
(Exec (I,s)) . o = s . o

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 in Data-Locations 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 in Data-Locations holds
(Exec (I,s)) . o = s . o
let I be Instruction of SCM+FSA; :: thesis: ( InsCode I = InsCode (halt SCM+FSA) & o in Data-Locations implies (Exec (I,s)) . o = s . o )
assume that
A1: InsCode I = InsCode (halt SCM+FSA) and
o in Data-Locations ; :: thesis: (Exec (I,s)) . o = s . o
I = halt SCM+FSA by A1, SCMFSA_2:95;
hence (Exec (I,s)) . o = s . o by EXTPRO_1:def 3; :: thesis: verum

end;

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