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
a
and implies the safety of b
.
MR better separates proofs but requires an intermediate condition transporting all required knowledge through a
to b
.