### ACL2-PC::S-PROP

(atomic macro)
` `

simplify propositionally
Major Section: PROOF-CHECKER-COMMANDS

Example:
s-prop
General Form:
(s-prop &rest names)

Simplify, using the default settings for `s`

(which include
if-normalization and rewriting without real backchaining), but with
respect to a theory in which only basic functions and rules (the
ones in `*s-prop-theory*`

), together with the names (or parenthesized
names) in the `&rest`

argument `names`

, are enabled.
See also the documentation for `s`

.