Proof of `Pebble transducers are computed by for-transducers`
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
Every pebble transducer computes a function of a for-transducer (Theorem D.2.4, from pebble transducers to for-transducers).
Proof strategy
The source proves by induction on the number of pebbles that a pebble transducer computes a polyregular function: the run of the top pebble between two consecutive configurations of the pebble below is a two-way transducer on the string representation of that configuration, and the sequence of those configurations is a marked squaring followed by a regular function (, , ); Theorem D.1.1 then gives a for-transducer (, left to right). and transport hypothesis and conclusion.
Attribution
Theorem D.2.4 of Transducers, Part D; formalised by Aristotle (Harmonic).