Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wwlk Structured version   Visualization version   Unicode version

Definition df-wwlk 25400
 Description: Define the set of all Walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlk 25229. has to be excluded because a walk always consists of at least one vertex, see wlkn0 25248. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
Assertion
Ref Expression
df-wwlk WWalks Word ..^
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-wwlk
StepHypRef Expression
1 cwwlk 25398 . 2 WWalks
2 vv . . 3
3 ve . . 3
4 cvv 3044 . . 3
5 vw . . . . . . 7
65cv 1442 . . . . . 6
7 c0 3730 . . . . . 6
86, 7wne 2621 . . . . 5
9 vi . . . . . . . . . 10
109cv 1442 . . . . . . . . 9
1110, 6cfv 5581 . . . . . . . 8
12 c1 9537 . . . . . . . . . 10
13 caddc 9539 . . . . . . . . . 10
1410, 12, 13co 6288 . . . . . . . . 9
1514, 6cfv 5581 . . . . . . . 8
1611, 15cpr 3969 . . . . . . 7
173cv 1442 . . . . . . . 8
1817crn 4834 . . . . . . 7
1916, 18wcel 1886 . . . . . 6
20 cc0 9536 . . . . . . 7
21 chash 12512 . . . . . . . . 9
226, 21cfv 5581 . . . . . . . 8
23 cmin 9857 . . . . . . . 8
2422, 12, 23co 6288 . . . . . . 7
25 cfzo 11912 . . . . . . 7 ..^
2620, 24, 25co 6288 . . . . . 6 ..^
2719, 9, 26wral 2736 . . . . 5 ..^
288, 27wa 371 . . . 4 ..^
292cv 1442 . . . . 5
3029cword 12653 . . . 4 Word
3128, 5, 30crab 2740 . . 3 Word ..^
322, 3, 4, 4, 31cmpt2 6290 . 2 Word ..^
331, 32wceq 1443 1 WWalks Word ..^
 Colors of variables: wff setvar class This definition is referenced by:  wwlk  25402  wwlkprop  25406
 Copyright terms: Public domain W3C validator