choiceb splits a nondeterministic choice a∪b between running a or b into its alternatives by reducing it to a conjunction [a]P ∧ [b]P that establishes the safety of a and of b separately.

Other tactics such as chase and unfold also use this axiom.