Proof of `Balanced runs between configurations are regular`
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.
In the paper
- page 167 of the paper of lax-157538, Transducers
Description
For every height , the string representations of pairs of configurations of height connected by a balanced run form a regular language (Claim D.2.3), .
Proof strategy
The same pebble automaton as for Lemma D.2.2, restricted to runs that never pop below height (); the concept's balanced run is the source's restricted reachability, transported by .
Attribution
Claim D.2.3 of Transducers, Part D; formalised by Aristotle (Harmonic), .