  RP-Rewriter (Retain-Property) is a verified clause processor that can use
some of the existing ACL2 rewrite rules to prove conjectures through term
rewriting. Optimized for conjectures that can expand into large terms, the
rewriter tries to mimic some of the ACL2 rewriting heuristics but also adds
some extra features. It can attach side-conditions to terms that help the
rewriter retain properties about them and prevent possibly some very expensive
backchaining. The rewriter supports user-defined complex meta rules that can
return a special structure to prevent redundant rewriting. Additionally, it can
store fast alists even when values are not quoted. RP-Rewriter is utilized for
two applications, multiplier design proofs and SVEX simplification, which
involve very large terms.
