Double rewriting for equivalential reasoning in ACL2

Matt Kaufmann, J. Strother Moore. Double rewriting for equivalential reasoning in ACL2. In Panagiotis Manolios, Matthew Wilding, editors, Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006. pages 103-106, ACM, 2006. [doi]

@inproceedings{KaufmannM06,
  title = {Double rewriting for equivalential reasoning in ACL2},
  author = {Matt Kaufmann and J. Strother Moore},
  year = {2006},
  doi = {10.1145/1217975.1217997},
  url = {http://doi.acm.org/10.1145/1217975.1217997},
  tags = {graph-rewriting, rewriting},
  researchr = {https://researchr.org/publication/KaufmannM06},
  cites = {0},
  citedby = {0},
  pages = {103-106},
  booktitle = {Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006},
  editor = {Panagiotis Manolios and Matthew Wilding},
  publisher = {ACM},
  isbn = {0-9788493-0-2},
}