Metamath Proof Explorer

Definition df-s6

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

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

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 0 1 2 3 4 5 cs6 
 |-  <" A B C D E F ">
7 0 1 2 3 4 cs5 
 |-  <" A B C D E ">
8 cconcat 
 |-  ++
9 5 cs1 
 |-  <" F ">
10 7 9 8 co 
 |-  ( <" A B C D E "> ++ <" F "> )
11 6 10 wceq 
 |-  <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )