Proof of `Aperiodicity through the state transformations of the minimal machine`
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 29 of the paper of lax-157538, Transducers
Description
A Mealy function is aperiodic if and only if some machine computing it satisfies the stabilisation condition () (Lemma A.2.11). The source constructs the minimal machine on the derivatives and shows that aperiodicity makes its state transformations stabilise; conversely () gives the pumping property.
Attribution
Lemma A.2.11 of Transducers; Lean proof by Aristotle ().