Part D of the book Transducers (M. Bojańczyk) as concepts and proofs: the polyregular functions, the top of the transducer ladder, with their two machine models. The Lean development is Aristotle's formalisation of the book, re-presented in the archive's form; it requires the submissions for Parts A and C §1–3 (concepts) and for Part C §4 (proofs).

The definition-concepts are marked squaring, the polyregular functions as compositions of regular functions and marked squaring (D.0.1), for-transducers with their prenex form (D.1.2), pebble transducers, the string representation of pairs of pebble configurations with balanced runs, and the children of a configuration with the string representation of child configuration graphs.

The theorem-concepts are continuity of polyregular functions (D.0.2), the equivalence of for-transducers with polyregular functions (D.1.1, as two implications and their conjunction), the prenex normal form (D.1.3), closure of for-transducers under composition (D.1.4), continuity of pebble transducers (D.2.1), the regularity of reachability and of balanced reachability between configurations (D.2.2, D.2.3, stated as regular languages of encodings rather than as mso formulas), the equivalence of pebble transducers with for-transducers (D.2.4, split), and the three results on the children of a configuration (D.2.5–D.2.7). All are proved. The exercises are not part of this submission.