ACL2-PC::SPLIT

(atomic macro) ` `split the current goal into cases
```Major Section:  PROOF-CHECKER-COMMANDS
```

```Example:
split
```
For example, if the current goal has one hypothesis `(or x y)` and a conclusion of `(and a b)`, then `split` will create four new goals:
```one with hypothesis X and conclusion A
one with hypothesis X and conclusion B
one with hypothesis Y and conclusion A
one with hypothesis Y and conclusion B.

General Form:
SPLIT
```
Replace the current goal by subgoals whose conjunction is equivalent (primarily by propositional reasoning) to the original goal, where each such goal cannot be similarly split.

Note: The new goals will all have their hypotheses promoted; in particular, no conclusion will have a top function symbol of `implies`. Also note that `split` will fail if there is exactly one new goal created and it is the same as the existing current goal.

The way `split` really works is to call the ACL2 theorem prover with only simplification (and preprocessing) turned on, and with only a few built-in functions (especially, propositional ones) enabled, namely, the ones in the list `(theory 'minimal-theory)`. However, because the prover is called, type-set reasoning can be used to eliminate some cases. For example, if `(true-listp x)` is in the hypotheses, then probably `(true-listp (cdr x))` will be reduced to `t`.