Proof of `MSO transductions define regular functions`
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
A function defined by an mso transduction is regular (Theorem C.4.8, the hard implication): a two-way transducer walking the output order (, left to right).
Proof strategy
The source normalises the type of the transduction to (Lemma C.4.9, ), precomputes the answers of the universe, letter and order formulas by a letter-to-letter rational function (Lemma C.4.10, ), and builds a two-way transducer that visits the selected elements in the order of the order formula, reading the precomputed answers (, , ); the composition is regular by Theorem C.2.9. The concept's transduction is the source's through , with and transported (); regular functions come from Part C §1–3's bridge.
Attribution
Theorem C.4.8 of Transducers, Part C; formalised by Aristotle (Harmonic), , .