` `

simplify the current subterm
Major Section: PROOF-CHECKER-COMMANDS

Examples: S -- simplify the current subterm (S :backchain-limit 2 :normalize t :expand (append x z)) -- simplify the current subterm, but during the rewriting process first ``normalize'' it by pushing IFs to the top-level, and also force the term (append x z) to be expanded during the rewriting process General Form: (s &key rewrite normalize backchain-limit repeat in-theory hands-off expand)Simplify the current subterm according to the keyword parameters supplied. First if-normalization is applied (unless the

`normalize`

argument is `nil`

), i.e., each subterm of the form
`(f ... (if test x y) ...)`

is replaced by the term
`(if test (f ... x ...) (f ... y ...))`

except, of course, when
`f`

is `if`

and the indicated `if`

subterm is in the second or
third argument position. Then rewriting is applied (unless the
rewrite argument is `nil`

). Finally this pair of actions is
repeated -- until the rewriting step causes no change in the term.
A description of each parameter follows.
:rewrite -- default tWhen non-

`nil`

, instructs the system to use ACL2's rewriter (or,
something close to it) during simplification.
:normalize -- default tWhen non-

`nil`

, instructs the system to use if-normalization (as
described above) during simplification.
:backchain-limit -- default 0Sets the number of recursive calls to the rewriter that are allowed for backchaining. Even with the default of 0, some reasoning is allowed (technically speaking, type-set reasoning is allowed) in the relieving of hypotheses. The value should be

`nil`

or a non-negative integer, and limits backchaining only
for rewriting, not for type-set reasoning.
:repeat -- default 0Sets the number of times the current term is to be rewritten. If this value is

`t`

, then the default is used (as specified by the
constant `*default-s-repeat-limit*`

).
:in-theory, :hands-off, :expandThese have their usual meaning; see hints.

**Remark:** if conditional rewrite rules are used that cause case splits
because of the use of `force`

, then appropriate new subgoals will be
created, i.e., with the same current subterm (and address) but with
each new (forced) hypothesis being negated and then used to create a
corresponding new subgoal. In that case, the current goal will have
all such new hypotheses added to the list of top-level hypotheses.