Step | Hyp | Ref
| Expression |
1 | | wwlksnextbij0.d |
. 2
Word substr
lastS lastS |
2 | | 3anass 1042 |
. . . . 5
substr lastS lastS substr lastS
lastS |
3 | 2 | bianass 842 |
. . . 4
Word
substr lastS lastS
Word
substr
lastS lastS |
4 | | wwlksnextbij0.v |
. . . . . . . . . . 11
Vtx |
5 | 4 | wwlknbp 26733 |
. . . . . . . . . 10
WWalksN
Word |
6 | | simpl 473 |
. . . . . . . . . . . . . 14
Word substr lastS
lastS |
7 | | simpl 473 |
. . . . . . . . . . . . . . . 16
Word
Word |
8 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . 20
|
9 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . 21
|
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
11 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . . . . . 20
|
12 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . . . . 21
|
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
14 | 8, 10, 11, 13 | addgegt0d 10601 |
. . . . . . . . . . . . . . . . . . 19
|
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Word
|
16 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 16 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
Word |
18 | 15, 17 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
Word |
19 | | hashgt0n0 13156 |
. . . . . . . . . . . . . . . . 17
Word |
20 | 7, 18, 19 | syl2an2 875 |
. . . . . . . . . . . . . . . 16
Word |
21 | | lswcl 13355 |
. . . . . . . . . . . . . . . 16
Word lastS |
22 | 7, 20, 21 | syl2an2 875 |
. . . . . . . . . . . . . . 15
Word lastS
|
23 | 22 | adantrr 753 |
. . . . . . . . . . . . . 14
Word substr lastS
lastS lastS |
24 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . . . . . 21
Word substr
Word |
25 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . 21
substr Word substr
Word |
26 | 24, 25 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . 20
substr Word Word |
27 | 26 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . 19
substr
Word Word |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
substr
lastS lastS Word
Word |
29 | 28 | com12 32 |
. . . . . . . . . . . . . . . . 17
Word substr
lastS lastS Word |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word substr lastS
lastS Word |
31 | 30 | imp 445 |
. . . . . . . . . . . . . . 15
Word substr lastS
lastS
Word |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . 14
Word substr lastS
lastS Word |
33 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
substr ++ lastS
substr ++
lastS |
34 | 33 | eqcoms 2630 |
. . . . . . . . . . . . . . . . 17
substr
++ lastS
substr ++
lastS |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . . 16
substr
lastS lastS ++ lastS substr ++ lastS |
36 | 35 | ad2antll 765 |
. . . . . . . . . . . . . . 15
Word substr lastS
lastS ++ lastS substr ++ lastS |
37 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
Word |
39 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
40 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
41 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
42 | 39, 40, 41 | addsubassd 10412 |
. . . . . . . . . . . . . . . . . . . . . 22
|
43 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
45 | 44 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
46 | 42, 45 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | 38, 46 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . 20
Word |
48 | 47 | opeq2d 4409 |
. . . . . . . . . . . . . . . . . . 19
Word
|
49 | 48 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
Word substr substr |
50 | 49 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
Word substr ++ lastS substr ++ lastS |
51 | | swrdccatwrd 13468 |
. . . . . . . . . . . . . . . . . 18
Word substr
++
lastS
|
52 | 7, 20, 51 | syl2an2 875 |
. . . . . . . . . . . . . . . . 17
Word substr ++ lastS |
53 | 50, 52 | eqtr3d 2658 |
. . . . . . . . . . . . . . . 16
Word substr ++ lastS |
54 | 53 | adantrr 753 |
. . . . . . . . . . . . . . 15
Word substr lastS
lastS substr
++ lastS
|
55 | 36, 54 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
Word substr lastS
lastS ++ lastS |
56 | | simprrr 805 |
. . . . . . . . . . . . . 14
Word substr lastS
lastS lastS lastS |
57 | | wwlksnextbij0.e |
. . . . . . . . . . . . . . 15
Edg |
58 | 4, 57 | wwlksnextbi 26789 |
. . . . . . . . . . . . . 14
lastS
Word ++ lastS lastS lastS
WWalksN
WWalksN |
59 | 6, 23, 32, 55, 56, 58 | syl23anc 1333 |
. . . . . . . . . . . . 13
Word substr lastS
lastS WWalksN
WWalksN |
60 | 59 | exbiri 652 |
. . . . . . . . . . . 12
Word substr lastS
lastS
WWalksN
WWalksN |
61 | 60 | com23 86 |
. . . . . . . . . . 11
WWalksN
Word substr lastS
lastS
WWalksN
|
62 | 61 | 3ad2ant2 1083 |
. . . . . . . . . 10
Word
WWalksN
Word substr lastS
lastS
WWalksN
|
63 | 5, 62 | mpcom 38 |
. . . . . . . . 9
WWalksN
Word substr lastS
lastS
WWalksN
|
64 | 63 | expcomd 454 |
. . . . . . . 8
WWalksN
substr
lastS lastS
Word
WWalksN |
65 | 64 | imp 445 |
. . . . . . 7
WWalksN substr
lastS lastS Word WWalksN |
66 | 4, 57 | wwlknp 26734 |
. . . . . . . . . . . 12
WWalksN
Word ..^ |
67 | 39, 41, 41 | addassd 10062 |
. . . . . . . . . . . . . . . . . . . 20
|
68 | | 1p1e2 11134 |
. . . . . . . . . . . . . . . . . . . . . 22
|
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | 69 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | 67, 70 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
72 | 71 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
73 | 72 | biimpd 219 |
. . . . . . . . . . . . . . . . 17
|
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word |
75 | 74 | com12 32 |
. . . . . . . . . . . . . . 15
Word |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . 14
Word
Word
|
77 | | simpl 473 |
. . . . . . . . . . . . . 14
Word
Word |
78 | 76, 77 | jctild 566 |
. . . . . . . . . . . . 13
Word
Word
Word |
79 | 78 | 3adant3 1081 |
. . . . . . . . . . . 12
Word
..^ Word Word |
80 | 66, 79 | syl 17 |
. . . . . . . . . . 11
WWalksN
Word Word
|
81 | 80 | com12 32 |
. . . . . . . . . 10
Word WWalksN Word
|
82 | 81 | 3adant1 1079 |
. . . . . . . . 9
Word WWalksN Word
|
83 | 5, 82 | syl 17 |
. . . . . . . 8
WWalksN
WWalksN
Word |
84 | 83 | adantr 481 |
. . . . . . 7
WWalksN substr
lastS lastS WWalksN Word
|
85 | 65, 84 | impbid 202 |
. . . . . 6
WWalksN substr
lastS lastS Word WWalksN |
86 | 85 | ex 450 |
. . . . 5
WWalksN
substr
lastS lastS
Word
WWalksN
|
87 | 86 | pm5.32rd 672 |
. . . 4
WWalksN
Word substr lastS
lastS WWalksN
substr
lastS lastS |
88 | 3, 87 | syl5bb 272 |
. . 3
WWalksN
Word
substr lastS lastS
WWalksN
substr
lastS lastS |
89 | 88 | rabbidva2 3186 |
. 2
WWalksN
Word substr
lastS lastS WWalksN substr
lastS lastS |
90 | 1, 89 | syl5eq 2668 |
1
WWalksN
WWalksN substr
lastS lastS |