Proof of `Aperiodicity as a pumping property`
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 28 of the paper of lax-157538, Transducers
Description
Aperiodicity of a Mealy function is the pumping property of Claim A.2.9. The source proves the pumping property from the stabilisation condition of Lemma A.2.11 () and the converse directly.
Attribution
Claim A.2.9 of Transducers; Lean proof by Aristotle ().