Proof of `First-order relabellings are computed by aperiodic bimachines`
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 first-order relabelling is computed by an aperiodic bimachine (Theorem C.4.16, the first implication): aperiodic automata for the formulas run from both ends (, left to right).
Proof strategy
The source turns every formula of the relabelling, with its free variable replaced by a marked position, into a first-order sentence, recognises it by an aperiodic dfa (Theorem C.4.11) and by its reverse, and assembles the products into a bimachine whose left and right automata are aperiodic (, , ). The bridge transports the relabelling along with ; aperiodic bimachines come from Part B's bridge.
Attribution
Theorem C.4.16 of Transducers, Part C; formalised by Aristotle (Harmonic), , .