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 "> ) |
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 "> ) |