Proof of `k-types are a congruence for concatenation`
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
The -type of a concatenation is determined by the -types of the parts (Lemma C.4.15, congruence): induction on , a factorisation of around a letter being a factorisation of or of (, second conjunct).
Attribution
Lemma C.4.15 of Transducers, Part C; formalised by Aristotle (Harmonic), , .