composeb splits the safety of a sequential composition a;b, which runs a followed by b, into successive safety properties [a][b]P. This shows after all runs of a it is the case that all runs of b are safe, so satisfy P.

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

See also