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