Proof of `Every streaming string transducer computes a regular function`
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
Every streaming string transducer computes a regular function (Theorem C.3.2, from sst to regular): the sst is normalised and simulated by a two-way transducer expanding the final output depth-first (, ), and two-way transducers compute regular functions (Theorem C.2.9); , left to right.
Attribution
Theorem C.3.2 of Transducers, Part C; formalised by Aristotle (Harmonic).