Proof of `Two-way transducers are closed under composition`
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.
In the paper
- page 95 of the paper of lax-157538, Transducers
Description
Two-way transducers are closed under composition (Theorem C.2.5), : the second transducer is simulated on the run of the first, walking backwards along the run when it moves left.
Attribution
Theorem C.2.5 of Transducers, Part C (Chytil and Jákl); formalised by Aristotle (Harmonic), .