A dually nondeterministic refinement algebra with a negation operator is proposed. The algebra facilitates reasoning about
total-correctness preserving program transformations and nondeterministic programs. The negation operator is used to express
enabledness and termination operators through a useful explicit definition. As a small application, a property of action systems
is proved employing the algebra. A dually nondeterministic refinement algebra without the negation operator is also discussed.