Every Mealy machine $f$ admits a decomposition

in which each Mealy machine $f_1, \ldots, f_n$ is either reversible or flip-flop (Theorem A.2.2 of Transducers, the Krohn–Rhodes theorem). No uniqueness is claimed. Since Mealy machines are closed under composition, the class of functions computed by Mealy machines is exactly the closure under composition of the prime Mealy machines,

The proof of the book has two steps: map lifting is compatible with decompositions into primes (Lemma A.2.4), and the state transformation transducer of every pre-automaton is a composition of primes (Lemma A.2.5), by an induction on the number of states and the number of letters whose state transformation is not a permutation; the output of the machine is then recovered from the state transformations of the prefixes by a delay machine and a letter-to-letter homomorphism.

If a Mealy machine decomposes into prime Mealy machines, then so does its map lifting (Lemma A.2.4 of Transducers). Since map lifting commutes with composition, it suffices to lift a single prime. A flip-flop is lifted by resetting its state at every separator. A reversible machine needs more care, because resetting would break reversibility: the book computes, by a reversible machine, the state transformation $\gamma_w$ of every prefix in the variant where the separator does nothing, stores the value at the last separator by a flip-flop delay machine, and recovers the state transformation of the current block by the cancellation law $\delta_w = \gamma_v^{-1} \cdot \gamma_{vw}$, all of which is a one-state machine's work.

For every pre-automaton, its state transformation transducer — the Mealy machine whose $n$-th output letter is the state transformation of the first $n$ input letters — is a composition of prime Mealy machines (Lemma A.2.5 of Transducers, the main lemma in the proof of the Krohn–Rhodes theorem).

The book proves it by induction on the number of states and, for a tie, on the number of letters whose state transformation is not a permutation. A pre-automaton all of whose letters are permutations is reversible as it stands. Otherwise one fixes a letter $a$ whose state transformation has a proper image $P \subset Q$, decomposes the input into its first $a$-block, the middle $a$-blocks and the $a$-free suffix, and computes the three state transformations in five stages: the map lifting of the induction hypothesis for the alphabet without $a$ (Lemma A.2.4) handles the $a$-free pieces, two flip-flops distribute the state transformations of the blocks, the induction hypothesis for the smaller state space $P$ handles the middle part, and a letter-to-letter homomorphism assembles the result.

The composition of two functions computed by reversible Mealy machines is computed by a reversible Mealy machine (Lemma A.2.6 of Transducers). Hence the class $(\mathrm{Reversible})^*$ of compositions of reversible machines is just the class of reversible machines: the product machine of the composition (Theorem A.1.3) is reversible, since the state transformation of a letter in it is a permutation in each coordinate.

A function computed by a Mealy machine is aperiodic if and only if it is computed by a composition of flip-flop Mealy machines (Theorem A.2.8 of Transducers). This answers the question what the class $(\mathrm{Flip\text{-}flop})^*$ of compositions of one kind of prime is; for the other kind, $(\mathrm{Reversible})^*$ is the class of reversible machines (Lemma A.2.6).

The two implications are separate results, each with its own proof: $AperiodicOfFlipFlops$ (a composition of flip-flops is aperiodic) and $FlipFlopsOfAperiodic$ (an aperiodic Mealy function decomposes into flip-flops); this statement is their conjunction.

Every aperiodic function computed by a Mealy machine is computed by a composition of flip-flop Mealy machines: the implication "aperiodic $\Rightarrow$ composition of flip-flops" of Theorem A.2.8 of Transducers, the hard half. By Lemma A.2.11 the function is computed by a machine whose state transformations satisfy the stabilisation condition (); the proof of the Krohn–Rhodes theorem is then run for this machine, and every machine arising in the induction inherits (), since it only uses state transformations of the original one, so that no reversible machine with more than one state ever appears and every prime in the decomposition is a flip-flop.

