Infer Menu:

Split Up Command

The Split Up command can only be used when you have a given of the form PQ or P1P2∧…∧Pn. If you select a given of the form PQ and give the Split Up command, then Proof Designer will infer PQ and QP. If you select a given of the form P1P2∧…∧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 PQR and give the Split Up command, then Proof Designer will infer P, Q, and R. But if the given is P∧(QR), then Proof Designer will infer P and QR. 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.