  Deciding termination is a fundamental problem in the analysis of
probabilistic imperative programs. We consider the qualitative and quantitative
probabilistic termination problems for an imperative programming model with
discrete probabilistic choice and demonic bounded nondeterminism. The
qualitative question asks if the program terminates almost-surely, no matter
how nondeterminism is resolved. The quantitative question asks for a bound on
the probability of termination. Despite a long and rich literature on the
topic, no sound and relatively complete proof systems were known for these
problems. In this paper, we provide such sound and relatively complete proof
rules for proving qualitative and quantitative termination in the assertion
language of arithmetic. Our rules use supermartingales as estimates of the
likelihood of a program's evolution and variants as measures of distances to
termination. Our key insight is our completeness result, which shows how to
construct a suitable supermartingales from an almost-surely terminating
program. We also show that proofs of termination in many existing proof systems
can be transformed to proofs in our system, pointing to its applicability in
practice. As an application of our proof rule, we show an explicit proof of
almost-sure termination for the two-dimensional random walker.
