Proof of `A for-transducer produces the children of a configuration`
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 169 of the paper of lax-157538, Transducers
Description
A for-transducer maps the string representation of a configuration to the concatenation of the representations of its children (Lemma D.2.5), : the composition (Lemma D.1.4) of the for-transducers of Claims D.2.6 and D.2.7.
Proof strategy
The source states the lemma after Theorems D.1.1 and D.2.4, from which the for-transducers of the two claims are obtained. The concept's children are the source's through (runs staying above a height are transported by ), and the representation of a configuration unfolds identically ().
Attribution
Lemma D.2.5 of Transducers, Part D; formalised by Aristotle (Harmonic), .