The source proves the regularity of the languages recognised by pebble automata (a pebble transducer whose output is a single accepting bit) by induction on the number of pebbles, the top pebble being eliminated by a two-way automaton that guesses the run of the automaton below it ($PartD/PebbleLev1.lean$, $PartD/PebbleAut.lean$, $PartD/PebbleReg.lean$); the inverse image of a regular language under the transducer is then recognised by a pebble automaton. The concept's pebble transducers are transported by $toSrcPeb$, whose configuration graph is that of the concept's transducer ($stepCfg_toSrcPeb$, $reaches_toSrcPeb$), giving $isPebbleTransducer_iff$.

Theorem D.2.1 of Transducers, Part D; formalised by Aristotle (Harmonic).