Metamath Proof Explorer

Definition df-s8

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

Ref Expression
Assertion df-s8 
|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cB 
 |-  B
2 cC 
 |-  C
3 cD 
 |-  D
4 cE 
 |-  E
5 cF 
 |-  F
6 cG 
 |-  G
7 cH 
 |-  H
8 0 1 2 3 4 5 6 7 cs8 
 |-  <" A B C D E F G H ">
9 0 1 2 3 4 5 6 cs7 
 |-  <" A B C D E F G ">
10 cconcat 
 |-  ++
11 7 cs1 
 |-  <" H ">
12 9 11 10 co 
 |-  ( <" A B C D E F G "> ++ <" H "> )
13 8 12 wceq 
 |-  <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )