Use the Cases command if you want to do a proof
by cases. If you select a given of the form
*P*_{1}∨*P*_{2}∨…∨*P*_{n}
and give the Cases command, then Proof Designer will break the proof into the
cases *P*_{1}, *P*_{2},
…, *P*_{n}.
You can also break your proof into cases *P*
and ¬*P*, for any statement
*P*. To do this, select the goal you want to
prove by cases and give the Cases command. Proof Designer will ask you to type in
the statement *P* that you want to use to determine
the two cases.

If you are using a given of the form
*P*_{1}∨*P*_{2}∨…∨*P*_{n}
to determine the cases,
then parentheses in the given can affect what cases you get. For example,
if you select a given of the form
*P*∨*Q*∨*R* and give the
Cases command, then you will get the three cases *P*,
*Q*, and *R*.
But if your given has the form *P*∨(*Q*∨*R*), then you
will get only two cases: *P* and
*Q*∨*R*. Thus, you may want to add
or remove parentheses in your given before using the Cases command. To add or remove parentheses,
use the Reexpress command.