Infer Menu:

Split Up Command

The Split Up command can only be used when you have a given of the form P↔Q or P1∧P2∧...∧Pn. If you select a given of the form P↔Q and give the Split Up command, then Proof Designer will infer P→Q and Q→P. If you select a given of the form P1∧P2∧...∧Pn and give the Split Up command, then Proof Designer will infer all of the statements P1, P2, ..., Pn.

Parentheses in your given can affect how the Split Up command works. For example, if you select a given of the form P∧Q∧R and give the Split Up command, then Proof Designer will infer P, Q, and R. But if the given is P∧(Q∧R), then Proof Designer will infer P and Q∧R. Thus, you may want to add or remove parentheses in your given before using the Split Up command. Too add or remove parentheses, use the Reexpress command.