Proof of `For-transducers are computed by pebble 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 for-transducer is simulated by a pebble transducer (Theorem D.2.4, from for-transducers to pebble transducers): the loop variables become the pebbles, in nesting order, and the Boolean variables are kept in the state (, ).
Attribution
Theorem D.2.4 of Transducers, Part D; formalised by Aristotle (Harmonic).