Proof of `Aperiodic Mealy machines are compositions of flip-flops`
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.
Description
An aperiodic Mealy function is a composition of flip-flops (the hard half of Theorem A.2.8): by Lemma A.2.11 some machine computing it satisfies the stabilisation condition (*), and the Krohn–Rhodes construction run for that machine only produces flip-flops (, from ).
Attribution
Theorem A.2.8 of Transducers, left-to-right; Lean proof by Aristotle ().