Description: A walk of length N as word corresponds to the sequence of vertices in a walk of length N in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018) (Revised by AV, 12-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wlklnwwlkln2 | |- ( G e. USPGraph -> ( P e. ( N WWalksN G ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wlkiswwlks2 | |- ( G e. USPGraph -> ( P e. ( WWalks ` G ) -> E. f f ( Walks ` G ) P ) ) |
|
| 2 | 1 | wlklnwwlkln2lem | |- ( G e. USPGraph -> ( P e. ( N WWalksN G ) -> E. f ( f ( Walks ` G ) P /\ ( # ` f ) = N ) ) ) |