Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `Every regular function is computed by a streaming string transducer`

groundedproofs/Lax916827Proofs/Results.lean · lax-916827

What this proof establishes

no assumptions

thm✓Lax916827.SSTOfRegular

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Every regular function is computed by a streaming string transducer (Theorem C.3.2, from regular to sst): ssts are closed under post-composition with every prime regular function (Transducers.sstiffregularTransducers.sst_iff_regular, right to left, PartC/SSTRegular.leanPartC/SSTRegular.lean, PartC/SSTMealy∗.leanPartC/SSTMealy*.lean, PartC/SSTMap∗.leanPartC/SSTMap*.lean).

Attribution

Theorem C.3.2 of Transducers, Part C; formalised by Aristotle (Harmonic).