Step | Hyp | Ref
| Expression |
1 | | pfxwlk 34114 |
. . . . . . 7
โข ((๐น(Walksโ๐บ)๐ โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐น prefix ๐ฟ)(Walksโ๐บ)(๐ prefix (๐ฟ + 1))) |
2 | 1 | 3adant2 1132 |
. . . . . 6
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐น prefix ๐ฟ)(Walksโ๐บ)(๐ prefix (๐ฟ + 1))) |
3 | | revwlk 34115 |
. . . . . 6
โข ((๐น prefix ๐ฟ)(Walksโ๐บ)(๐ prefix (๐ฟ + 1)) โ (reverseโ(๐น prefix ๐ฟ))(Walksโ๐บ)(reverseโ(๐ prefix (๐ฟ + 1)))) |
4 | 2, 3 | syl 17 |
. . . . 5
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (reverseโ(๐น prefix ๐ฟ))(Walksโ๐บ)(reverseโ(๐ prefix (๐ฟ + 1)))) |
5 | | fznn0sub2 13608 |
. . . . . . 7
โข (๐ต โ (0...๐ฟ) โ (๐ฟ โ ๐ต) โ (0...๐ฟ)) |
6 | 5 | 3ad2ant2 1135 |
. . . . . 6
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐ฟ โ ๐ต) โ (0...๐ฟ)) |
7 | | eqid 2733 |
. . . . . . . . . . 11
โข
(iEdgโ๐บ) =
(iEdgโ๐บ) |
8 | 7 | wlkf 28871 |
. . . . . . . . . 10
โข (๐น(Walksโ๐บ)๐ โ ๐น โ Word dom (iEdgโ๐บ)) |
9 | 8 | 3ad2ant1 1134 |
. . . . . . . . 9
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ ๐น โ Word dom (iEdgโ๐บ)) |
10 | | pfxcl 14627 |
. . . . . . . . 9
โข (๐น โ Word dom
(iEdgโ๐บ) โ
(๐น prefix ๐ฟ) โ Word dom (iEdgโ๐บ)) |
11 | | revlen 14712 |
. . . . . . . . 9
โข ((๐น prefix ๐ฟ) โ Word dom (iEdgโ๐บ) โ
(โฏโ(reverseโ(๐น prefix ๐ฟ))) = (โฏโ(๐น prefix ๐ฟ))) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . 8
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ
(โฏโ(reverseโ(๐น prefix ๐ฟ))) = (โฏโ(๐น prefix ๐ฟ))) |
13 | | pfxlen 14633 |
. . . . . . . . . 10
โข ((๐น โ Word dom
(iEdgโ๐บ) โง ๐ฟ โ
(0...(โฏโ๐น)))
โ (โฏโ(๐น
prefix ๐ฟ)) = ๐ฟ) |
14 | 8, 13 | sylan 581 |
. . . . . . . . 9
โข ((๐น(Walksโ๐บ)๐ โง ๐ฟ โ (0...(โฏโ๐น))) โ (โฏโ(๐น prefix ๐ฟ)) = ๐ฟ) |
15 | 14 | 3adant2 1132 |
. . . . . . . 8
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (โฏโ(๐น prefix ๐ฟ)) = ๐ฟ) |
16 | 12, 15 | eqtrd 2773 |
. . . . . . 7
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ
(โฏโ(reverseโ(๐น prefix ๐ฟ))) = ๐ฟ) |
17 | 16 | oveq2d 7425 |
. . . . . 6
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ
(0...(โฏโ(reverseโ(๐น prefix ๐ฟ)))) = (0...๐ฟ)) |
18 | 6, 17 | eleqtrrd 2837 |
. . . . 5
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐ฟ โ ๐ต) โ
(0...(โฏโ(reverseโ(๐น prefix ๐ฟ))))) |
19 | | pfxwlk 34114 |
. . . . 5
โข
(((reverseโ(๐น
prefix ๐ฟ))(Walksโ๐บ)(reverseโ(๐ prefix (๐ฟ + 1))) โง (๐ฟ โ ๐ต) โ
(0...(โฏโ(reverseโ(๐น prefix ๐ฟ))))) โ ((reverseโ(๐น prefix ๐ฟ)) prefix (๐ฟ โ ๐ต))(Walksโ๐บ)((reverseโ(๐ prefix (๐ฟ + 1))) prefix ((๐ฟ โ ๐ต) + 1))) |
20 | 4, 18, 19 | syl2anc 585 |
. . . 4
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ
((reverseโ(๐น prefix
๐ฟ)) prefix (๐ฟ โ ๐ต))(Walksโ๐บ)((reverseโ(๐ prefix (๐ฟ + 1))) prefix ((๐ฟ โ ๐ต) + 1))) |
21 | | elfzel2 13499 |
. . . . . . . 8
โข (๐ต โ (0...๐ฟ) โ ๐ฟ โ โค) |
22 | 21 | 3ad2ant2 1135 |
. . . . . . 7
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ ๐ฟ โ โค) |
23 | 22 | zcnd 12667 |
. . . . . 6
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ ๐ฟ โ โ) |
24 | | 1cnd 11209 |
. . . . . 6
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ 1 โ
โ) |
25 | | elfzelz 13501 |
. . . . . . . 8
โข (๐ต โ (0...๐ฟ) โ ๐ต โ โค) |
26 | 25 | 3ad2ant2 1135 |
. . . . . . 7
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ ๐ต โ โค) |
27 | 26 | zcnd 12667 |
. . . . . 6
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ ๐ต โ โ) |
28 | 23, 24, 27 | addsubd 11592 |
. . . . 5
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ ((๐ฟ + 1) โ ๐ต) = ((๐ฟ โ ๐ต) + 1)) |
29 | 28 | oveq2d 7425 |
. . . 4
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ
((reverseโ(๐ prefix
(๐ฟ + 1))) prefix ((๐ฟ + 1) โ ๐ต)) = ((reverseโ(๐ prefix (๐ฟ + 1))) prefix ((๐ฟ โ ๐ต) + 1))) |
30 | 20, 29 | breqtrrd 5177 |
. . 3
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ
((reverseโ(๐น prefix
๐ฟ)) prefix (๐ฟ โ ๐ต))(Walksโ๐บ)((reverseโ(๐ prefix (๐ฟ + 1))) prefix ((๐ฟ + 1) โ ๐ต))) |
31 | | revwlk 34115 |
. . 3
โข
(((reverseโ(๐น
prefix ๐ฟ)) prefix (๐ฟ โ ๐ต))(Walksโ๐บ)((reverseโ(๐ prefix (๐ฟ + 1))) prefix ((๐ฟ + 1) โ ๐ต)) โ
(reverseโ((reverseโ(๐น prefix ๐ฟ)) prefix (๐ฟ โ ๐ต)))(Walksโ๐บ)(reverseโ((reverseโ(๐ prefix (๐ฟ + 1))) prefix ((๐ฟ + 1) โ ๐ต)))) |
32 | 30, 31 | syl 17 |
. 2
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ
(reverseโ((reverseโ(๐น prefix ๐ฟ)) prefix (๐ฟ โ ๐ต)))(Walksโ๐บ)(reverseโ((reverseโ(๐ prefix (๐ฟ + 1))) prefix ((๐ฟ + 1) โ ๐ต)))) |
33 | | swrdrevpfx 34107 |
. . 3
โข ((๐น โ Word dom
(iEdgโ๐บ) โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐น substr โจ๐ต, ๐ฟโฉ) =
(reverseโ((reverseโ(๐น prefix ๐ฟ)) prefix (๐ฟ โ ๐ต)))) |
34 | 8, 33 | syl3an1 1164 |
. 2
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐น substr โจ๐ต, ๐ฟโฉ) =
(reverseโ((reverseโ(๐น prefix ๐ฟ)) prefix (๐ฟ โ ๐ต)))) |
35 | | eqid 2733 |
. . . . 5
โข
(Vtxโ๐บ) =
(Vtxโ๐บ) |
36 | 35 | wlkpwrd 28874 |
. . . 4
โข (๐น(Walksโ๐บ)๐ โ ๐ โ Word (Vtxโ๐บ)) |
37 | 36 | 3ad2ant1 1134 |
. . 3
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ ๐ โ Word (Vtxโ๐บ)) |
38 | | fzelp1 13553 |
. . . 4
โข (๐ต โ (0...๐ฟ) โ ๐ต โ (0...(๐ฟ + 1))) |
39 | 38 | 3ad2ant2 1135 |
. . 3
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ ๐ต โ (0...(๐ฟ + 1))) |
40 | | fzp1elp1 13554 |
. . . . 5
โข (๐ฟ โ
(0...(โฏโ๐น))
โ (๐ฟ + 1) โ
(0...((โฏโ๐น) +
1))) |
41 | 40 | 3ad2ant3 1136 |
. . . 4
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐ฟ + 1) โ (0...((โฏโ๐น) + 1))) |
42 | | wlklenvp1 28875 |
. . . . . 6
โข (๐น(Walksโ๐บ)๐ โ (โฏโ๐) = ((โฏโ๐น) + 1)) |
43 | 42 | 3ad2ant1 1134 |
. . . . 5
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (โฏโ๐) = ((โฏโ๐น) + 1)) |
44 | 43 | oveq2d 7425 |
. . . 4
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ
(0...(โฏโ๐)) =
(0...((โฏโ๐น) +
1))) |
45 | 41, 44 | eleqtrrd 2837 |
. . 3
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐ฟ + 1) โ (0...(โฏโ๐))) |
46 | | swrdrevpfx 34107 |
. . 3
โข ((๐ โ Word (Vtxโ๐บ) โง ๐ต โ (0...(๐ฟ + 1)) โง (๐ฟ + 1) โ (0...(โฏโ๐))) โ (๐ substr โจ๐ต, (๐ฟ + 1)โฉ) =
(reverseโ((reverseโ(๐ prefix (๐ฟ + 1))) prefix ((๐ฟ + 1) โ ๐ต)))) |
47 | 37, 39, 45, 46 | syl3anc 1372 |
. 2
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐ substr โจ๐ต, (๐ฟ + 1)โฉ) =
(reverseโ((reverseโ(๐ prefix (๐ฟ + 1))) prefix ((๐ฟ + 1) โ ๐ต)))) |
48 | 32, 34, 47 | 3brtr4d 5181 |
1
โข ((๐น(Walksโ๐บ)๐ โง ๐ต โ (0...๐ฟ) โง ๐ฟ โ (0...(โฏโ๐น))) โ (๐น substr โจ๐ต, ๐ฟโฉ)(Walksโ๐บ)(๐ substr โจ๐ต, (๐ฟ + 1)โฉ)) |