...invariant

A1 is valid initially, and for every rule R with guard G and action S, $\{A1 \wedge G\} \:S\: \{A1\}$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.