A sound and complete axiomatization of the equational theory of Mealy machines.
Résumé
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.
