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 ; :: according to AMISTD_1:def 16 :: thesis: (Exec (SubFrom a,b),s) . (IC SCM ) = NextLoc (IC s)
Next = NextLoc (IC s) by Th56;
hence (Exec (SubFrom a,b),s) . (IC SCM ) = NextLoc (IC s) by AMI_3:10; :: thesis: verum