ACL2-PC::S

(primitive) 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 t
When non-nil, instructs the system to use ACL2's rewriter (or, something close to it) during simplification. 
:normalize -- default t
When non-nil, instructs the system to use if-normalization (as described above) during simplification. 
:backchain-limit -- default 0
Sets 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 0
Sets 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, :expand
These 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.