Modelling algebraic structures and morphisms in ACL2 | Publicación