Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `Myhill–Nerode for Mealy machines`

groundedproofs/Lax765601Proofs/Results.lean · lax-765601

What this proof establishes

no assumptions

thm✓Lax765601.MealyDerivatives

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

Description

The Myhill–Nerode lemma for Mealy machines (Lemma A.2.10). From a machine, the derivative after ww is the run from the state reached after ww; conversely the source builds the minimal machine Transducers.derivMealyTransducers.derivMealy on the finitely many derivatives, its transition from f(w)f(w_) on aa outputting the first letter of f(w)(a)f(w_)(a) and moving to f(wa)f(wa_).

Attribution

Lemma A.2.10 of Transducers; Lean proof by Aristotle (Transducers.myhillnerodemealyTransducers.myhill_nerode_mealy).