Lax Lean Archive

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

Proof of `Two-way transducers are continuous`

groundedproofs/Lax916827Proofs/Results.lean · lax-916827

What this proof establishes

no assumptions

thm✓Lax916827.TwoWayContinuity

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

In the paper

Description

Two-way transducers are continuous (Theorem C.2.2): the source runs a deterministic automaton for the output language inside the transducer and appeals to Shepherdson's theorem (Transducers.twoWaycontinuousTransducers.twoWay_continuous).

Attribution

Theorem C.2.2 of Transducers, Part C (Rabin–Scott, Shepherdson); formalised by Aristotle (Harmonic), PartC/TwoWayCont.leanPartC/TwoWayCont.lean, PartC/TwoDFA.leanPartC/TwoDFA.lean.