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