If you know that A and B are true, then you know, by the and truth
table, that both A and B are true too.
and elimination exploits this property by allowing you to conclude either
A is true or B is true if you know that A and B is true.
For a co statement, you know that the precondition
{ P1 and P2 and ... and Pn }
is true at the time statement Si begins execution. You can use
and elimination to get rid of all the predicates Sj,
j != i (as a tactical matter, however, you may want to keep a few of
the other predicates in Si's precondition, particularly if you
anticipate the need to weaken Si's precondition to avoid
interference).
This page last modified on 11 June 2003.