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.