Step | Hyp | Ref
| Expression |
1 | | wwlksnext.v |
. . . . 5
Vtx |
2 | | wwlksnext.e |
. . . . 5
Edg |
3 | 1, 2 | wwlknp 26734 |
. . . 4
WWalksN
Word ..^ |
4 | | wwlksnred 26787 |
. . . . . . . 8
WWalksN
substr WWalksN |
5 | 4 | ad2antrr 762 |
. . . . . . 7
Word ++
lastS
WWalksN
substr WWalksN
|
6 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
++ ++ |
7 | 6 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
++
++ |
8 | 7 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
Word
++ lastS
++ |
9 | 8 | adantl 482 |
. . . . . . . . . . . . . 14
Word ++
lastS
++ |
10 | | s1cl 13382 |
. . . . . . . . . . . . . . . . . . . . . 22
Word
|
11 | 10 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
Word |
12 | 11 | anim2i 593 |
. . . . . . . . . . . . . . . . . . . 20
Word
Word Word
|
13 | 12 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
Word
Word Word
|
14 | | ccatlen 13360 |
. . . . . . . . . . . . . . . . . . 19
Word Word ++ |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Word
++ |
16 | 15 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
Word
++
|
17 | | s1len 13385 |
. . . . . . . . . . . . . . . . . . . 20
|
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
Word
|
19 | 18 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
Word
|
20 | 19 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
Word
|
21 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . . 20
Word |
22 | 21 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
Word |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
Word
|
24 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . 20
|
25 | 24 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
|
26 | 25 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
Word
|
27 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . 18
Word
|
28 | 23, 26, 27 | addcan2d 10240 |
. . . . . . . . . . . . . . . . 17
Word
|
29 | 16, 20, 28 | 3bitrd 294 |
. . . . . . . . . . . . . . . 16
Word
++
|
30 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 30 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 31 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
++ substr
++ substr
|
33 | | swrdccat1 13457 |
. . . . . . . . . . . . . . . . . . 19
Word Word ++ substr
|
34 | 13, 33 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Word
++
substr |
35 | 32, 34 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . 17
Word ++ substr
|
36 | 35 | ex 450 |
. . . . . . . . . . . . . . . 16
Word
++
substr |
37 | 29, 36 | sylbid 230 |
. . . . . . . . . . . . . . 15
Word
++ ++ substr |
38 | 37 | 3ad2antr1 1226 |
. . . . . . . . . . . . . 14
Word ++
lastS
++ ++ substr |
39 | 9, 38 | sylbid 230 |
. . . . . . . . . . . . 13
Word ++
lastS
++
substr |
40 | 39 | imp 445 |
. . . . . . . . . . . 12
Word ++ lastS ++ substr |
41 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
++ substr ++ substr |
42 | 41 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
++ substr
++ substr
|
43 | 42 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
Word
++ lastS substr
++ substr |
44 | 43 | ad2antlr 763 |
. . . . . . . . . . . 12
Word ++ lastS substr
++ substr
|
45 | 40, 44 | mpbird 247 |
. . . . . . . . . . 11
Word ++ lastS substr
|
46 | 45 | eleq1d 2686 |
. . . . . . . . . 10
Word ++ lastS substr WWalksN
WWalksN |
47 | 46 | biimpd 219 |
. . . . . . . . 9
Word ++ lastS substr WWalksN
WWalksN |
48 | 47 | ex 450 |
. . . . . . . 8
Word ++
lastS
substr
WWalksN WWalksN
|
49 | 48 | com23 86 |
. . . . . . 7
Word ++
lastS
substr
WWalksN WWalksN
|
50 | 5, 49 | syld 47 |
. . . . . 6
Word ++
lastS
WWalksN
WWalksN |
51 | 50 | com13 88 |
. . . . 5
WWalksN
Word ++ lastS
WWalksN |
52 | 51 | 3ad2ant2 1083 |
. . . 4
Word
..^
WWalksN
Word ++ lastS
WWalksN |
53 | 3, 52 | mpcom 38 |
. . 3
WWalksN
Word ++
lastS
WWalksN |
54 | 53 | com12 32 |
. 2
Word ++
lastS
WWalksN
WWalksN |
55 | 1, 2 | wwlksnext 26788 |
. . . . . . . . . . 11
WWalksN
lastS
++ WWalksN |
56 | | eleq1 2689 |
. . . . . . . . . . 11
++ WWalksN
++
WWalksN |
57 | 55, 56 | syl5ibrcom 237 |
. . . . . . . . . 10
WWalksN
lastS
++
WWalksN
|
58 | 57 | 3exp 1264 |
. . . . . . . . 9
WWalksN
lastS ++
WWalksN
|
59 | 58 | com23 86 |
. . . . . . . 8
WWalksN
lastS ++
WWalksN
|
60 | 59 | com14 96 |
. . . . . . 7
++ lastS
WWalksN
WWalksN
|
61 | 60 | imp 445 |
. . . . . 6
++ lastS
WWalksN WWalksN
|
62 | 61 | 3adant1 1079 |
. . . . 5
Word
++ lastS
WWalksN WWalksN
|
63 | 62 | com12 32 |
. . . 4
Word
++
lastS
WWalksN WWalksN
|
64 | 63 | adantl 482 |
. . 3
Word ++
lastS
WWalksN WWalksN
|
65 | 64 | imp 445 |
. 2
Word ++
lastS
WWalksN
WWalksN |
66 | 54, 65 | impbid 202 |
1
Word ++
lastS
WWalksN
WWalksN |