Definition df-s8

Description: Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	df-s8	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ++ ⟨“ 𝐻 ”⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cC	⊢ 𝐶
3		cD	⊢ 𝐷
4		cE	⊢ 𝐸
5		cF	⊢ 𝐹
6		cG	⊢ 𝐺
7		cH	⊢ 𝐻
8	0 1 2 3 4 5 6 7	cs8	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩
9	0 1 2 3 4 5 6	cs7	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩
10		cconcat	⊢ ++
11	7	cs1	⊢ ⟨“ 𝐻 ”⟩
12	9 11 10	co	⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ++ ⟨“ 𝐻 ”⟩ )
13	8 12	wceq	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ++ ⟨“ 𝐻 ”⟩ )