` `

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.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.General Form: 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 `*s-prop-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`

.