double rewriting for equivalential reasoning in acl2
Several users have had problems using equivalence-based rewriting in ACL2 because the ACL2 rewriter caches its results. We describe this problem in some detail, together with a partial solution first implemented in ACL2 Version 2.9.4. This partial solution consists of a new primitive, double--rewrite, together with a new warning to suggest possible use of this primitive.
rewriting formal methods equivalence relations congruences verification double-rewrite