# The Old Decompose Proof Command

This command has been replaced with a new version.

The Decompose Proof command is executed by placing the cursor in a proof obligation, either a proof step or a theorem, and either typing `Ctl+G Ctl+D` or right-clicking and selecting the command.

There are two basic ways to decompose a proof obligation into simpler obligtions:

`/\` decomposition
  If `P` equals `P1 /\ ... /\ Pn` , then the proof of `P` can be broken into the proof of the `n` formulas `P1, ... , Pn` .
`\/` decomposition (case split)
  If `P` equals `P1 \/ ... \/ Pn` , then the proof of `ASSUME P PROVE Q` can be broken into the proof of the `n` obligations `ASSUME P1 PROVE Q, ..., ASSUME Pn PROVE Q` .

Often, a proof obligation must be transformed into an equivalent one in order to be decomposed by `/\` or `\/` decomposition. There are two transformations that can be applied to the goal of an obligation. (The goal is the `PROVE` formula of an `ASSUME`/`PROVE` obligation or the entire obligation, if it is a single formula.)

`=>` splitting
  A goal `P => Q` is equivalent to the assumption `P` and the goal `Q` .
`\A` splitting
  A goal `\A x \in S : P` is equivalent to the assumption `NEW x \in S` and the goal `P` . The goal `\A x : P` is similarly split.

There are two transformations that can be applied to an assumption of an `ASSUME`/`PROVE` obligation:

`/\` splitting
  An assumption `P1 /\ ... /\ Pn` , is equivalent to the `n` assumptions P1, ..., Pn .
`\E` splitting
  An assumption `\E x \in S : P` is equivalent to the two assumptions `NEW x \in S, P` . The goal `\E x : P` is similarly split.

These splittings are effected by clicking on the appropriately labeled buttons. (`\/` and `\E` splittings can be combined hierarchically.)

The proof is generated by clicking a button that is either labeled by P or (for an `/\` decomposition) by a button with P next to it.

Instead of generating an `/\` or `\/` decomposition, the button labeled P at the top of the command's dialog window generates a proof consisting of only a `SUFFICES ASSUME ... PROVE` step constructed by splitting the original obligation and a `QED` step. For example, starting from the obligation `P => \E x \in S : Q`, performing a `=>` split followed by a `\A` split on the goal and then clicking on this button produces a proof like this:

       <3> SUFFICES ASSUME P, NEW x \in S
                    PROVE  Q
         OBVIOUS
       <3> QED

The obligation to which you apply the Decompose Proof command must have either no proof or else a leaf proof, such as a `BY` proof or the proof `OBVIOUS`). If it has a leaf proof, that proof is made the proof of each of the simpler obligations into which the proof is decomposed. For a proof generated by the top P button (which does no decomposing), the obligation's leaf proof becomes the `QED` step's proof.

## Options

There are two options that you can select.

Use `SUFFICES`
  Splitting the goal or a `\E` assumption generates new assumptions. Selecting this option causes those assumptions to be asserted by a `SUFFICES ASSUME/PROVE` step. Otherwise, these assumption are added to each of the decomposed proof steps.
Use `CASE`
  This selection determines whether, in the created substeps of the proof of an `\/` decomposition, `CASE` steps should be used instead of `ASSUME/PROVE` steps when possible. One reason not to choose this option is that the Decompose Command does not decompose `CASE` steps.

## Limitations

The following are the known problems and limitations of the command.

- The command will not expand definitions that come from a different module.
- Decomposing a proof step may require renaming of bound identifiers to avoid name clashes. This renaming is not done for clashes with names defined by `LET` definitions within the step. This can cause parsing errors in the decomposed proof.

↑ Viewing and Editing Structured Proofs