` `

split the current goal into cases
Major Section: PROOF-CHECKER-COMMANDS

Example: splitFor 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: SPLITReplace 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.

**Remark:** 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`

.