Step | Hyp | Ref
| Expression |
1 | | wlkp1.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | | wlkp1.i |
. . . 4
β’ πΌ = (iEdgβπΊ) |
3 | | wlkp1.f |
. . . 4
β’ (π β Fun πΌ) |
4 | | wlkp1.a |
. . . 4
β’ (π β πΌ β Fin) |
5 | | wlkp1.b |
. . . 4
β’ (π β π΅ β π) |
6 | | wlkp1.c |
. . . 4
β’ (π β πΆ β π) |
7 | | wlkp1.d |
. . . 4
β’ (π β Β¬ π΅ β dom πΌ) |
8 | | wlkp1.w |
. . . 4
β’ (π β πΉ(WalksβπΊ)π) |
9 | | wlkp1.n |
. . . 4
β’ π = (β―βπΉ) |
10 | | wlkp1.e |
. . . 4
β’ (π β πΈ β (EdgβπΊ)) |
11 | | wlkp1.x |
. . . 4
β’ (π β {(πβπ), πΆ} β πΈ) |
12 | | wlkp1.u |
. . . 4
β’ (π β (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©})) |
13 | | wlkp1.h |
. . . 4
β’ π» = (πΉ βͺ {β¨π, π΅β©}) |
14 | | wlkp1.q |
. . . 4
β’ π = (π βͺ {β¨(π + 1), πΆβ©}) |
15 | | wlkp1.s |
. . . 4
β’ (π β (Vtxβπ) = π) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | wlkp1lem6 28935 |
. . 3
β’ (π β βπ β (0..^π)((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ)))) |
17 | 10 | elfvexd 6931 |
. . . . . 6
β’ (π β πΊ β V) |
18 | 1, 2 | iswlkg 28870 |
. . . . . 6
β’ (πΊ β V β (πΉ(WalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))))) |
19 | 17, 18 | syl 17 |
. . . . 5
β’ (π β (πΉ(WalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))))) |
20 | 9 | eqcomi 2742 |
. . . . . . . . 9
β’
(β―βπΉ) =
π |
21 | 20 | oveq2i 7420 |
. . . . . . . 8
β’
(0..^(β―βπΉ)) = (0..^π) |
22 | 21 | raleqi 3324 |
. . . . . . 7
β’
(βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
23 | 22 | biimpi 215 |
. . . . . 6
β’
(βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
24 | 23 | 3ad2ant3 1136 |
. . . . 5
β’ ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
25 | 19, 24 | syl6bi 253 |
. . . 4
β’ (π β (πΉ(WalksβπΊ)π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))))) |
26 | 8, 25 | mpd 15 |
. . 3
β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
27 | | eqeq12 2750 |
. . . . . . 7
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1))) β ((πβπ) = (πβ(π + 1)) β (πβπ) = (πβ(π + 1)))) |
28 | 27 | 3adant3 1133 |
. . . . . 6
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β ((πβπ) = (πβ(π + 1)) β (πβπ) = (πβ(π + 1)))) |
29 | | simp3 1139 |
. . . . . . 7
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) |
30 | | simp1 1137 |
. . . . . . . 8
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β (πβπ) = (πβπ)) |
31 | 30 | sneqd 4641 |
. . . . . . 7
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β {(πβπ)} = {(πβπ)}) |
32 | 29, 31 | eqeq12d 2749 |
. . . . . 6
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β (((iEdgβπ)β(π»βπ)) = {(πβπ)} β (πΌβ(πΉβπ)) = {(πβπ)})) |
33 | | preq12 4740 |
. . . . . . . 8
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1))) β {(πβπ), (πβ(π + 1))} = {(πβπ), (πβ(π + 1))}) |
34 | 33 | 3adant3 1133 |
. . . . . . 7
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β {(πβπ), (πβ(π + 1))} = {(πβπ), (πβ(π + 1))}) |
35 | 34, 29 | sseq12d 4016 |
. . . . . 6
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β ({(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ)) β {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
36 | 28, 32, 35 | ifpbi123d 1079 |
. . . . 5
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))))) |
37 | 36 | biimprd 247 |
. . . 4
β’ (((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))))) |
38 | 37 | ral2imi 3086 |
. . 3
β’
(βπ β
(0..^π)((πβπ) = (πβπ) β§ (πβ(π + 1)) = (πβ(π + 1)) β§ ((iEdgβπ)β(π»βπ)) = (πΌβ(πΉβπ))) β (βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))))) |
39 | 16, 26, 38 | sylc 65 |
. 2
β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ)))) |
40 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | wlkp1lem3 28932 |
. . . . 5
β’ (π β ((iEdgβπ)β(π»βπ)) = ((πΌ βͺ {β¨π΅, πΈβ©})βπ΅)) |
41 | 40 | adantr 482 |
. . . 4
β’ ((π β§ (πβπ) = (πβ(π + 1))) β ((iEdgβπ)β(π»βπ)) = ((πΌ βͺ {β¨π΅, πΈβ©})βπ΅)) |
42 | 5, 10, 7 | 3jca 1129 |
. . . . . 6
β’ (π β (π΅ β π β§ πΈ β (EdgβπΊ) β§ Β¬ π΅ β dom πΌ)) |
43 | 42 | adantr 482 |
. . . . 5
β’ ((π β§ (πβπ) = (πβ(π + 1))) β (π΅ β π β§ πΈ β (EdgβπΊ) β§ Β¬ π΅ β dom πΌ)) |
44 | | fsnunfv 7185 |
. . . . 5
β’ ((π΅ β π β§ πΈ β (EdgβπΊ) β§ Β¬ π΅ β dom πΌ) β ((πΌ βͺ {β¨π΅, πΈβ©})βπ΅) = πΈ) |
45 | 43, 44 | syl 17 |
. . . 4
β’ ((π β§ (πβπ) = (πβ(π + 1))) β ((πΌ βͺ {β¨π΅, πΈβ©})βπ΅) = πΈ) |
46 | | fveq2 6892 |
. . . . . . . 8
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
47 | | fveq2 6892 |
. . . . . . . 8
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
48 | 46, 47 | eqeq12d 2749 |
. . . . . . 7
β’ (π₯ = π β ((πβπ₯) = (πβπ₯) β (πβπ) = (πβπ))) |
49 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | wlkp1lem5 28934 |
. . . . . . 7
β’ (π β βπ₯ β (0...π)(πβπ₯) = (πβπ₯)) |
50 | 2 | wlkf 28871 |
. . . . . . . . . 10
β’ (πΉ(WalksβπΊ)π β πΉ β Word dom πΌ) |
51 | | lencl 14483 |
. . . . . . . . . . 11
β’ (πΉ β Word dom πΌ β (β―βπΉ) β
β0) |
52 | 9 | eleq1i 2825 |
. . . . . . . . . . . 12
β’ (π β β0
β (β―βπΉ)
β β0) |
53 | | elnn0uz 12867 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
(β€β₯β0)) |
54 | 52, 53 | sylbb1 236 |
. . . . . . . . . . 11
β’
((β―βπΉ)
β β0 β π β
(β€β₯β0)) |
55 | 51, 54 | syl 17 |
. . . . . . . . . 10
β’ (πΉ β Word dom πΌ β π β
(β€β₯β0)) |
56 | 8, 50, 55 | 3syl 18 |
. . . . . . . . 9
β’ (π β π β
(β€β₯β0)) |
57 | 56, 53 | sylibr 233 |
. . . . . . . 8
β’ (π β π β
β0) |
58 | | nn0fz0 13599 |
. . . . . . . 8
β’ (π β β0
β π β (0...π)) |
59 | 57, 58 | sylib 217 |
. . . . . . 7
β’ (π β π β (0...π)) |
60 | 48, 49, 59 | rspcdva 3614 |
. . . . . 6
β’ (π β (πβπ) = (πβπ)) |
61 | 14 | fveq1i 6893 |
. . . . . . . . . . 11
β’ (πβ(π + 1)) = ((π βͺ {β¨(π + 1), πΆβ©})β(π + 1)) |
62 | | ovex 7442 |
. . . . . . . . . . . 12
β’ (π + 1) β V |
63 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | wlkp1lem1 28930 |
. . . . . . . . . . . 12
β’ (π β Β¬ (π + 1) β dom π) |
64 | | fsnunfv 7185 |
. . . . . . . . . . . 12
β’ (((π + 1) β V β§ πΆ β π β§ Β¬ (π + 1) β dom π) β ((π βͺ {β¨(π + 1), πΆβ©})β(π + 1)) = πΆ) |
65 | 62, 6, 63, 64 | mp3an2i 1467 |
. . . . . . . . . . 11
β’ (π β ((π βͺ {β¨(π + 1), πΆβ©})β(π + 1)) = πΆ) |
66 | 61, 65 | eqtrid 2785 |
. . . . . . . . . 10
β’ (π β (πβ(π + 1)) = πΆ) |
67 | 66 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π β ((πβπ) = (πβ(π + 1)) β (πβπ) = πΆ)) |
68 | | eqcom 2740 |
. . . . . . . . 9
β’ ((πβπ) = πΆ β πΆ = (πβπ)) |
69 | 67, 68 | bitrdi 287 |
. . . . . . . 8
β’ (π β ((πβπ) = (πβ(π + 1)) β πΆ = (πβπ))) |
70 | | wlkp1.l |
. . . . . . . . . 10
β’ ((π β§ πΆ = (πβπ)) β πΈ = {πΆ}) |
71 | | sneq 4639 |
. . . . . . . . . . 11
β’ (πΆ = (πβπ) β {πΆ} = {(πβπ)}) |
72 | 71 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ πΆ = (πβπ)) β {πΆ} = {(πβπ)}) |
73 | 70, 72 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ πΆ = (πβπ)) β πΈ = {(πβπ)}) |
74 | 73 | ex 414 |
. . . . . . . 8
β’ (π β (πΆ = (πβπ) β πΈ = {(πβπ)})) |
75 | 69, 74 | sylbid 239 |
. . . . . . 7
β’ (π β ((πβπ) = (πβ(π + 1)) β πΈ = {(πβπ)})) |
76 | | eqeq1 2737 |
. . . . . . . 8
β’ ((πβπ) = (πβπ) β ((πβπ) = (πβ(π + 1)) β (πβπ) = (πβ(π + 1)))) |
77 | | sneq 4639 |
. . . . . . . . 9
β’ ((πβπ) = (πβπ) β {(πβπ)} = {(πβπ)}) |
78 | 77 | eqeq2d 2744 |
. . . . . . . 8
β’ ((πβπ) = (πβπ) β (πΈ = {(πβπ)} β πΈ = {(πβπ)})) |
79 | 76, 78 | imbi12d 345 |
. . . . . . 7
β’ ((πβπ) = (πβπ) β (((πβπ) = (πβ(π + 1)) β πΈ = {(πβπ)}) β ((πβπ) = (πβ(π + 1)) β πΈ = {(πβπ)}))) |
80 | 75, 79 | syl5ibrcom 246 |
. . . . . 6
β’ (π β ((πβπ) = (πβπ) β ((πβπ) = (πβ(π + 1)) β πΈ = {(πβπ)}))) |
81 | 60, 80 | mpd 15 |
. . . . 5
β’ (π β ((πβπ) = (πβ(π + 1)) β πΈ = {(πβπ)})) |
82 | 81 | imp 408 |
. . . 4
β’ ((π β§ (πβπ) = (πβ(π + 1))) β πΈ = {(πβπ)}) |
83 | 41, 45, 82 | 3eqtrd 2777 |
. . 3
β’ ((π β§ (πβπ) = (πβ(π + 1))) β ((iEdgβπ)β(π»βπ)) = {(πβπ)}) |
84 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | wlkp1lem7 28936 |
. . . 4
β’ (π β {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) |
85 | 84 | adantr 482 |
. . 3
β’ ((π β§ Β¬ (πβπ) = (πβ(π + 1))) β {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) |
86 | 83, 85 | ifpimpda 1082 |
. 2
β’ (π β if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ)))) |
87 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | wlkp1lem2 28931 |
. . . . . 6
β’ (π β (β―βπ») = (π + 1)) |
88 | 87 | oveq2d 7425 |
. . . . 5
β’ (π β (0..^(β―βπ»)) = (0..^(π + 1))) |
89 | | fzosplitsn 13740 |
. . . . . 6
β’ (π β
(β€β₯β0) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
90 | 56, 89 | syl 17 |
. . . . 5
β’ (π β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
91 | 88, 90 | eqtrd 2773 |
. . . 4
β’ (π β (0..^(β―βπ»)) = ((0..^π) βͺ {π})) |
92 | 91 | raleqdv 3326 |
. . 3
β’ (π β (βπ β
(0..^(β―βπ»))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β βπ β ((0..^π) βͺ {π})if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))))) |
93 | | ralunb 4192 |
. . . 4
β’
(βπ β
((0..^π) βͺ {π})if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β (βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β§ βπ β {π}if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))))) |
94 | 93 | a1i 11 |
. . 3
β’ (π β (βπ β ((0..^π) βͺ {π})if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β (βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β§ βπ β {π}if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ)))))) |
95 | 9 | fvexi 6906 |
. . . . 5
β’ π β V |
96 | | wkslem1 28864 |
. . . . . 6
β’ (π = π β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))))) |
97 | 96 | ralsng 4678 |
. . . . 5
β’ (π β V β (βπ β {π}if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))))) |
98 | 95, 97 | mp1i 13 |
. . . 4
β’ (π β (βπ β {π}if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))))) |
99 | 98 | anbi2d 630 |
. . 3
β’ (π β ((βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β§ βπ β {π}if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ)))) β (βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β§ if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ)))))) |
100 | 92, 94, 99 | 3bitrd 305 |
. 2
β’ (π β (βπ β
(0..^(β―βπ»))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β (βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ))) β§ if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ)))))) |
101 | 39, 86, 100 | mpbir2and 712 |
1
β’ (π β βπ β (0..^(β―βπ»))if-((πβπ) = (πβ(π + 1)), ((iEdgβπ)β(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπ)β(π»βπ)))) |