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