Refinement algebra provides axioms for the stepwise removal of abstraction, in the form of
demonic nondetermisn, in a first-order system that supports reasoning about loops. It has 
been extended by Solin and Meinicke to computations involving implicit probabilistic choices:
demonic nondeterminism then satisfied weaker properties. In this paper their axion system is
extended to capture explicit probabilistics choices. The first form is an unquantified 
probabilistic choice; the second is a partial quantified probabilistic choice (from which the
usual binary probabilistic choice can be recovered). The new refinement algebra is sound with
respect to 1-bounded expectation transformers, the premier model of probabilistic computations,
but also with respect to a new model introduced here to capture more directly partial quantified
computations. In this setting a 'normal form' result if Kozen is proved, replacing multiple loops 
with a single loop that does the same job; and the extent to which the two forms of loop
have the same expected number of steps to termination is considered. Being entirely within
first-order logic, the new refinement algebra is targetted to automation.