Step | Hyp | Ref
| Expression |
1 | | isclwwlknon 29077 |
. . 3
β’ (π β (π(ClWWalksNOnβπΊ)π) β (π β (π ClWWalksN πΊ) β§ (πβ0) = π)) |
2 | | 3anan32 1098 |
. . . . 5
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)β0) = π β§ ((π ++ β¨βπββ©)βπ) = π) β (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)βπ) = π) β§ ((π ++ β¨βπββ©)β0) = π)) |
3 | | s1eq 14495 |
. . . . . . . . . . . 12
β’ ((πβ0) = π β β¨β(πβ0)ββ© = β¨βπββ©) |
4 | 3 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((πβ0) = π β (π ++ β¨β(πβ0)ββ©) = (π ++ β¨βπββ©)) |
5 | 4 | eleq1d 2823 |
. . . . . . . . . 10
β’ ((πβ0) = π β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β (π ++ β¨βπββ©) β (π WWalksN πΊ))) |
6 | 5 | biimpac 480 |
. . . . . . . . 9
β’ (((π ++ β¨β(πβ0)ββ©) β
(π WWalksN πΊ) β§ (πβ0) = π) β (π ++ β¨βπββ©) β (π WWalksN πΊ)) |
7 | 6 | adantl 483 |
. . . . . . . 8
β’ (((π β Word π β§ π β β) β§ ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π)) β (π ++ β¨βπββ©) β (π WWalksN πΊ)) |
8 | | fvex 6860 |
. . . . . . . . . . . . . 14
β’ (πβ0) β
V |
9 | | eleq1 2826 |
. . . . . . . . . . . . . 14
β’ ((πβ0) = π β ((πβ0) β V β π β V)) |
10 | 8, 9 | mpbii 232 |
. . . . . . . . . . . . 13
β’ ((πβ0) = π β π β V) |
11 | | clwwlknonwwlknonb.v |
. . . . . . . . . . . . . . . 16
β’ π = (VtxβπΊ) |
12 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(EdgβπΊ) =
(EdgβπΊ) |
13 | 11, 12 | wwlknp 28830 |
. . . . . . . . . . . . . . 15
β’ ((π ++ β¨βπββ©) β (π WWalksN πΊ) β ((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1) β§ βπ β (0..^π){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β (EdgβπΊ))) |
14 | | simprrl 780 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β§ (π β V β§ (π β Word π β§ π β β))) β π β Word π) |
15 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β Word π β§ π β β) β π β Word π) |
16 | 15 | anim2i 618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β V β§ (π β Word π β§ π β β)) β (π β V β§ π β Word π)) |
17 | 16 | ancomd 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β V β§ (π β Word π β§ π β β)) β (π β Word π β§ π β V)) |
18 | | ccats1alpha 14514 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Word π β§ π β V) β ((π ++ β¨βπββ©) β Word π β (π β Word π β§ π β π))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β V β§ (π β Word π β§ π β β)) β ((π ++ β¨βπββ©) β Word π β (π β Word π β§ π β π))) |
20 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Word π β§ π β π) β π β π) |
21 | 19, 20 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β V β§ (π β Word π β§ π β β)) β ((π ++ β¨βπββ©) β Word π β π β π)) |
22 | 21 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π ++ β¨βπββ©) β Word π β ((π β V β§ (π β Word π β§ π β β)) β π β π)) |
23 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β ((π β V β§ (π β Word π β§ π β β)) β π β π)) |
24 | 23 | imp 408 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β§ (π β V β§ (π β Word π β§ π β β))) β π β π) |
25 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β π β
β0) |
26 | | ccatws1lenp1b 14516 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β Word π β§ π β β0) β
((β―β(π ++
β¨βπββ©)) = (π + 1) β (β―βπ) = π)) |
27 | 25, 26 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β Word π β§ π β β) β
((β―β(π ++
β¨βπββ©)) = (π + 1) β (β―βπ) = π)) |
28 | 27 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Word π β§ π β β) β
((β―β(π ++
β¨βπββ©)) = (π + 1) β (β―βπ) = π)) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β V β§ (π β Word π β§ π β β)) β
((β―β(π ++
β¨βπββ©)) = (π + 1) β (β―βπ) = π)) |
30 | 29 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―β(π
++ β¨βπββ©)) = (π + 1) β ((π β V β§ (π β Word π β§ π β β)) β
(β―βπ) = π)) |
31 | 30 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β ((π β V β§ (π β Word π β§ π β β)) β
(β―βπ) = π)) |
32 | 31 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β§ (π β V β§ (π β Word π β§ π β β))) β
(β―βπ) = π) |
33 | 32 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β§ (π β V β§ (π β Word π β§ π β β))) β π = (β―βπ)) |
34 | 14, 24, 33 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
β’ ((((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β§ (π β V β§ (π β Word π β§ π β β))) β (π β Word π β§ π β π β§ π = (β―βπ))) |
35 | 34 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β ((π β V β§ (π β Word π β§ π β β)) β (π β Word π β§ π β π β§ π = (β―βπ)))) |
36 | 35 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
β’ (((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1) β§ βπ β (0..^π){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β (EdgβπΊ)) β ((π β V β§ (π β Word π β§ π β β)) β (π β Word π β§ π β π β§ π = (β―βπ)))) |
37 | 13, 36 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π ++ β¨βπββ©) β (π WWalksN πΊ) β ((π β V β§ (π β Word π β§ π β β)) β (π β Word π β§ π β π β§ π = (β―βπ)))) |
38 | 37 | expd 417 |
. . . . . . . . . . . . 13
β’ ((π ++ β¨βπββ©) β (π WWalksN πΊ) β (π β V β ((π β Word π β§ π β β) β (π β Word π β§ π β π β§ π = (β―βπ))))) |
39 | 10, 38 | syl5com 31 |
. . . . . . . . . . . 12
β’ ((πβ0) = π β ((π ++ β¨βπββ©) β (π WWalksN πΊ) β ((π β Word π β§ π β β) β (π β Word π β§ π β π β§ π = (β―βπ))))) |
40 | 5, 39 | sylbid 239 |
. . . . . . . . . . 11
β’ ((πβ0) = π β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β ((π β Word π β§ π β β) β (π β Word π β§ π β π β§ π = (β―βπ))))) |
41 | 40 | com13 88 |
. . . . . . . . . 10
β’ ((π β Word π β§ π β β) β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β ((πβ0) = π β (π β Word π β§ π β π β§ π = (β―βπ))))) |
42 | 41 | imp32 420 |
. . . . . . . . 9
β’ (((π β Word π β§ π β β) β§ ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π)) β (π β Word π β§ π β π β§ π = (β―βπ))) |
43 | | ccats1val2 14522 |
. . . . . . . . 9
β’ ((π β Word π β§ π β π β§ π = (β―βπ)) β ((π ++ β¨βπββ©)βπ) = π) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
β’ (((π β Word π β§ π β β) β§ ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π)) β ((π ++ β¨βπββ©)βπ) = π) |
45 | | ccat1st1st 14523 |
. . . . . . . . . . . 12
β’ (π β Word π β ((π ++ β¨β(πβ0)ββ©)β0) = (πβ0)) |
46 | 45 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β Word π β§ π β β) β ((π ++ β¨β(πβ0)ββ©)β0) = (πβ0)) |
47 | 4 | fveq1d 6849 |
. . . . . . . . . . . . 13
β’ ((πβ0) = π β ((π ++ β¨β(πβ0)ββ©)β0) = ((π ++ β¨βπββ©)β0)) |
48 | 47 | eqeq1d 2739 |
. . . . . . . . . . . 12
β’ ((πβ0) = π β (((π ++ β¨β(πβ0)ββ©)β0) = (πβ0) β ((π ++ β¨βπββ©)β0) = (πβ0))) |
49 | 48 | adantl 483 |
. . . . . . . . . . 11
β’ (((π ++ β¨β(πβ0)ββ©) β
(π WWalksN πΊ) β§ (πβ0) = π) β (((π ++ β¨β(πβ0)ββ©)β0) = (πβ0) β ((π ++ β¨βπββ©)β0) = (πβ0))) |
50 | 46, 49 | syl5ibcom 244 |
. . . . . . . . . 10
β’ ((π β Word π β§ π β β) β (((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π) β ((π ++ β¨βπββ©)β0) = (πβ0))) |
51 | 50 | imp 408 |
. . . . . . . . 9
β’ (((π β Word π β§ π β β) β§ ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π)) β ((π ++ β¨βπββ©)β0) = (πβ0)) |
52 | | simprr 772 |
. . . . . . . . 9
β’ (((π β Word π β§ π β β) β§ ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π)) β (πβ0) = π) |
53 | 51, 52 | eqtrd 2777 |
. . . . . . . 8
β’ (((π β Word π β§ π β β) β§ ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π)) β ((π ++ β¨βπββ©)β0) = π) |
54 | 7, 44, 53 | jca31 516 |
. . . . . . 7
β’ (((π β Word π β§ π β β) β§ ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π)) β (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)βπ) = π) β§ ((π ++ β¨βπββ©)β0) = π)) |
55 | 54 | ex 414 |
. . . . . 6
β’ ((π β Word π β§ π β β) β (((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π) β (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)βπ) = π) β§ ((π ++ β¨βπββ©)β0) = π))) |
56 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β§ (π β Word π β§ π β β)) β π β Word π) |
57 | 27 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―β(π
++ β¨βπββ©)) = (π + 1) β ((π β Word π β§ π β β) β (β―βπ) = π)) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β ((π β Word π β§ π β β) β (β―βπ) = π)) |
59 | 58 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β§ (π β Word π β§ π β β)) β
(β―βπ) = π) |
60 | 59 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β§ (π β Word π β§ π β β)) β π = (β―βπ)) |
61 | 56, 60 | jca 513 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β§ (π β Word π β§ π β β)) β (π β Word π β§ π = (β―βπ))) |
62 | 61 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ (((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1)) β ((π β Word π β§ π β β) β (π β Word π β§ π = (β―βπ)))) |
63 | 62 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
β’ (((π ++ β¨βπββ©) β Word π β§ (β―β(π ++ β¨βπββ©)) = (π + 1) β§ βπ β (0..^π){((π ++ β¨βπββ©)βπ), ((π ++ β¨βπββ©)β(π + 1))} β (EdgβπΊ)) β ((π β Word π β§ π β β) β (π β Word π β§ π = (β―βπ)))) |
64 | 13, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π ++ β¨βπββ©) β (π WWalksN πΊ) β ((π β Word π β§ π β β) β (π β Word π β§ π = (β―βπ)))) |
65 | 64 | imp 408 |
. . . . . . . . . . . . . . 15
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (π β Word π β§ π β β)) β (π β Word π β§ π = (β―βπ))) |
66 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (β―βπ) β (π β β β (β―βπ) β
β)) |
67 | | lbfzo0 13619 |
. . . . . . . . . . . . . . . . . . . 20
β’ (0 β
(0..^(β―βπ))
β (β―βπ)
β β) |
68 | 67 | biimpri 227 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπ)
β β β 0 β (0..^(β―βπ))) |
69 | 66, 68 | syl6bi 253 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (β―βπ) β (π β β β 0 β
(0..^(β―βπ)))) |
70 | 69 | com12 32 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π = (β―βπ) β 0 β
(0..^(β―βπ)))) |
71 | 70 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (π β Word π β§ π β β)) β (π = (β―βπ) β 0 β (0..^(β―βπ)))) |
72 | 71 | anim2d 613 |
. . . . . . . . . . . . . . 15
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (π β Word π β§ π β β)) β ((π β Word π β§ π = (β―βπ)) β (π β Word π β§ 0 β (0..^(β―βπ))))) |
73 | 65, 72 | mpd 15 |
. . . . . . . . . . . . . 14
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (π β Word π β§ π β β)) β (π β Word π β§ 0 β (0..^(β―βπ)))) |
74 | | ccats1val1 14521 |
. . . . . . . . . . . . . 14
β’ ((π β Word π β§ 0 β (0..^(β―βπ))) β ((π ++ β¨βπββ©)β0) = (πβ0)) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (π β Word π β§ π β β)) β ((π ++ β¨βπββ©)β0) = (πβ0)) |
76 | 75 | eqeq1d 2739 |
. . . . . . . . . . . 12
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (π β Word π β§ π β β)) β (((π ++ β¨βπββ©)β0) = π β (πβ0) = π)) |
77 | 76 | biimpd 228 |
. . . . . . . . . . 11
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (π β Word π β§ π β β)) β (((π ++ β¨βπββ©)β0) = π β (πβ0) = π)) |
78 | 77 | ex 414 |
. . . . . . . . . 10
β’ ((π ++ β¨βπββ©) β (π WWalksN πΊ) β ((π β Word π β§ π β β) β (((π ++ β¨βπββ©)β0) = π β (πβ0) = π))) |
79 | 78 | adantr 482 |
. . . . . . . . 9
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)βπ) = π) β ((π β Word π β§ π β β) β (((π ++ β¨βπββ©)β0) = π β (πβ0) = π))) |
80 | 79 | com3r 87 |
. . . . . . . 8
β’ (((π ++ β¨βπββ©)β0) = π β (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)βπ) = π) β ((π β Word π β§ π β β) β (πβ0) = π))) |
81 | 80 | impcom 409 |
. . . . . . 7
β’ ((((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)βπ) = π) β§ ((π ++ β¨βπββ©)β0) = π) β ((π β Word π β§ π β β) β (πβ0) = π)) |
82 | 5 | biimparc 481 |
. . . . . . . . . 10
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (πβ0) = π) β (π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ)) |
83 | | simpr 486 |
. . . . . . . . . 10
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (πβ0) = π) β (πβ0) = π) |
84 | 82, 83 | jca 513 |
. . . . . . . . 9
β’ (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ (πβ0) = π) β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π)) |
85 | 84 | ex 414 |
. . . . . . . 8
β’ ((π ++ β¨βπββ©) β (π WWalksN πΊ) β ((πβ0) = π β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π))) |
86 | 85 | ad2antrr 725 |
. . . . . . 7
β’ ((((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)βπ) = π) β§ ((π ++ β¨βπββ©)β0) = π) β ((πβ0) = π β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π))) |
87 | 81, 86 | syldc 48 |
. . . . . 6
β’ ((π β Word π β§ π β β) β ((((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)βπ) = π) β§ ((π ++ β¨βπββ©)β0) = π) β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π))) |
88 | 55, 87 | impbid 211 |
. . . . 5
β’ ((π β Word π β§ π β β) β (((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π) β (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)βπ) = π) β§ ((π ++ β¨βπββ©)β0) = π))) |
89 | 2, 88 | bitr4id 290 |
. . . 4
β’ ((π β Word π β§ π β β) β (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)β0) = π β§ ((π ++ β¨βπββ©)βπ) = π) β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π))) |
90 | 11 | clwwlknwwlksnb 29041 |
. . . . 5
β’ ((π β Word π β§ π β β) β (π β (π ClWWalksN πΊ) β (π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ))) |
91 | 90 | anbi1d 631 |
. . . 4
β’ ((π β Word π β§ π β β) β ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β§ (πβ0) = π))) |
92 | 89, 91 | bitr4d 282 |
. . 3
β’ ((π β Word π β§ π β β) β (((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)β0) = π β§ ((π ++ β¨βπββ©)βπ) = π) β (π β (π ClWWalksN πΊ) β§ (πβ0) = π))) |
93 | 1, 92 | bitr4id 290 |
. 2
β’ ((π β Word π β§ π β β) β (π β (π(ClWWalksNOnβπΊ)π) β ((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)β0) = π β§ ((π ++ β¨βπββ©)βπ) = π))) |
94 | | wwlknon 28844 |
. 2
β’ ((π ++ β¨βπββ©) β (π(π WWalksNOn πΊ)π) β ((π ++ β¨βπββ©) β (π WWalksN πΊ) β§ ((π ++ β¨βπββ©)β0) = π β§ ((π ++ β¨βπββ©)βπ) = π)) |
95 | 93, 94 | bitr4di 289 |
1
β’ ((π β Word π β§ π β β) β (π β (π(ClWWalksNOnβπΊ)π) β (π ++ β¨βπββ©) β (π(π WWalksNOn πΊ)π))) |