thus not InsCode (a := b) is jump-only ; :: according to AMISTD_1:def 4 :: thesis: a := b is sequential
let s be State of SCM ; :: according to AMISTD_1:def 16 :: thesis: (Exec (a := b),s) . (IC SCM ) = NextLoc (IC s),SCM
succ (IC s) = NextLoc (IC s),SCM by Th56;
hence (Exec (a := b),s) . (IC SCM ) = NextLoc (IC s),SCM by AMI_3:8; :: thesis: verum