Description: Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | s1s6 | ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-s6 | ⊢ ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ++ ⟨“ 𝐺 ”⟩ ) | |
2 | s1cli | ⊢ ⟨“ 𝐴 ”⟩ ∈ Word V | |
3 | s5cli | ⊢ ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ∈ Word V | |
4 | df-s7 | ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ++ ⟨“ 𝐺 ”⟩ ) | |
5 | s1s5 | ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ) | |
6 | 1 2 3 4 5 | cats1cat | ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ) |