Lax Lean Archive

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

Proof of `Rational functions are MSO relabellings`

groundedproofs/Lax314295Proofs/Results.lean · lax-314295

What this proof establishes

no assumptions

thm✓Lax314295.RelabellingOfRational

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 rational function is defined by an mso relabelling (Theorem C.4.4, the converse implication): the transition formulas of a bimachine (Transducers.rationaliffmsoRelabellingTransducers.rational_iff_msoRelabelling, left to right).

Proof strategy

The source takes a bimachine for ff (Theorem B.2.3) and writes, for every pair of a left and a right state, the formula "the left automaton reaches this state before xx and the right automaton that state after xx" (Claim C.4.5, Transducers.RatRelab.existsformTransducers.RatRelab.exists_form); these formulas form a relabelling computing ff. The bridge transports the relabelling along ofSrcRelofSrcRel.

Attribution

Theorem C.4.4 of Transducers, Part C; formalised by Aristotle (Harmonic), PartC/MSORatRelab.leanPartC/MSORatRelab.lean, PartC/MarkLogic.leanPartC/MarkLogic.lean, PartC/MSO.leanPartC/MSO.lean.