Every composition of flip-flop Mealy machines computes an aperiodic function: the implication "composition of flip-flops $\Rightarrow$ aperiodic" of Theorem A.2.8 of Transducers. A single flip-flop is aperiodic, because the last letter of $f(u v^n w)$ depends only on the last letter read and on the last letter of $u v w$ whose state transformation is a constant, neither of which depends on $n$; and aperiodicity is preserved by composition, by the pumping form of aperiodicity (Claim A.2.9), in which the shifts $k$ of the two functions add up.

A function $f$ computed by a Mealy machine is aperiodic if and only if for all input strings $u, v, w$ there are output strings $x, y, z$ and a number $k$ such that

(Claim A.2.9 of Transducers). The right-to-left direction is immediate, since the last letter of $x y^n z$ does not depend on $n$. For the other direction, aperiodicity fixes the last $|v|$ letters of $f(u v^n)$ for large $n$, so that from some point on the output ends with repetitions of a fixed string $y$ of length $|v|$, and fixes the last $|w|$ letters of $f(u v^n w)$, which gives $z$. The pumping form is what makes aperiodicity compatible with composition: the shift $k$ of $f \cdot g$ is the sum of the shifts of $f$ and $g$.

A string-to-string function is computed by a Mealy machine if and only if (1) it has finitely many derivatives, (2) it is letter-to-letter, and (3) its $n$-th output letter depends only on the first $n$ input letters (Lemma A.2.10 of Transducers). From a machine, the derivative $f(w\_)$ is determined by the state reached after reading $w$, so there are finitely many. Conversely, the minimal machine of $f$ has the derivatives as its states, the derivative of the empty string as initial state, and the transitions

which are well defined because the output letter and the target depend only on the derivative $f(w\_)$ and not on $w$.

A function computed by a Mealy machine is aperiodic if and only if its minimal Mealy machine satisfies the stabilisation condition (): for every state transformation $\delta : Q \to Q$ that arises from some input string, the sequence $\delta^1, \delta^2, \ldots$ eventually stabilises on a single state transformation (Lemma A.2.11 of Transducers). If any machine computing $f$ satisfies (), then $f$ is aperiodic; conversely, if the minimal machine violates (*) for the state transformation of a string $v$, then two powers $\delta^i \neq \delta^j$ recur infinitely often, and minimality yields strings $u, w$ for which the last letters of $f(u v^i w)$ and $f(u v^j w)$ differ, contradicting aperiodicity. This lemma is what the book's decision procedure for aperiodicity rests on.

The equivalence problem for Mealy machines — do two given machines compute the same function? — is decidable (Theorem A.1.2 of Transducers). The book reduces it to the equivalence of regular languages: a letter-to-letter function is determined by the languages "the last output letter is $b$", one for each output letter $b$, and each of them is recognised by the automaton underlying the machine. In the form stated here, two Mealy machines with $n_1$ and $n_2$ states are equivalent if and only if they agree on all input strings of length at most $n_1 n_2$ — a finite check, since the alphabet is finite.

If $f : A^* \to B^*$ and $g : B^* \to C^*$ are computed by Mealy machines, then so is their composition $A^* \xrightarrow{f} B^* \xrightarrow{g} C^*$ (Theorem A.1.3 of Transducers). The proof is a product construction: the composed machine runs both machines in lockstep, feeding each output letter of the first to the second, so its state space is the product of the two state spaces.

Every function computed by a Mealy machine is continuous: the inverse image of a regular language under it is regular (Theorem A.1.4 of Transducers). The book derives this from closure under composition through the letter-to-letter lifting of a language, which labels every position of a string by whether the prefix ending there belongs to the language; a direct product construction works just as well, and is the one formalised.

A function $f : A^* \to B^*$ is computed by a Mealy machine if and only if it is (a) continuous, (b) prefix preserving, and (c) length preserving (Theorem B.4.1 of Transducers). A Mealy machine clearly has the three properties; conversely, for every output letter $b$ the language of inputs whose output ends with $b$ is regular by continuity, each input position contributes exactly one output letter by prefix and length preservation, and the product of the automata of these languages is the state space of a Mealy machine computing $f$.

