Proof of `A for-transducer reads the children off a child configuration graph`
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 170 of the paper of lax-157538, Transducers
Description
A for-transducer maps the string representation of a child configuration graph to the concatenation of the representations of the children (Claim D.2.7), .
Proof strategy
The source's for-transducer is a one-pebble transducer that follows the recorded edges from the first child, outputting the representation of the current child at every vertex (, ), and Theorem D.2.4 makes it a for-transducer; its correctness rests on a string representing at most one run of children (). The concept's graphs are transported along the bijection of the alphabets: the local consistency test, the recorded edges and the output commute with the bijection (), and the source's for-transducer is pre-composed with it ().
Attribution
Claim D.2.7 of Transducers, Part D; formalised by Aristotle (Harmonic), .