Lax Lean Archive

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

Proof of `Aperiodic bimachines compute first-order relabellings`

groundedproofs/Lax314295Proofs/Results.lean · lax-314295

What this proof establishes

no assumptions

thm✓Lax314295.FORelabellingOfAperiodicBimachine

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

A function computed by an aperiodic bimachine is a first-order relabelling (Theorem C.4.16, the converse implication): the runs of an aperiodic automaton are first-order describable (Transducers.foRelabellingiffaperiodicBimachineTransducers.foRelabelling_iff_aperiodicBimachine, right to left).

Proof strategy

The source describes, by Theorem C.4.11 relativised to the positions before and after xx, the states of the left and right automata of the bimachine at xx in first-order logic; the formulas "left state pp, letter aa, right state ss at xx" form a first-order relabelling computing ff (PartC/FOBimachRelab.leanPartC/FOBimachRelab.lean). The bridge transports the relabelling along ofSrcRelofSrcRel.

Attribution

Theorem C.4.16 of Transducers, Part C; formalised by Aristotle (Harmonic), PartC/FOBimachRelab.leanPartC/FOBimachRelab.lean, PartC/MSO.leanPartC/MSO.lean.