Proof of `Decidable equivalence of Mealy machines`
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
In the paper
- page 14 of the paper of lax-157538, Transducers
Description
Two Mealy machines are equivalent if and only if they agree on all inputs of length at most the product of their numbers of states (Theorem A.1.2).
Proof strategy
The source theorem proves the finite check for state spaces and : a pair of runs of the two machines that repeats a pair of states can be shortened by cutting out the loop without removing a disagreement, so a shortest disagreeing input has length at most . The bridge moves between the concept machine and the source machine () and between and .
Attribution
Theorem A.1.2 of Transducers (M. Bojańczyk); the Lean proof is Aristotle's, in .