Proof of `Computing the reachable configuration graph is rational`
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 94 of the paper of lax-157538, Transducers
Description
The string representation of the reachable configuration graph is a rational function of the input (Lemma C.2.3), .
Proof strategy
The concept's alphabet is a distinct inductive type from the source's; the bridge's shows the two representations equal up to the bijection of the alphabets, and the source's rational function is post-composed with the inverse letter-to-letter map (, ).
Attribution
Lemma C.2.3 of Transducers, Part C; formalised by Aristotle (Harmonic), .