Lemma·L64
Associativity of concatenation
Joining three finite sequences end to end gives the same result however the joins are grouped.
For a set
and
:
In words
For finite sequences f, g, h from a set A, joining f to g and then h gives the same sequence as joining f to the result of joining g to h: concatenation does not care how the joins are grouped.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 (computed from the citation graph, not asserted).
Proof
- 1Write , , . By T29 twice, and , equal by associativity of addition on : both sides are functions with the same domain.
- 2Entries below : for , by T29 applied twice (once with , once with ); likewise directly. Both sides agree.
- 3Entries from to : for with , by T29 (using , order and addition). On the other side, by T29 applied twice ( ). Both sides agree.
- 4Entries from on: for with , by T29 (domain of is ). On the other side, by associativity, and by T29 applied twice (domain of is , domain of is , and by order and addition). Both sides agree.
- 5Every index gives the same value on both sides, and the domains agree (step 1): by Extensionality, .
∎
Remarks
A routine but necessary bookkeeping fact: it lets
be written without parentheses, unambiguously. Used to justify building a term or formula up one symbol or one argument at a time regardless of the order the pieces are assembled in, e.g. in verifying the parse-balance invariant for a function application built via n-ary concatenation.