thus not InsCode (f :=<0,...,0> a) is jump-only ; :: according to AMISTD_1:def 4 :: thesis: f :=<0,...,0> a is sequential
let s be State of SCM+FSA ; :: according to AMISTD_1:def 16 :: thesis: (Exec (f :=<0,...,0> a),s) . (IC SCM+FSA ) = succ (IC s)
thus (Exec (f :=<0,...,0> a),s) . (IC SCM+FSA ) = succ (IC s) by SCMFSA_2:101; :: thesis: verum