| | | B.3.2 decompose: Decompose Formulas |
decompose
In proving mode.
: decompose
The command generates a single child state by repeatedly applying the command flatten, the command skolemize, and a simplification procedure, until the resulting proof state does not change any more. If the resulting state equals the current state, no child state is generated.
The command generates at most one child state. This state can be considered as a simplified version of the current state and thus may be inspected to get further insight, e.g. to determine why a proof does not work or to find another proving strategy. An application of the command can be considered as safe in the sense that it does (should?) never complicate the proof.
This command is used by the command scatter (which may generate multiple child states).
The effect of this command may be simulated by repeated applications of the commands flatten and skolemize.
| | | B.3.2 decompose: Decompose Formulas |