Description: Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | df-s7 | |- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> ) |
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 | 0 1 2 3 4 5 6 | cs7 | |- <" A B C D E F G "> |
8 | 0 1 2 3 4 5 | cs6 | |- <" A B C D E F "> |
9 | cconcat | |- ++ |
|
10 | 6 | cs1 | |- <" G "> |
11 | 8 10 9 | co | |- ( <" A B C D E F "> ++ <" G "> ) |
12 | 7 11 | wceq | |- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> ) |