Definition·D080
Concatenation of a sequence of sequences
Join any finite number of sequences end to end, in order, generalizing binary concatenation.
For
a set,
, and
with
, the concatenation
is the element
characterized by:
and
In words
If there are zero sequences then the concatenation is the empty sequence; and for any m, if there are m+1 sequences then the concatenation is the first m sequences concatenated, followed by the last one.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
Existence and uniqueness, with this recursive computation rule, is T30 (by strong induction on
, mirroring the Euclidean algorithm's own recursive existence proof).
generalizes binary concatenation
to any finite number of pieces joined in order; needed because a language symbol's arity can be any natural number, so term and formula formation must join arbitrarily many argument-sequences at once, not just two. Here
and
are as in D074, and
is the restriction of
to its first
entries.