Step | Hyp | Ref
| Expression |
1 | | iswspthn 26736 |
. . 3
⊢ (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊)) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊))) |
3 | | wwlksnwwlksnon.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
4 | 3 | wwlksnwwlksnon 26810 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) |
5 | 4 | anbi1d 741 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊) ↔ (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊))) |
6 | | r19.41vv 3091 |
. . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊) ↔ (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊)) |
7 | 5, 6 | syl6bbr 278 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊))) |
8 | | 3anass 1042 |
. . . . . . . 8
⊢ ((𝑓(SPaths‘𝐺)𝑊 ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏) ↔ (𝑓(SPaths‘𝐺)𝑊 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → ((𝑓(SPaths‘𝐺)𝑊 ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏) ↔ (𝑓(SPaths‘𝐺)𝑊 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
10 | | simpr 477 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) |
11 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
12 | 11 | jctl 564 |
. . . . . . . 8
⊢ (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) → (𝑓 ∈ V ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) |
13 | 3 | isspthonpth 26645 |
. . . . . . . 8
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑓 ∈ V ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏))) → (𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊 ↔ (𝑓(SPaths‘𝐺)𝑊 ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
14 | 10, 12, 13 | syl2an 494 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊 ↔ (𝑓(SPaths‘𝐺)𝑊 ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
15 | | spthiswlk 26624 |
. . . . . . . . . 10
⊢ (𝑓(SPaths‘𝐺)𝑊 → 𝑓(Walks‘𝐺)𝑊) |
16 | | wlklenvm1 26517 |
. . . . . . . . . 10
⊢ (𝑓(Walks‘𝐺)𝑊 → (#‘𝑓) = ((#‘𝑊) − 1)) |
17 | 3 | wwlknon 26742 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏))) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏))) |
19 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (𝑊‘0) = 𝑎) |
20 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑓) =
((#‘𝑊) − 1))
→ (#‘𝑓) =
((#‘𝑊) −
1)) |
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (#‘𝑓) =
((#‘𝑊) −
1)) |
22 | | wwlknbp2 26752 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) |
23 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑊) =
(𝑁 + 1) →
((#‘𝑊) − 1) =
((𝑁 + 1) −
1)) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → ((#‘𝑊) − 1) = ((𝑁 + 1) − 1)) |
25 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
26 | | pncan1 10454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑓) =
((#‘𝑊) − 1))
→ ((𝑁 + 1) − 1)
= 𝑁) |
29 | 24, 28 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ ((#‘𝑊) −
1) = 𝑁) |
30 | 29 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1))
→ ((#‘𝑊) −
1) = 𝑁)) |
31 | 22, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1))
→ ((#‘𝑊) −
1) = 𝑁)) |
32 | 31 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1))
→ ((#‘𝑊) −
1) = 𝑁)) |
33 | 32 | imp 445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ ((#‘𝑊) −
1) = 𝑁) |
34 | 21, 33 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (#‘𝑓) = 𝑁) |
35 | 34 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (𝑊‘(#‘𝑓)) = (𝑊‘𝑁)) |
36 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (𝑊‘𝑁) = 𝑏) |
37 | 35, 36 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ (𝑊‘(#‘𝑓)) = 𝑏) |
38 | 19, 37 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑓) =
((#‘𝑊) − 1)))
→ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)) |
39 | 38 | exp32 631 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → (𝑁 ∈ ℕ0 →
((#‘𝑓) =
((#‘𝑊) − 1)
→ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
40 | 39 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
42 | 41 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑊‘0) = 𝑎 ∧ (𝑊‘𝑁) = 𝑏) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
43 | 18, 42 | sylbid 230 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
44 | 43 | imp 445 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → ((#‘𝑓) = ((#‘𝑊) − 1) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
45 | 44 | com12 32 |
. . . . . . . . . 10
⊢
((#‘𝑓) =
((#‘𝑊) − 1)
→ ((((𝑁 ∈
ℕ0 ∧ 𝐺
∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
46 | 15, 16, 45 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑓(SPaths‘𝐺)𝑊 → ((((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
47 | 46 | com12 32 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (𝑓(SPaths‘𝐺)𝑊 → ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏))) |
48 | 47 | pm4.71d 666 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (𝑓(SPaths‘𝐺)𝑊 ↔ (𝑓(SPaths‘𝐺)𝑊 ∧ ((𝑊‘0) = 𝑎 ∧ (𝑊‘(#‘𝑓)) = 𝑏)))) |
49 | 9, 14, 48 | 3bitr4rd 301 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (𝑓(SPaths‘𝐺)𝑊 ↔ 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊)) |
50 | 49 | exbidv 1850 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ 𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏)) → (∃𝑓 𝑓(SPaths‘𝐺)𝑊 ↔ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊)) |
51 | 50 | pm5.32da 673 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊) ↔ (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊))) |
52 | 3 | wspthnon 26743 |
. . . . 5
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏) ↔ (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊))) |
53 | 52 | adantl 482 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏) ↔ (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑊))) |
54 | 51, 53 | bitr4d 271 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊) ↔ 𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏))) |
55 | 54 | 2rexbidva 3056 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∧ ∃𝑓 𝑓(SPaths‘𝐺)𝑊) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏))) |
56 | 2, 7, 55 | 3bitrd 294 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐺 ∈ 𝑈) → (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑊 ∈ (𝑎(𝑁 WSPathsNOn 𝐺)𝑏))) |