| | | B.3.1 scatter: Scatter Proof State |
scatter
: scatter
In proving mode.
This command generates one or more child states by applying the commands decompose and split. The application of scatter is recursively repeated for each child state until no more state is generated. If the initial applications of decompose and split do not generate new states, then scatter does not generate a child state.
For the recursive application of split being effective, scatter should be applied to a state with a single goal. The command then replaces the current state by a (potentially large) number of child states each of which has a number of (hopefully simple) assumptions and a single (hopefully simple) goal. Some of these states may have been already closed by a decision procedure; some others may be subsequently closed by the application of the autostar command.
It is advisable to apply decompose manually before scatter in order to get insight into the current proof state before attempting to scatter it.
The effect of this command may be simulated by repeated applications of the commands decompose and split.
| | | B.3.1 scatter: Scatter Proof State |