Proof of `MSO relabellings are rational`
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.
Description
A function defined by an mso relabelling is rational (Theorem C.4.4, the easy implication): a bimachine reading, at every position, the answers of the formulas (, right to left).
Proof strategy
The source evaluates the formulas of the relabelling by the automata of Lemma C.4.2 run from both ends (, ) and concludes by Theorem B.2.3 on bimachines. The concept's relabelling is the source's through with its graph (); rational functions come from Part B's bridge.
Attribution
Theorem C.4.4 of Transducers, Part C; formalised by Aristotle (Harmonic), , .