John R. Cowles, Ruben Gamboa. Unique factorization in ACL2: Euclidean domains. 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 21-27, ACM, 2006. [doi]
Abstract is missing.