One can decide whether a given rational function is computed by a Mealy machine (Theorem B.4.2 of Transducers). By Theorem B.4.1 it suffices to check the three properties of a Mealy function: continuity is automatic for a rational function, length preservation is decided by Lemma B.4.3, and after Lemma B.4.5 has put the automaton in a form where every transition reads and writes one letter, prefix preservation fails exactly when two transitions with the same input letter and different output letters start in states reachable by a common input string.

One can decide whether a given rational function is length preserving (Lemma B.4.3 of Transducers). The book's direct argument computes the unique candidate typing $\tau : Q \to \mathbb{Z}$ of the automaton — the difference between output and input length of the runs reaching each state — and checks that every transition respects it and that accepting states have type zero (Claim B.4.4).

Fix an automaton with output computing a function $f$, all of whose states are productive. A typing is a function $\tau : Q \to \mathbb{Z}$ such that every run from an initial state to a state $q$ satisfies

The function $f$ is length preserving if and only if a typing exists and maps every accepting state to zero (Claim B.4.4 of Transducers). If no typing exists, two runs reach the same state with different length differences and the function cannot be length preserving; if a typing exists but some accepting state has nonzero type, a run reaching it witnesses the same.

If a rational function is length preserving, then it is computed by an automaton with output in which the input and the output string of every transition have the same length (Lemma B.4.5 of Transducers). The book's proof takes the typing of Claim B.4.4 and works in the free group over the output alphabet: the new states are pairs $(q, x)$ of a state and a reduced string $x$ of length $\tau(q)$, possibly negative, and a transition $q \xrightarrow{w / x^{-1} v y} p$ of the original automaton becomes the transition $(q, x) \xrightarrow{w / v} (p, y)$, whose lengths agree.

A function $f : A^* \to B^*$ is sequential if and only if it (a) is continuous, (b) is prefix preserving, (c) outputs $\varepsilon$ on the input $\varepsilon$, and (d) has the bounded increase property: the increase of output length caused by extending the input by one letter,

is finite (Theorem B.4.6 of Transducers, Ginsburg and Rose). The derivative $wa \mapsto f(w)^{-1} f(wa)$, well defined by prefix preservation and of finite image by bounded increase, is shown to be computed by a finite automaton — its length by continuity modulo a large enough number, and then its value by continuity again.

A partial function $f : A^* \to B^*$ is subsequential if and only if it is continuous and has bounded variation: for all $w_1, w_2$,

$w$ ranging over the strings for which both values are defined (Theorem B.4.8 of Transducers, Choffrut). The construction of the transducer splits the output after a prefix into a branching part, which depends on the future, and a non-branching part, both of which are shown regular; the book's Claims B.4.9–B.4.12 are the steps of that construction.

A function $f : A^* \to B^*$ is rational if and only if it is continuous and the equivalence relation

on input strings has finite index (Theorem B.4.13 of Transducers, Reutenauer and Schützenberger). For a rational function computed by a bimachine, two strings with the same state of the suffix automaton are equivalent, so the index is finite; conversely the finitely many classes are used as the states of a suffix automaton, and the output after a prefix is computed by a subsequential transducer for each class. String reversal is not rational: all its input strings are pairwise inequivalent.

For a string-to-string function the following are equivalent (Theorem B.2.3 of Transducers, Eilenberg): (1) it is a rational relation which happens to be functional; (2) it is computed by an unambiguous nondeterministic automaton with output; (3) it is computed by a bimachine. The book proves (3) ⇒ (1) ⇒ (2) ⇒ (3); here the three implications with content are separate statements — $RationalOfBimachine$, $UnambiguousOfRational$ and $BimachineOfRational$ — and this statement is their conjunction, the implication (2) ⇒ (1) being immediate since an unambiguous automaton is an automaton.