A sound and complete axiomatization of the equational theory of Mealy machines.
Pradic, Cécilia · HAL (Le Centre pour la Communication Scientifique Directe) · 2019
This small development in the Coq proof assistant introduces a term language and a basic equational theory for Mealy machines., i.e. finite-state letter-to-letter transducer. Soundness and completeness are proved for the equational theory.