Proof of `Rational relations are closed under composition`
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 38 of the paper of lax-157538, Transducers
Description
Rational relations are closed under composition (Theorem B.1.4): the product construction on ε-normalised automata ().
Attribution
Theorem B.1.4 of Transducers; Lean proof by Aristotle ().