finish the proof of astep_deterministic
finish the proof of bstep_deterministic
add/refine some comments