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
(theory 'minimal-theory)
), together with the names (or parenthesized
names) in the &rest
argument names
, are enabled.See also the documentation for s
.