Formal Reasoning about Efficient Data Structures: A Case Study in ACL2 | Publicación