Integration of state machine graphical animation and Maude to facilitate characteristic conjecture: an approach to lemma discovery in theorem proving | Publicación