List of theorems referencing the symbol CONCAT

(381) Theorem 330: [Concatenation of finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp ((concat(F,G) in Fin_seqs(S)) & (domain(concat(F,G)) = domain(F) •PLUS domain(G)) & (range(concat(F,G)) = range(F) + range(G))) & ((U in domain(F) •PLUS domain(G)) •imp (concat(F,G)~[U] = if U in domain(F) then F~[U] else G~[U •MINUS domain(F)] end if))
(382) Theorem 331: [0 is bilateral unit for sequence concatenation] (F in Fin_seqs(S)) •imp ((concat(F,0) = F) & (concat(0,F) = F))
(383) Theorem 332: [Associativity of sequence concatenation] ((F in Fin_seqs(S)) & (G in Fin_seqs(S)) & (H in Fin_seqs(S))) •imp (concat(F,concat(G,H)) = concat(concat(F,G),H))
(384) Theorem 333: [Concatenation of shifted sequences] ((F in Fin_seqs(S)) & (M in domain(F))) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (F = concat((F •ON M), shifted_seq(F,M))))