Proof of `For-transducers compute polyregular functions`
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 computes a polyregular function (Theorem D.1.1, from for-transducers to polyregular): the prenex form of Lemma D.1.3, whose loop block is simulated by iterated marked squarings and a regular function enumerating the tuples of positions in loop order, and whose loop-free body is a regular function of the enumeration ().
Attribution
Theorem D.1.1 of Transducers, Part D; formalised by Aristotle (Harmonic), , , .