Proof of `The state transformation transducer is a composition of primes`
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
The state transformation transducer of a pre-automaton is a composition of primes (Lemma A.2.5): the induction of the book on the number of states and, for a tie, on the number of letters whose state transformation is not a permutation, with the tripartite decomposition of the input into the first -block, the middle blocks and the -free suffix.
Attribution
Lemma A.2.5 of Transducers; Lean proof by Aristotle (, ).