`Simp` returns a list of simplified versions of its input
term, each paired with a hypothesis list under which the input and output
terms are provably equal.

This tool is implemented on top of another tool, `bash-term-to-dnf`.
However,

However, a case split may occur under simplification. Moroever,

(implies (and <simplified-hypothesis-1> ... <simplified-hypothesis-k>) <simplified-term>)

Example:

Suppose we have submitted the following two definitions.

(defun p (x) (or (stringp x) (acl2-numberp x))) (defun f (x) (if (p x) (cons x x) 17))

Then:

ACL2 !>(simp (f x) nil) (((CONS X X) (ACL2-NUMBERP X)) (17 (NOT (STRINGP X)) (NOT (ACL2-NUMBERP X))) ((CONS X X) (STRINGP X))) ACL2 !>(simp (f x) nil :hints (("Goal" :in-theory (disable p)))) ((17 (NOT (P X))) ((CONS X X) (P X))) ACL2 !>

Notice the space in front of the results. This indicates that what is actually returned is an error triple, for example as follows in the final case above.

(mv ((17 (NOT (P X))) ((CONS X X) (P X))) <state>)

General Form:

(simp term hypothesis-list :hints hints :verbose verbose)

where `defthm`, and a `(mv nil val state)`, where `val` is a list, each member of
which is of the form