Strategy Menu:

Cases Command

Use the Cases command if you want to do a proof by cases. If you select a given of the form P1∨P2∨...∨Pn and give the Cases command, then Proof Designer will break the proof into the cases P1, P2, ..., Pn. 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 P1∨P2∨...∨Pn 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. Too add or remove parentheses, use the Reexpress command.