:: Walks in a Graph
:: by Gilbert Lee
::
:: Copyright (c) 2005-2021 Association of Mizar Users

theorem Th1: :: GLIB_001:1
for x, y being odd Element of NAT holds
( x < y iff x + 2 <= y )
proof end;

theorem :: GLIB_001:2
canceled;

::$CT theorem Th2: :: GLIB_001:3 for X being set for fs being FinSequence of X for fss being Subset of fs holds len (Seq fss) <= len fs proof end; theorem Th3: :: GLIB_001:4 for X being set for fs being FinSequence of X for fss being Subset of fs for m being Element of NAT st m in dom (Seq fss) holds ex n being Element of NAT st ( n in dom fs & m <= n & (Seq fss) . m = fs . n ) proof end; theorem Th4: :: GLIB_001:5 for X being set for fs being FinSequence of X for fss being Subset of fs holds len (Seq fss) = card fss proof end; theorem Th5: :: GLIB_001:6 for X being set for fs being FinSequence of X for fss being Subset of fs holds dom (Seq fss) = dom (Sgm (dom fss)) proof end; definition let G be _Graph; mode VertexSeq of G -> FinSequence of the_Vertices_of G means :Def1: :: GLIB_001:def 1 for n being Element of NAT st 1 <= n & n < len it holds ex e being set st e Joins it . n,it . (n + 1),G; existence ex b1 being FinSequence of the_Vertices_of G st for n being Element of NAT st 1 <= n & n < len b1 holds ex e being set st e Joins b1 . n,b1 . (n + 1),G proof end; end; :: deftheorem Def1 defines VertexSeq GLIB_001:def 1 : for G being _Graph for b2 being FinSequence of the_Vertices_of G holds ( b2 is VertexSeq of G iff for n being Element of NAT st 1 <= n & n < len b2 holds ex e being set st e Joins b2 . n,b2 . (n + 1),G ); definition let G be _Graph; mode EdgeSeq of G -> FinSequence of the_Edges_of G means :Def2: :: GLIB_001:def 2 ex vs being FinSequence of the_Vertices_of G st ( len vs = (len it) + 1 & ( for n being Element of NAT st 1 <= n & n <= len it holds it . n Joins vs . n,vs . (n + 1),G ) ); existence ex b1 being FinSequence of the_Edges_of G ex vs being FinSequence of the_Vertices_of G st ( len vs = (len b1) + 1 & ( for n being Element of NAT st 1 <= n & n <= len b1 holds b1 . n Joins vs . n,vs . (n + 1),G ) ) proof end; end; :: deftheorem Def2 defines EdgeSeq GLIB_001:def 2 : for G being _Graph for b2 being FinSequence of the_Edges_of G holds ( b2 is EdgeSeq of G iff ex vs being FinSequence of the_Vertices_of G st ( len vs = (len b2) + 1 & ( for n being Element of NAT st 1 <= n & n <= len b2 holds b2 . n Joins vs . n,vs . (n + 1),G ) ) ); definition let G be _Graph; mode Walk of G -> FinSequence of () \/ () means :Def3: :: GLIB_001:def 3 ( len it is odd & it . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len it holds it . (n + 1) Joins it . n,it . (n + 2),G ) ); existence ex b1 being FinSequence of () \/ () st ( len b1 is odd & b1 . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len b1 holds b1 . (n + 1) Joins b1 . n,b1 . (n + 2),G ) ) proof end; end; :: deftheorem Def3 defines Walk GLIB_001:def 3 : for G being _Graph for b2 being FinSequence of () \/ () holds ( b2 is Walk of G iff ( len b2 is odd & b2 . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len b2 holds b2 . (n + 1) Joins b2 . n,b2 . (n + 2),G ) ) ); registration let G be _Graph; let W be Walk of G; cluster card W -> non empty odd ; correctness coherence ( not len W is even & not len W is empty ) ; proof end; end; definition let G be _Graph; let v be Vertex of G; func G .walkOf v -> Walk of G equals :: GLIB_001:def 4 <*v*>; coherence <*v*> is Walk of G proof end; end; :: deftheorem defines .walkOf GLIB_001:def 4 : for G being _Graph for v being Vertex of G holds G .walkOf v = <*v*>; definition let G be _Graph; let x, y, e be object ; func G .walkOf (x,e,y) -> Walk of G equals :Def5: :: GLIB_001:def 5 <*x,e,y*> if e Joins x,y,G otherwise G .walkOf the Element of the_Vertices_of G; coherence ( ( e Joins x,y,G implies <*x,e,y*> is Walk of G ) & ( not e Joins x,y,G implies G .walkOf the Element of the_Vertices_of G is Walk of G ) ) proof end; consistency for b1 being Walk of G holds verum ; end; :: deftheorem Def5 defines .walkOf GLIB_001:def 5 : for G being _Graph for x, y, e being object holds ( ( e Joins x,y,G implies G .walkOf (x,e,y) = <*x,e,y*> ) & ( not e Joins x,y,G implies G .walkOf (x,e,y) = G .walkOf the Element of the_Vertices_of G ) ); definition let G be _Graph; let W be Walk of G; func W .first() -> Vertex of G equals :: GLIB_001:def 6 W . 1; coherence W . 1 is Vertex of G by Def3; func W .last() -> Vertex of G equals :: GLIB_001:def 7 W . (len W); coherence W . (len W) is Vertex of G proof end; end; :: deftheorem defines .first() GLIB_001:def 6 : for G being _Graph for W being Walk of G holds W .first() = W . 1; :: deftheorem defines .last() GLIB_001:def 7 : for G being _Graph for W being Walk of G holds W .last() = W . (len W); definition let G be _Graph; let W be Walk of G; let n be Nat; func W .vertexAt n -> Vertex of G equals :Def8: :: GLIB_001:def 8 W . n if ( n is odd & n <= len W ) otherwise W .first() ; correctness coherence ( ( n is odd & n <= len W implies W . n is Vertex of G ) & ( ( not n is odd or not n <= len W ) implies W .first() is Vertex of G ) ) ; consistency for b1 being Vertex of G holds verum ; proof end; end; :: deftheorem Def8 defines .vertexAt GLIB_001:def 8 : for G being _Graph for W being Walk of G for n being Nat holds ( ( n is odd & n <= len W implies W .vertexAt n = W . n ) & ( ( not n is odd or not n <= len W ) implies W .vertexAt n = W .first() ) ); definition let G be _Graph; let W be Walk of G; func W .reverse() -> Walk of G equals :: GLIB_001:def 9 Rev W; coherence Rev W is Walk of G proof end; involutiveness for b1, b2 being Walk of G st b1 = Rev b2 holds b2 = Rev b1 ; end; :: deftheorem defines .reverse() GLIB_001:def 9 : for G being _Graph for W being Walk of G holds W .reverse() = Rev W; definition let G be _Graph; let W1, W2 be Walk of G; func W1 .append W2 -> Walk of G equals :Def10: :: GLIB_001:def 10 W1 ^' W2 if W1 .last() = W2 .first() otherwise W1; correctness coherence ( ( W1 .last() = W2 .first() implies W1 ^' W2 is Walk of G ) & ( not W1 .last() = W2 .first() implies W1 is Walk of G ) ) ; consistency for b1 being Walk of G holds verum ; proof end; end; :: deftheorem Def10 defines .append GLIB_001:def 10 : for G being _Graph for W1, W2 being Walk of G holds ( ( W1 .last() = W2 .first() implies W1 .append W2 = W1 ^' W2 ) & ( not W1 .last() = W2 .first() implies W1 .append W2 = W1 ) ); definition let G be _Graph; let W be Walk of G; let m, n be Nat; func W .cut (m,n) -> Walk of G equals :Def11: :: GLIB_001:def 11 (m,n) -cut W if ( m is odd & n is odd & m <= n & n <= len W ) otherwise W; correctness coherence ( ( m is odd & n is odd & m <= n & n <= len W implies (m,n) -cut W is Walk of G ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W is Walk of G ) ) ; consistency for b1 being Walk of G holds verum ; proof end; end; :: deftheorem Def11 defines .cut GLIB_001:def 11 : for G being _Graph for W being Walk of G for m, n being Nat holds ( ( m is odd & n is odd & m <= n & n <= len W implies W .cut (m,n) = (m,n) -cut W ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W .cut (m,n) = W ) ); definition let G be _Graph; let W be Walk of G; let m, n be Element of NAT ; func W .remove (m,n) -> Walk of G equals :Def12: :: GLIB_001:def 12 (W .cut (1,m)) .append (W .cut (n,(len W))) if ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) otherwise W; correctness coherence ( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n implies (W .cut (1,m)) .append (W .cut (n,(len W))) is Walk of G ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) implies W is Walk of G ) ) ; consistency for b1 being Walk of G holds verum ; ; end; :: deftheorem Def12 defines .remove GLIB_001:def 12 : for G being _Graph for W being Walk of G for m, n being Element of NAT holds ( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n implies W .remove (m,n) = (W .cut (1,m)) .append (W .cut (n,(len W))) ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) implies W .remove (m,n) = W ) ); definition let G be _Graph; let W be Walk of G; let e be object ; func W .addEdge e -> Walk of G equals :: GLIB_001:def 13 W .append (G .walkOf ((),e,(() .adj e))); coherence W .append (G .walkOf ((),e,(() .adj e))) is Walk of G ; end; :: deftheorem defines .addEdge GLIB_001:def 13 : for G being _Graph for W being Walk of G for e being object holds W .addEdge e = W .append (G .walkOf ((),e,(() .adj e))); definition let G be _Graph; let W be Walk of G; func W .vertexSeq() -> VertexSeq of G means :Def14: :: GLIB_001:def 14 ( (len W) + 1 = 2 * (len it) & ( for n being Nat st 1 <= n & n <= len it holds it . n = W . ((2 * n) - 1) ) ); existence ex b1 being VertexSeq of G st ( (len W) + 1 = 2 * (len b1) & ( for n being Nat st 1 <= n & n <= len b1 holds b1 . n = W . ((2 * n) - 1) ) ) proof end; uniqueness for b1, b2 being VertexSeq of G st (len W) + 1 = 2 * (len b1) & ( for n being Nat st 1 <= n & n <= len b1 holds b1 . n = W . ((2 * n) - 1) ) & (len W) + 1 = 2 * (len b2) & ( for n being Nat st 1 <= n & n <= len b2 holds b2 . n = W . ((2 * n) - 1) ) holds b1 = b2 proof end; end; :: deftheorem Def14 defines .vertexSeq() GLIB_001:def 14 : for G being _Graph for W being Walk of G for b3 being VertexSeq of G holds ( b3 = W .vertexSeq() iff ( (len W) + 1 = 2 * (len b3) & ( for n being Nat st 1 <= n & n <= len b3 holds b3 . n = W . ((2 * n) - 1) ) ) ); definition let G be _Graph; let W be Walk of G; func W .edgeSeq() -> EdgeSeq of G means :Def15: :: GLIB_001:def 15 ( len W = (2 * (len it)) + 1 & ( for n being Nat st 1 <= n & n <= len it holds it . n = W . (2 * n) ) ); existence ex b1 being EdgeSeq of G st ( len W = (2 * (len b1)) + 1 & ( for n being Nat st 1 <= n & n <= len b1 holds b1 . n = W . (2 * n) ) ) proof end; uniqueness for b1, b2 being EdgeSeq of G st len W = (2 * (len b1)) + 1 & ( for n being Nat st 1 <= n & n <= len b1 holds b1 . n = W . (2 * n) ) & len W = (2 * (len b2)) + 1 & ( for n being Nat st 1 <= n & n <= len b2 holds b2 . n = W . (2 * n) ) holds b1 = b2 proof end; end; :: deftheorem Def15 defines .edgeSeq() GLIB_001:def 15 : for G being _Graph for W being Walk of G for b3 being EdgeSeq of G holds ( b3 = W .edgeSeq() iff ( len W = (2 * (len b3)) + 1 & ( for n being Nat st 1 <= n & n <= len b3 holds b3 . n = W . (2 * n) ) ) ); definition let G be _Graph; let W be Walk of G; func W .vertices() -> finite Subset of () equals :: GLIB_001:def 16 rng (); coherence rng () is finite Subset of () ; end; :: deftheorem defines .vertices() GLIB_001:def 16 : for G being _Graph for W being Walk of G holds W .vertices() = rng (); definition let G be _Graph; let W be Walk of G; func W .edges() -> finite Subset of () equals :: GLIB_001:def 17 rng (); coherence rng () is finite Subset of () ; end; :: deftheorem defines .edges() GLIB_001:def 17 : for G being _Graph for W being Walk of G holds W .edges() = rng (); definition let G be _Graph; let W be Walk of G; func W .length() -> Element of NAT equals :: GLIB_001:def 18 len (); coherence len () is Element of NAT ; end; :: deftheorem defines .length() GLIB_001:def 18 : for G being _Graph for W being Walk of G holds W .length() = len (); definition let G be _Graph; let W be Walk of G; let v be set ; func W .find v -> odd Element of NAT means :Def19: :: GLIB_001:def 19 ( it <= len W & W . it = v & ( for n being odd Nat st n <= len W & W . n = v holds it <= n ) ) if v in W .vertices() otherwise it = len W; existence ( ( v in W .vertices() implies ex b1 being odd Element of NAT st ( b1 <= len W & W . b1 = v & ( for n being odd Nat st n <= len W & W . n = v holds b1 <= n ) ) ) & ( not v in W .vertices() implies ex b1 being odd Element of NAT st b1 = len W ) ) proof end; uniqueness for b1, b2 being odd Element of NAT holds ( ( v in W .vertices() & b1 <= len W & W . b1 = v & ( for n being odd Nat st n <= len W & W . n = v holds b1 <= n ) & b2 <= len W & W . b2 = v & ( for n being odd Nat st n <= len W & W . n = v holds b2 <= n ) implies b1 = b2 ) & ( not v in W .vertices() & b1 = len W & b2 = len W implies b1 = b2 ) ) proof end; consistency for b1 being odd Element of NAT holds verum ; end; :: deftheorem Def19 defines .find GLIB_001:def 19 : for G being _Graph for W being Walk of G for v being set for b4 being odd Element of NAT holds ( ( v in W .vertices() implies ( b4 = W .find v iff ( b4 <= len W & W . b4 = v & ( for n being odd Nat st n <= len W & W . n = v holds b4 <= n ) ) ) ) & ( not v in W .vertices() implies ( b4 = W .find v iff b4 = len W ) ) ); definition let G be _Graph; let W be Walk of G; let n be Element of NAT ; func W .find n -> odd Element of NAT means :Def20: :: GLIB_001:def 20 ( it <= len W & W . it = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds it <= k ) ) if ( n is odd & n <= len W ) otherwise it = len W; existence ( ( n is odd & n <= len W implies ex b1 being odd Element of NAT st ( b1 <= len W & W . b1 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds b1 <= k ) ) ) & ( ( not n is odd or not n <= len W ) implies ex b1 being odd Element of NAT st b1 = len W ) ) proof end; uniqueness for b1, b2 being odd Element of NAT holds ( ( n is odd & n <= len W & b1 <= len W & W . b1 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds b1 <= k ) & b2 <= len W & W . b2 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds b2 <= k ) implies b1 = b2 ) & ( ( not n is odd or not n <= len W ) & b1 = len W & b2 = len W implies b1 = b2 ) ) proof end; consistency for b1 being odd Element of NAT holds verum ; end; :: deftheorem Def20 defines .find GLIB_001:def 20 : for G being _Graph for W being Walk of G for n being Element of NAT for b4 being odd Element of NAT holds ( ( n is odd & n <= len W implies ( b4 = W .find n iff ( b4 <= len W & W . b4 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds b4 <= k ) ) ) ) & ( ( not n is odd or not n <= len W ) implies ( b4 = W .find n iff b4 = len W ) ) ); definition let G be _Graph; let W be Walk of G; let v be set ; func W .rfind v -> odd Element of NAT means :Def21: :: GLIB_001:def 21 ( it <= len W & W . it = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds n <= it ) ) if v in W .vertices() otherwise it = len W; existence ( ( v in W .vertices() implies ex b1 being odd Element of NAT st ( b1 <= len W & W . b1 = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds n <= b1 ) ) ) & ( not v in W .vertices() implies ex b1 being odd Element of NAT st b1 = len W ) ) proof end; uniqueness for b1, b2 being odd Element of NAT holds ( ( v in W .vertices() & b1 <= len W & W . b1 = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds n <= b1 ) & b2 <= len W & W . b2 = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds n <= b2 ) implies b1 = b2 ) & ( not v in W .vertices() & b1 = len W & b2 = len W implies b1 = b2 ) ) proof end; consistency for b1 being odd Element of NAT holds verum ; end; :: deftheorem Def21 defines .rfind GLIB_001:def 21 : for G being _Graph for W being Walk of G for v being set for b4 being odd Element of NAT holds ( ( v in W .vertices() implies ( b4 = W .rfind v iff ( b4 <= len W & W . b4 = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds n <= b4 ) ) ) ) & ( not v in W .vertices() implies ( b4 = W .rfind v iff b4 = len W ) ) ); definition let G be _Graph; let W be Walk of G; let n be Element of NAT ; func W .rfind n -> odd Element of NAT means :Def22: :: GLIB_001:def 22 ( it <= len W & W . it = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds k <= it ) ) if ( n is odd & n <= len W ) otherwise it = len W; existence ( ( n is odd & n <= len W implies ex b1 being odd Element of NAT st ( b1 <= len W & W . b1 = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds k <= b1 ) ) ) & ( ( not n is odd or not n <= len W ) implies ex b1 being odd Element of NAT st b1 = len W ) ) proof end; uniqueness for b1, b2 being odd Element of NAT holds ( ( n is odd & n <= len W & b1 <= len W & W . b1 = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds k <= b1 ) & b2 <= len W & W . b2 = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds k <= b2 ) implies b1 = b2 ) & ( ( not n is odd or not n <= len W ) & b1 = len W & b2 = len W implies b1 = b2 ) ) proof end; consistency for b1 being odd Element of NAT holds verum ; end; :: deftheorem Def22 defines .rfind GLIB_001:def 22 : for G being _Graph for W being Walk of G for n being Element of NAT for b4 being odd Element of NAT holds ( ( n is odd & n <= len W implies ( b4 = W .rfind n iff ( b4 <= len W & W . b4 = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds k <= b4 ) ) ) ) & ( ( not n is odd or not n <= len W ) implies ( b4 = W .rfind n iff b4 = len W ) ) ); definition let G be _Graph; let u, v be object ; let W be Walk of G; pred W is_Walk_from u,v means :: GLIB_001:def 23 ( W .first() = u & W .last() = v ); end; :: deftheorem defines is_Walk_from GLIB_001:def 23 : for G being _Graph for u, v being object for W being Walk of G holds ( W is_Walk_from u,v iff ( W .first() = u & W .last() = v ) ); definition let G be _Graph; let W be Walk of G; attr W is closed means :Def24: :: GLIB_001:def 24 W .first() = W .last() ; attr W is directed means :Def25: :: GLIB_001:def 25 for n being odd Element of NAT st n < len W holds () . (W . (n + 1)) = W . n; :: original: trivial redefine attr W is trivial means :: GLIB_001:def 26 W .length() = 0 ; compatibility ( W is trivial iff W .length() = 0 ) proof end; attr W is Trail-like means :Def27: :: GLIB_001:def 27 W .edgeSeq() is one-to-one ; end; :: deftheorem Def24 defines closed GLIB_001:def 24 : for G being _Graph for W being Walk of G holds ( W is closed iff W .first() = W .last() ); :: deftheorem Def25 defines directed GLIB_001:def 25 : for G being _Graph for W being Walk of G holds ( W is directed iff for n being odd Element of NAT st n < len W holds () . (W . (n + 1)) = W . n ); :: deftheorem defines trivial GLIB_001:def 26 : for G being _Graph for W being Walk of G holds ( W is trivial iff W .length() = 0 ); :: deftheorem Def27 defines Trail-like GLIB_001:def 27 : for G being _Graph for W being Walk of G holds ( W is Trail-like iff W .edgeSeq() is one-to-one ); notation let G be _Graph; let W be Walk of G; antonym open W for closed ; end; definition let G be _Graph; let W be Walk of G; attr W is Path-like means :Def28: :: GLIB_001:def 28 ( W is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len W & W . m = W . n holds ( m = 1 & n = len W ) ) ); end; :: deftheorem Def28 defines Path-like GLIB_001:def 28 : for G being _Graph for W being Walk of G holds ( W is Path-like iff ( W is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len W & W . m = W . n holds ( m = 1 & n = len W ) ) ) ); definition let G be _Graph; let W be Walk of G; attr W is vertex-distinct means :Def29: :: GLIB_001:def 29 for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds m = n; end; :: deftheorem Def29 defines vertex-distinct GLIB_001:def 29 : for G being _Graph for W being Walk of G holds ( W is vertex-distinct iff for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds m = n ); definition let G be _Graph; let W be Walk of G; attr W is Circuit-like means :: GLIB_001:def 30 ( W is closed & W is Trail-like & W is V5() ); attr W is Cycle-like means :: GLIB_001:def 31 ( W is closed & W is Path-like & W is V5() ); end; :: deftheorem defines Circuit-like GLIB_001:def 30 : for G being _Graph for W being Walk of G holds ( W is Circuit-like iff ( W is closed & W is Trail-like & W is V5() ) ); :: deftheorem defines Cycle-like GLIB_001:def 31 : for G being _Graph for W being Walk of G holds ( W is Cycle-like iff ( W is closed & W is Path-like & W is V5() ) ); Lm1: for G being _Graph for W being Walk of G for n being odd Element of NAT st n <= len W holds W . n in the_Vertices_of G proof end; Lm2: for G being _Graph for W being Walk of G for n being even Element of NAT st n in dom W holds ex naa1 being odd Element of NAT st ( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G ) proof end; Lm3: for G being _Graph for W being Walk of G for n being odd Element of NAT st n < len W holds ( n in dom W & n + 1 in dom W & n + 2 in dom W ) proof end; Lm4: for G being _Graph for v being Vertex of G holds ( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is V5() & G .walkOf v is Trail-like & G .walkOf v is Path-like ) proof end; Lm5: for G being _Graph for x, e, y being object st e Joins x,y,G holds len (G .walkOf (x,e,y)) = 3 proof end; Lm6: for G being _Graph for x, e, y being object st e Joins x,y,G holds ( (G .walkOf (x,e,y)) .first() = x & (G .walkOf (x,e,y)) .last() = y & G .walkOf (x,e,y) is_Walk_from x,y ) proof end; Lm7: for G being _Graph for W being Walk of G holds ( W .first() = () .last() & W .last() = () .first() ) proof end; Lm8: for G being _Graph for W being Walk of G for n being Element of NAT st n in dom () holds ( () . n = W . (((len W) - n) + 1) & ((len W) - n) + 1 in dom W ) proof end; Lm9: for G being _Graph for W1, W2 being Walk of G st W1 .last() = W2 .first() holds (len (W1 .append W2)) + 1 = (len W1) + (len W2) proof end; Lm10: for G being _Graph for W1, W2 being Walk of G st W1 .last() = W2 .first() holds ( len W1 <= len (W1 .append W2) & len W2 <= len (W1 .append W2) ) proof end; Lm11: for G being _Graph for W1, W2 being Walk of G st W1 .last() = W2 .first() holds ( (W1 .append W2) .first() = W1 .first() & (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() ) proof end; Lm12: for G being _Graph for W1, W2 being Walk of G for n being Element of NAT st n in dom W1 holds ( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) proof end; Lm13: for G being _Graph for W1, W2 being Walk of G st W1 .last() = W2 .first() holds for n being Element of NAT st n < len W2 holds ( (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) & (len W1) + n in dom (W1 .append W2) ) proof end; Lm14: for G being _Graph for W1, W2 being Walk of G for n being Element of NAT holds ( not n in dom (W1 .append W2) or n in dom W1 or ex k being Element of NAT st ( k < len W2 & n = (len W1) + k ) ) proof end; Lm15: for G being _Graph for W being Walk of G for m, n being odd Element of NAT st m <= n & n <= len W holds ( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of NAT st i < len (W .cut (m,n)) holds ( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W ) ) ) proof end; Lm16: for G being _Graph for W being Walk of G for m, n being odd Element of NAT st m <= n & n <= len W holds ( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n ) proof end; Lm17: for G being _Graph for W being Walk of G for m, n, o being odd Element of NAT st m <= n & n <= o & o <= len W holds (W .cut (m,n)) .append (W .cut (n,o)) = W .cut (m,o) proof end; Lm18: for G being _Graph for W being Walk of G holds W .cut (1,(len W)) = W proof end; Lm19: for G being _Graph for W being Walk of G for n being odd Element of NAT st n <= len W holds W .cut (n,n) = <*()*> proof end; Lm20: for G being _Graph for W being Walk of G for m, n being Element of NAT st m is odd & m <= n holds (W .cut (1,n)) .cut (1,m) = W .cut (1,m) proof end; Lm21: for G being _Graph for W1, W2 being Walk of G for m, n being odd Element of NAT st m <= n & n <= len W1 & W1 .last() = W2 .first() holds (W1 .append W2) .cut (m,n) = W1 .cut (m,n) proof end; Lm22: for G being _Graph for W being Walk of G for m being odd Element of NAT st m <= len W holds len (W .cut (1,m)) = m proof end; Lm23: for G being _Graph for W being Walk of G for m being odd Element of NAT for x being Element of NAT st x in dom (W .cut (1,m)) & m <= len W holds (W .cut (1,m)) . x = W . x proof end; Lm24: for G being _Graph for W being Walk of G for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds (len (W .remove (m,n))) + n = (len W) + m proof end; Lm25: for G being _Graph for W being Walk of G for m, n being Element of NAT for x, y being set st W is_Walk_from x,y holds W .remove (m,n) is_Walk_from x,y proof end; Lm26: for G being _Graph for W being Walk of G for m, n being Element of NAT holds len (W .remove (m,n)) <= len W proof end; Lm27: for G being _Graph for W being Walk of G for m being Element of NAT holds W .remove (m,m) = W proof end; Lm28: for G being _Graph for W being Walk of G for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds (W .cut (1,m)) .last() = (W .cut (n,(len W))) .first() proof end; Lm29: for G being _Graph for W being Walk of G for x, y being set for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds for x being Element of NAT st x in Seg m holds (W .remove (m,n)) . x = W . x proof end; Lm30: for G being _Graph for W being Walk of G for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds ( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W ) proof end; Lm31: for G being _Graph for W being Walk of G for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds len (W .remove (m,n)) = ((len W) + m) - n proof end; Lm32: for G being _Graph for W being Walk of G for m being Element of NAT st W .first() = W . m holds W .remove (1,m) = W .cut (m,(len W)) proof end; Lm33: for G being _Graph for W being Walk of G for m, n being Element of NAT holds ( (W .remove (m,n)) .first() = W .first() & (W .remove (m,n)) .last() = W .last() ) proof end; Lm34: for G being _Graph for W being Walk of G for m, n being odd Element of NAT for x being Element of NAT holds ( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) ) proof end; Lm35: for G being _Graph for W being Walk of G for e, x being object st e Joins W .last() ,x,G holds W .addEdge e = W ^ <*e,x*> proof end; Lm36: for G being _Graph for W being Walk of G for e, x being object st e Joins W .last() ,x,G holds ( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x ) proof end; Lm37: for G being _Graph for W being Walk of G for e, x being object st e Joins W .last() ,x,G holds len (W .addEdge e) = (len W) + 2 proof end; Lm38: for G being _Graph for W being Walk of G for e, x being object st e Joins W .last() ,x,G holds ( (W .addEdge e) . ((len W) + 1) = e & (W .addEdge e) . ((len W) + 2) = x & ( for n being Element of NAT st n in dom W holds (W .addEdge e) . n = W . n ) ) proof end; Lm39: for G being _Graph for W being Walk of G for e, x, y, z being object st W is_Walk_from x,y & e Joins y,z,G holds W .addEdge e is_Walk_from x,z by Lm36; Lm40: for G being _Graph for W being Walk of G for n being even Nat st 1 <= n & n <= len W holds ( n div 2 in dom () & W . n = () . (n div 2) ) proof end; Lm41: for G being _Graph for W being Walk of G for n being Nat holds ( n in dom () iff 2 * n in dom W ) proof end; Lm42: for G being _Graph for W being Walk of G ex lenWaa1 being even Element of NAT st ( lenWaa1 = (len W) - 1 & len () = lenWaa1 div 2 ) proof end; Lm43: for G being _Graph for W being Walk of G for n being Element of NAT holds (W .cut (1,n)) .edgeSeq() c= W .edgeSeq() proof end; Lm44: for G being _Graph for W being Walk of G for e, x being object st e Joins W .last() ,x,G holds (W .addEdge e) .edgeSeq() = () ^ <*e*> proof end; Lm45: for G being _Graph for W being Walk of G for x being set holds ( x in W .vertices() iff ex n being odd Element of NAT st ( n <= len W & W . n = x ) ) proof end; Lm46: for G being _Graph for W being Walk of G for e being set holds ( e in W .edges() iff ex n being even Element of NAT st ( 1 <= n & n <= len W & W . n = e ) ) proof end; Lm47: for G being _Graph for W being Walk of G for e being set st e in W .edges() holds ex v1, v2 being Vertex of G ex n being odd Element of NAT st ( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G ) proof end; Lm48: for G being _Graph for W being Walk of G for e, x, y being object st e in W .edges() & e Joins x,y,G holds ( x in W .vertices() & y in W .vertices() ) proof end; Lm49: for G being _Graph for W being Walk of G for n being odd Element of NAT st n <= len W holds W .find n <= n proof end; Lm50: for G being _Graph for W being Walk of G for n being odd Element of NAT st n <= len W holds W .rfind n >= n proof end; Lm51: for G being _Graph for W being Walk of G holds ( W is directed iff for n being odd Element of NAT st n < len W holds W . (n + 1) DJoins W . n,W . (n + 2),G ) proof end; Lm52: for G being _Graph for W being Walk of G for x, e, y, z being set st W is directed & W is_Walk_from x,y & e DJoins y,z,G holds ( W .addEdge e is directed & W .addEdge e is_Walk_from x,z ) proof end; Lm53: for G being _Graph for W being Walk of G for m, n being Element of NAT st W is directed holds W .cut (m,n) is directed proof end; Lm54: for G being _Graph for W being Walk of G holds ( W is V5() iff 3 <= len W ) proof end; Lm55: for G being _Graph for W being Walk of G holds ( W is V5() iff len W <> 1 ) proof end; Lm56: for G being _Graph for W being Walk of G holds ( W is V5() iff ex v being Vertex of G st W = G .walkOf v ) proof end; Lm57: for G being _Graph for W being Walk of G holds ( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds W . m <> W . n ) proof end; Lm58: for G being _Graph for W being Walk of G holds ( W is Trail-like iff W .reverse() is Trail-like ) proof end; Lm59: for G being _Graph for W being Walk of G for m, n being Element of NAT st W is Trail-like holds W .cut (m,n) is Trail-like proof end; Lm60: for G being _Graph for W being Walk of G for e being set st W is Trail-like & e in () .edgesInOut() & not e in W .edges() holds W .addEdge e is Trail-like proof end; Lm61: for G being _Graph for W being Walk of G st len W <= 3 holds W is Trail-like proof end; Lm62: for G being _Graph for x, e, y being object st e Joins x,y,G holds G .walkOf (x,e,y) is Path-like proof end; Lm63: for G being _Graph for W being Walk of G holds ( W is Path-like iff W .reverse() is Path-like ) proof end; Lm64: for G being _Graph for W being Walk of G for m, n being Element of NAT st W is Path-like holds W .cut (m,n) is Path-like proof end; Lm65: for G being _Graph for W being Walk of G for e, v being object st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( not W is V5() or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds W . n <> v ) holds W .addEdge e is Path-like proof end; Lm66: for G being _Graph for W being Walk of G st ( for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds m = n ) holds W is Path-like proof end; Lm67: for G being _Graph for W being Walk of G st ( for n being odd Element of NAT st n <= len W holds W .rfind n = n ) holds W is Path-like proof end; Lm68: for G being _Graph for W being Walk of G for e, v being object st e Joins W .last() ,v,G & W is Path-like & not v in W .vertices() & ( not W is V5() or W is open ) holds W .addEdge e is Path-like proof end; Lm69: for G being _Graph for W being Walk of G st len W <= 3 holds W is Path-like proof end; registration let G be _Graph; cluster Path-like -> Trail-like for Walk of G; correctness coherence for b1 being Walk of G st b1 is Path-like holds b1 is Trail-like ; ; cluster V5() -> Path-like for Walk of G; correctness coherence for b1 being Walk of G st b1 is V5() holds b1 is Path-like ; proof end; cluster V5() -> vertex-distinct for Walk of G; coherence for b1 being Walk of G st b1 is V5() holds b1 is vertex-distinct proof end; cluster vertex-distinct -> Path-like for Walk of G; coherence for b1 being Walk of G st b1 is vertex-distinct holds b1 is Path-like by Lm66; cluster Circuit-like -> V5() closed Trail-like for Walk of G; correctness coherence for b1 being Walk of G st b1 is Circuit-like holds ( b1 is closed & b1 is Trail-like & b1 is V5() ) ; ; cluster Cycle-like -> V5() closed Path-like for Walk of G; correctness coherence for b1 being Walk of G st b1 is Cycle-like holds ( b1 is closed & b1 is Path-like & b1 is V5() ) ; ; end; registration let G be _Graph; existence ex b1 being Walk of G st ( b1 is closed & b1 is directed & b1 is V5() ) proof end; end; registration let G be _Graph; existence ex b1 being Walk of G st b1 is vertex-distinct proof end; end; definition end; definition end; registration let G be _Graph; let v be Vertex of G; coherence ( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is trivial ) by Lm4; end; registration let G be _Graph; let x, e, y be object ; cluster G .walkOf (x,e,y) -> Path-like ; coherence G .walkOf (x,e,y) is Path-like proof end; end; registration let G be _Graph; let x, e be object ; cluster G .walkOf (x,e,x) -> closed ; coherence G .walkOf (x,e,x) is closed proof end; end; registration let G be _Graph; let W be closed Walk of G; coherence proof end; end; registration let G be _Graph; let W be V5() Walk of G; cluster W .reverse() -> V5() ; coherence proof end; end; registration let G be _Graph; let W be Trail of G; coherence by Lm58; end; registration let G be _Graph; let W be Path of G; coherence by Lm63; end; registration let G be _Graph; let W1, W2 be closed Walk of G; cluster W1 .append W2 -> closed ; coherence W1 .append W2 is closed proof end; end; registration let G be _Graph; let W1, W2 be DWalk of G; cluster W1 .append W2 -> directed ; coherence W1 .append W2 is directed proof end; end; registration let G be _Graph; let W1, W2 be V5() Walk of G; cluster W1 .append W2 -> V5() ; coherence W1 .append W2 is trivial proof end; end; registration let G be _Graph; let W be DWalk of G; let m, n be Element of NAT ; cluster W .cut (m,n) -> directed ; coherence W .cut (m,n) is directed by Lm53; end; registration let G be _Graph; let W be V5() Walk of G; let m, n be Element of NAT ; cluster W .cut (m,n) -> V5() ; coherence W .cut (m,n) is trivial proof end; end; registration let G be _Graph; let W be Trail of G; let m, n be Element of NAT ; cluster W .cut (m,n) -> Trail-like ; coherence W .cut (m,n) is Trail-like by Lm59; end; registration let G be _Graph; let W be Path of G; let m, n be Element of NAT ; cluster W .cut (m,n) -> Path-like ; coherence W .cut (m,n) is Path-like by Lm64; end; registration let G be _Graph; let W be vertex-distinct Walk of G; let m, n be Element of NAT ; cluster W .cut (m,n) -> vertex-distinct ; coherence W .cut (m,n) is vertex-distinct proof end; end; registration let G be _Graph; let W be closed Walk of G; let m, n be Element of NAT ; cluster W .remove (m,n) -> closed ; coherence W .remove (m,n) is closed proof end; end; registration let G be _Graph; let W be DWalk of G; let m, n be Element of NAT ; cluster W .remove (m,n) -> directed ; coherence W .remove (m,n) is directed proof end; end; registration let G be _Graph; let W be V5() Walk of G; let m, n be Element of NAT ; cluster W .remove (m,n) -> V5() ; coherence W .remove (m,n) is trivial proof end; end; registration let G be _Graph; let W be Trail of G; let m, n be Element of NAT ; cluster W .remove (m,n) -> Trail-like ; coherence W .remove (m,n) is Trail-like proof end; end; registration let G be _Graph; let W be Path of G; let m, n be Element of NAT ; cluster W .remove (m,n) -> Path-like ; coherence W .remove (m,n) is Path-like proof end; end; definition let G be _Graph; let W be Walk of G; mode Subwalk of W -> Walk of G means :Def32: :: GLIB_001:def 32 ( it is_Walk_from W .first() ,W .last() & ex es being Subset of () st it .edgeSeq() = Seq es ); existence ex b1 being Walk of G st ( b1 is_Walk_from W .first() ,W .last() & ex es being Subset of () st b1 .edgeSeq() = Seq es ) proof end; end; :: deftheorem Def32 defines Subwalk GLIB_001:def 32 : for G being _Graph for W, b3 being Walk of G holds ( b3 is Subwalk of W iff ( b3 is_Walk_from W .first() ,W .last() & ex es being Subset of () st b3 .edgeSeq() = Seq es ) ); Lm70: for G being _Graph for W being Walk of G holds W is Subwalk of W proof end; Lm71: for G being _Graph for W1 being Walk of G for W2 being Subwalk of W1 for W3 being Subwalk of W2 holds W3 is Subwalk of W1 proof end; Lm72: for G being _Graph for W1, W2 being Walk of G st W1 is Subwalk of W2 holds len W1 <= len W2 proof end; definition let G be _Graph; let W be Walk of G; let m, n be Element of NAT ; :: original: .remove redefine func W .remove (m,n) -> Subwalk of W; coherence W .remove (m,n) is Subwalk of W proof end; end; registration let G be _Graph; let W be Walk of G; existence ex b1 being Subwalk of W st ( b1 is Trail-like & b1 is Path-like ) proof end; end; definition let G be _Graph; let W be Walk of G; mode Trail of W is Trail-like Subwalk of W; mode Path of W is Path-like Subwalk of W; end; registration let G be _Graph; let W be DWalk of G; existence ex b1 being Path of W st b1 is directed proof end; end; definition let G be _Graph; let W be DWalk of G; mode DWalk of W is directed Subwalk of W; mode DTrail of W is directed Trail of W; mode DPath of W is directed Path of W; end; definition let G be _Graph; func G .allWalks() -> non empty Subset of ((() \/ ()) *) equals :: GLIB_001:def 33 { W where W is Walk of G : verum } ; coherence { W where W is Walk of G : verum } is non empty Subset of ((() \/ ()) *) proof end; end; :: deftheorem defines .allWalks() GLIB_001:def 33 : for G being _Graph holds G .allWalks() = { W where W is Walk of G : verum } ; definition let G be _Graph; func G .allTrails() -> non empty Subset of () equals :: GLIB_001:def 34 { W where W is Trail of G : verum } ; coherence { W where W is Trail of G : verum } is non empty Subset of () proof end; end; :: deftheorem defines .allTrails() GLIB_001:def 34 : for G being _Graph holds G .allTrails() = { W where W is Trail of G : verum } ; definition let G be _Graph; func G .allPaths() -> non empty Subset of () equals :: GLIB_001:def 35 { W where W is Path of G : verum } ; coherence { W where W is Path of G : verum } is non empty Subset of () proof end; end; :: deftheorem defines .allPaths() GLIB_001:def 35 : for G being _Graph holds G .allPaths() = { W where W is Path of G : verum } ; definition let G be _Graph; func G .allDWalks() -> non empty Subset of () equals :: GLIB_001:def 36 { W where W is DWalk of G : verum } ; coherence { W where W is DWalk of G : verum } is non empty Subset of () proof end; end; :: deftheorem defines .allDWalks() GLIB_001:def 36 : for G being _Graph holds G .allDWalks() = { W where W is DWalk of G : verum } ; definition let G be _Graph; func G .allDTrails() -> non empty Subset of () equals :: GLIB_001:def 37 { W where W is DTrail of G : verum } ; coherence { W where W is DTrail of G : verum } is non empty Subset of () proof end; end; :: deftheorem defines .allDTrails() GLIB_001:def 37 : for G being _Graph holds G .allDTrails() = { W where W is DTrail of G : verum } ; definition let G be _Graph; func G .allDPaths() -> non empty Subset of () equals :: GLIB_001:def 38 { W where W is directed Path of G : verum } ; coherence { W where W is directed Path of G : verum } is non empty Subset of () proof end; end; :: deftheorem defines .allDPaths() GLIB_001:def 38 : for G being _Graph holds G .allDPaths() = { W where W is directed Path of G : verum } ; registration let G be _finite _Graph; correctness coherence ; proof end; end; definition let G be _Graph; let X be non empty Subset of (); :: original: Element redefine mode Element of X -> Walk of G; coherence for b1 being Element of X holds b1 is Walk of G proof end; end; definition let G be _Graph; let X be non empty Subset of (); :: original: Element redefine mode Element of X -> Trail of G; coherence for b1 being Element of X holds b1 is Trail of G proof end; end; definition let G be _Graph; let X be non empty Subset of (); :: original: Element redefine mode Element of X -> Path of G; coherence for b1 being Element of X holds b1 is Path of G proof end; end; definition let G be _Graph; let X be non empty Subset of (); :: original: Element redefine mode Element of X -> DWalk of G; coherence for b1 being Element of X holds b1 is DWalk of G proof end; end; definition let G be _Graph; let X be non empty Subset of (); :: original: Element redefine mode Element of X -> DTrail of G; coherence for b1 being Element of X holds b1 is DTrail of G proof end; end; definition let G be _Graph; let X be non empty Subset of (); :: original: Element redefine mode Element of X -> DPath of G; coherence for b1 being Element of X holds b1 is DPath of G proof end; end; theorem :: GLIB_001:7 for G being _Graph for W being Walk of G for n being odd Element of NAT st n <= len W holds W . n in the_Vertices_of G by Lm1; theorem Th7: :: GLIB_001:8 for G being _Graph for W being Walk of G for n being even Element of NAT st n in dom W holds W . n in the_Edges_of G proof end; theorem :: GLIB_001:9 for G being _Graph for W being Walk of G for n being even Element of NAT st n in dom W holds ex naa1 being odd Element of NAT st ( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G ) by Lm2; theorem Th9: :: GLIB_001:10 for G being _Graph for W being Walk of G for n being odd Element of NAT st n < len W holds W . (n + 1) in () .edgesInOut() proof end; theorem Th10: :: GLIB_001:11 for G being _Graph for W being Walk of G for n being odd Element of NAT st 1 < n & n <= len W holds W . (n - 1) in () .edgesInOut() proof end; theorem :: GLIB_001:12 for G being _Graph for W being Walk of G for n being odd Element of NAT st n < len W holds ( n in dom W & n + 1 in dom W & n + 2 in dom W ) proof end; theorem Th12: :: GLIB_001:13 for G being _Graph for v being Vertex of G holds ( len (G .walkOf v) = 1 & (G .walkOf v) . 1 = v & (G .walkOf v) .first() = v & (G .walkOf v) .last() = v & G .walkOf v is_Walk_from v,v ) proof end; theorem Th13: :: GLIB_001:14 for G being _Graph for e, x, y being object st e Joins x,y,G holds len (G .walkOf (x,e,y)) = 3 proof end; theorem Th14: :: GLIB_001:15 for G being _Graph for e, x, y being object st e Joins x,y,G holds ( (G .walkOf (x,e,y)) .first() = x & (G .walkOf (x,e,y)) .last() = y & G .walkOf (x,e,y) is_Walk_from x,y ) proof end; theorem :: GLIB_001:16 for G1, G2 being _Graph for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 holds ( W1 .first() = W2 .first() & W1 .last() = W2 .last() ) ; theorem :: GLIB_001:17 for G being _Graph for W being Walk of G for x, y being object holds ( W is_Walk_from x,y iff ( W . 1 = x & W . (len W) = y ) ) ; theorem :: GLIB_001:18 for G being _Graph for W being Walk of G for x, y being object st W is_Walk_from x,y holds ( x is Vertex of G & y is Vertex of G ) ; theorem :: GLIB_001:19 for G1, G2 being _Graph for x, y being object for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 holds ( W1 is_Walk_from x,y iff W2 is_Walk_from x,y ) ; theorem :: GLIB_001:20 for G1, G2 being _Graph for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 holds for n being Element of NAT holds W1 .vertexAt n = W2 .vertexAt n proof end; theorem :: GLIB_001:21 for G being _Graph for W being Walk of G holds ( len W = len () & dom W = dom () & rng W = rng () ) by ; theorem Th21: :: GLIB_001:22 for G being _Graph for W being Walk of G holds ( W .first() = () .last() & W .last() = () .first() ) proof end; theorem Th22: :: GLIB_001:23 for G being _Graph for W being Walk of G for x, y being object holds ( W is_Walk_from x,y iff W .reverse() is_Walk_from y,x ) proof end; theorem Th23: :: GLIB_001:24 for G being _Graph for W being Walk of G for n being Element of NAT st n in dom W holds ( W . n = () . (((len W) - n) + 1) & ((len W) - n) + 1 in dom () ) proof end; theorem :: GLIB_001:25 for G being _Graph for W being Walk of G for n being Element of NAT st n in dom () holds ( () . n = W . (((len W) - n) + 1) & ((len W) - n) + 1 in dom W ) by Lm8; theorem :: GLIB_001:26 canceled; ::$CT
theorem :: GLIB_001:27
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .reverse() = W2 .reverse() ;

theorem :: GLIB_001:28
for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(len (W1 .append W2)) + 1 = (len W1) + (len W2) by Lm9;

theorem :: GLIB_001:29
for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
( len W1 <= len (W1 .append W2) & len W2 <= len (W1 .append W2) ) by Lm10;

theorem :: GLIB_001:30
for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
( (W1 .append W2) .first() = W1 .first() & (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() ) by Lm11;

theorem Th29: :: GLIB_001:31
for G being _Graph
for W1, W2 being Walk of G
for x, y, z being object st W1 is_Walk_from x,y & W2 is_Walk_from y,z holds
W1 .append W2 is_Walk_from x,z by Lm11;

theorem :: GLIB_001:32
for G being _Graph
for W1, W2 being Walk of G
for n being Element of NAT st n in dom W1 holds
( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) by Lm12;

theorem :: GLIB_001:33
for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
for n being Element of NAT st n < len W2 holds
( (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) & (len W1) + n in dom (W1 .append W2) ) by Lm13;

theorem :: GLIB_001:34
for G being _Graph
for W1, W2 being Walk of G
for n being Element of NAT holds
( not n in dom (W1 .append W2) or n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ) by Lm14;

theorem Th33: :: GLIB_001:35
for G1, G2 being _Graph
for W1A, W1B being Walk of G1
for W2A, W2B being Walk of G2 st W1A = W2A & W1B = W2B holds
W1A .append W1B = W2A .append W2B
proof end;

theorem :: GLIB_001:36
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W holds
( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of NAT st i < len (W .cut (m,n)) holds
( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W ) ) ) by Lm15;

theorem :: GLIB_001:37
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W holds
( (W .cut (m,n)) .first() = W . m & (W .cut (m,n)) .last() = W . n & W .cut (m,n) is_Walk_from W . m,W . n ) by Lm16;

theorem :: GLIB_001:38
for G being _Graph
for W being Walk of G
for m, n, o being odd Element of NAT st m <= n & n <= o & o <= len W holds
(W .cut (m,n)) .append (W .cut (n,o)) = W .cut (m,o) by Lm17;

theorem :: GLIB_001:39
for G being _Graph
for W being Walk of G holds W .cut (1,(len W)) = W by Lm18;

theorem Th38: :: GLIB_001:40
for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n < len W holds
G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = W .cut (n,(n + 2))
proof end;

theorem Th39: :: GLIB_001:41
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n < len W holds
(W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2))
proof end;

theorem :: GLIB_001:42
for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n <= len W holds
W .cut (n,n) = <*()*> by Lm19;

theorem :: GLIB_001:43
for G being _Graph
for W being Walk of G
for n, m being Element of NAT st m is odd & m <= n holds
(W .cut (1,n)) .cut (1,m) = W .cut (1,m) by Lm20;

theorem :: GLIB_001:44
for G being _Graph
for W1, W2 being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W1 & W1 .last() = W2 .first() holds
(W1 .append W2) .cut (m,n) = W1 .cut (m,n) by Lm21;

theorem :: GLIB_001:45
for G being _Graph
for W being Walk of G
for m being odd Element of NAT st m <= len W holds
len (W .cut (1,m)) = m by Lm22;

theorem :: GLIB_001:46
for G being _Graph
for W being Walk of G
for m being odd Element of NAT
for x being Element of NAT st x in dom (W .cut (1,m)) & m <= len W holds
(W .cut (1,m)) . x = W . x by Lm23;

theorem :: GLIB_001:47
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT
for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut (m,n)) holds
( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )
proof end;

theorem Th46: :: GLIB_001:48
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2
for m, n being Element of NAT st W1 = W2 holds
W1 .cut (m,n) = W2 .cut (m,n)
proof end;

theorem :: GLIB_001:49
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds
(len (W .remove (m,n))) + n = (len W) + m by Lm24;

theorem :: GLIB_001:50
for G being _Graph
for W being Walk of G
for x, y being set
for n, m being Element of NAT st W is_Walk_from x,y holds
W .remove (m,n) is_Walk_from x,y by Lm25;

theorem :: GLIB_001:51
for G being _Graph
for W being Walk of G
for n, m being Element of NAT holds len (W .remove (m,n)) <= len W by Lm26;

theorem :: GLIB_001:52
for G being _Graph
for W being Walk of G
for m being Element of NAT holds W .remove (m,m) = W by Lm27;

theorem :: GLIB_001:53
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds
(W .cut (1,m)) .last() = (W .cut (n,(len W))) .first() by Lm28;

theorem :: GLIB_001:54
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds
for x being Element of NAT st x in Seg m holds
(W .remove (m,n)) . x = W . x by Lm29;

theorem :: GLIB_001:55
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds
for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds
( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W ) by Lm30;

theorem :: GLIB_001:56
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds
len (W .remove (m,n)) = ((len W) + m) - n by Lm31;

theorem Th55: :: GLIB_001:57
for G being _Graph
for W being Walk of G
for m being Element of NAT st W . m = W .last() holds
W .remove (m,(len W)) = W .cut (1,m)
proof end;

theorem :: GLIB_001:58
for G being _Graph
for W being Walk of G
for m being Element of NAT st W .first() = W . m holds
W .remove (1,m) = W .cut (m,(len W)) by Lm32;

theorem :: GLIB_001:59
for G being _Graph
for W being Walk of G
for n, m being Element of NAT holds
( (W .remove (m,n)) .first() = W .first() & (W .remove (m,n)) .last() = W .last() ) by Lm33;

theorem :: GLIB_001:60
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT
for x being Element of NAT st m <= n & n <= len W & W . m = W . n & x in dom (W .remove (m,n)) & not x in Seg m holds
( m <= x & x <= len (W .remove (m,n)) ) by Lm34;

theorem :: GLIB_001:61
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2
for m, n being Element of NAT st W1 = W2 holds
W1 .remove (m,n) = W2 .remove (m,n)
proof end;

theorem :: GLIB_001:62
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
W .addEdge e = W ^ <*e,x*> by Lm35;

theorem :: GLIB_001:63
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x ) by Lm36;

theorem :: GLIB_001:64
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
len (W .addEdge e) = (len W) + 2 by Lm37;

theorem :: GLIB_001:65
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
( (W .addEdge e) . ((len W) + 1) = e & (W .addEdge e) . ((len W) + 2) = x & ( for n being Element of NAT st n in dom W holds
(W .addEdge e) . n = W . n ) ) by Lm38;

theorem :: GLIB_001:66
for G being _Graph
for W being Walk of G
for e, x, y, z being object st W is_Walk_from x,y & e Joins y,z,G holds
W .addEdge e is_Walk_from x,z by Lm39;

theorem Th65: :: GLIB_001:67
for G being _Graph
for W being Walk of G holds 1 <= len ()
proof end;

theorem Th66: :: GLIB_001:68
for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n <= len W holds
( (2 * ((n + 1) div 2)) - 1 = n & 1 <= (n + 1) div 2 & (n + 1) div 2 <= len () )
proof end;

theorem :: GLIB_001:69
for G being _Graph
for v being Vertex of G holds (G .walkOf v) .vertexSeq() = <*v*>
proof end;

theorem Th68: :: GLIB_001:70
for G being _Graph
for e, x, y being object st e Joins x,y,G holds
(G .walkOf (x,e,y)) .vertexSeq() = <*x,y*>
proof end;

theorem :: GLIB_001:71
for G being _Graph
for W being Walk of G holds
( W .first() = () . 1 & W .last() = () . (len ()) )
proof end;

theorem :: GLIB_001:72
for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n <= len W holds
W .vertexAt n = () . ((n + 1) div 2)
proof end;

theorem Th71: :: GLIB_001:73
for G being _Graph
for W being Walk of G
for n being Element of NAT holds
( n in dom () iff (2 * n) - 1 in dom W )
proof end;

theorem :: GLIB_001:74
for G being _Graph
for W being Walk of G
for n being Element of NAT holds (W .cut (1,n)) .vertexSeq() c= W .vertexSeq()
proof end;

theorem Th73: :: GLIB_001:75
for G being _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .vertexSeq() = () ^ <*x*>
proof end;

theorem Th74: :: GLIB_001:76
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .vertexSeq() = W2 .vertexSeq()
proof end;

theorem :: GLIB_001:77
for G being _Graph
for W being Walk of G
for n being even Element of NAT st 1 <= n & n <= len W holds
( n div 2 in dom () & W . n = () . (n div 2) ) by Lm40;

theorem :: GLIB_001:78
for G being _Graph
for W being Walk of G
for n being Element of NAT holds
( n in dom () iff 2 * n in dom W ) by Lm41;

theorem :: GLIB_001:79
for G being _Graph
for W being Walk of G
for n being Element of NAT st n in dom () holds
() . n in the_Edges_of G
proof end;

theorem :: GLIB_001:80
for G being _Graph
for W being Walk of G ex lenWaa1 being even Element of NAT st
( lenWaa1 = (len W) - 1 & len () = lenWaa1 div 2 ) by Lm42;

theorem :: GLIB_001:81
for G being _Graph
for W being Walk of G
for n being Element of NAT holds (W .cut (1,n)) .edgeSeq() c= W .edgeSeq() by Lm43;

theorem :: GLIB_001:82
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .edgeSeq() = () ^ <*e*> by Lm44;

theorem Th81: :: GLIB_001:83
for G being _Graph
for e, x, y being object holds
( e Joins x,y,G iff (G .walkOf (x,e,y)) .edgeSeq() = <*e*> )
proof end;

theorem :: GLIB_001:84
for G being _Graph
for W being Walk of G holds () .edgeSeq() = Rev ()
proof end;

theorem :: GLIB_001:85
for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .edgeSeq() = () ^ ()
proof end;

theorem Th84: :: GLIB_001:86
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .edgeSeq() = W2 .edgeSeq()
proof end;

theorem :: GLIB_001:87
for G being _Graph
for W being Walk of G
for x being set holds
( x in W .vertices() iff ex n being odd Element of NAT st
( n <= len W & W . n = x ) ) by Lm45;

theorem Th86: :: GLIB_001:88
for G being _Graph
for W being Walk of G holds
( W .first() in W .vertices() & W .last() in W .vertices() )
proof end;

theorem Th87: :: GLIB_001:89
for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n <= len W holds
W .vertexAt n in W .vertices()
proof end;

theorem :: GLIB_001:90
for G being _Graph
for v being Vertex of G holds (G .walkOf v) .vertices() = {v}
proof end;

theorem Th89: :: GLIB_001:91
for G being _Graph
for e, x, y being object st e Joins x,y,G holds
(G .walkOf (x,e,y)) .vertices() = {x,y}
proof end;

theorem :: GLIB_001:92
for G being _Graph
for W being Walk of G holds W .vertices() = () .vertices()
proof end;

theorem Th91: :: GLIB_001:93
for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .vertices() = () \/ ()
proof end;

theorem :: GLIB_001:94
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W holds
(W .cut (m,n)) .vertices() c= W .vertices()
proof end;

theorem Th93: :: GLIB_001:95
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .vertices() = () \/ {x}
proof end;

theorem :: GLIB_001:96
for G being _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G & not x in W .vertices() holds
card ((W .addEdge e) .vertices()) = (card ()) + 1
proof end;

theorem :: GLIB_001:97
for G being _Graph
for W being Walk of G
for x, y being set st x in W .vertices() & y in W .vertices() holds
ex W9 being Walk of G st W9 is_Walk_from x,y
proof end;

theorem :: GLIB_001:98
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .vertices() = W2 .vertices() by Th74;

theorem :: GLIB_001:99
for G being _Graph
for W being Walk of G
for e being set holds
( e in W .edges() iff ex n being even Element of NAT st
( 1 <= n & n <= len W & W . n = e ) ) by Lm46;

theorem Th98: :: GLIB_001:100
for G being _Graph
for W being Walk of G
for e being set holds
( e in W .edges() iff ex n being odd Element of NAT st
( n < len W & W . (n + 1) = e ) )
proof end;

theorem Th99: :: GLIB_001:101
for G being _Graph
for W being Walk of G holds rng W = () \/ ()
proof end;

theorem Th100: :: GLIB_001:102
for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .edges() = (W1 .edges()) \/ (W2 .edges())
proof end;

theorem :: GLIB_001:103
for G being _Graph
for W being Walk of G
for e being set st e in W .edges() holds
ex v1, v2 being Vertex of G ex n being odd Element of NAT st
( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G ) by Lm47;

theorem Th102: :: GLIB_001:104
for G being _Graph
for W being Walk of G
for e being set holds
( e in W .edges() iff ex n being Element of NAT st
( n in dom () & () . n = e ) )
proof end;

theorem :: GLIB_001:105
for G being _Graph
for W being Walk of G
for e, x, y being set st e in W .edges() & e Joins x,y,G holds
( x in W .vertices() & y in W .vertices() ) by Lm48;

theorem :: GLIB_001:106
for G being _Graph
for W being Walk of G
for n, m being Element of NAT holds (W .cut (m,n)) .edges() c= W .edges()
proof end;

theorem Th105: :: GLIB_001:107
for G being _Graph
for W being Walk of G holds W .edges() = () .edges()
proof end;

theorem Th106: :: GLIB_001:108
for G being _Graph
for e, x, y being object holds
( e Joins x,y,G iff (G .walkOf (x,e,y)) .edges() = {e} )
proof end;

theorem :: GLIB_001:109
for G being _Graph
for W being Walk of G holds W .edges() c= G .edgesBetween ()
proof end;

theorem :: GLIB_001:110
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .edges() = W2 .edges() by Th84;

theorem :: GLIB_001:111
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .edges() = () \/ {e}
proof end;

theorem :: GLIB_001:112
for G being _Graph
for W being Walk of G holds len W = (2 * ()) + 1 by Def15;

theorem :: GLIB_001:113
for G being _Graph
for W1, W2 being Walk of G holds
( len W1 = len W2 iff W1 .length() = W2 .length() )
proof end;

theorem :: GLIB_001:114
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .length() = W2 .length() by Th84;

theorem Th113: :: GLIB_001:115
for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n <= len W holds
( W .find (W . n) <= n & W .rfind (W . n) >= n )
proof end;

theorem :: GLIB_001:116
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2
for v being set st W1 = W2 holds
( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )
proof end;

theorem :: GLIB_001:117
for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n <= len W holds
( W .find n <= n & W .rfind n >= n ) by ;

theorem :: GLIB_001:118
for G being _Graph
for W being Walk of G holds
( W is closed iff W . 1 = W . (len W) ) ;

theorem :: GLIB_001:119
for G being _Graph
for W being Walk of G holds
( W is closed iff ex x being set st W is_Walk_from x,x )
proof end;

theorem :: GLIB_001:120
for G being _Graph
for W being Walk of G holds
( W is closed iff W .reverse() is closed )
proof end;

theorem :: GLIB_001:121
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is closed holds
W2 is closed ;

theorem :: GLIB_001:122
for G being _Graph
for W being Walk of G holds
( W is directed iff for n being odd Element of NAT st n < len W holds
W . (n + 1) DJoins W . n,W . (n + 2),G ) by Lm51;

theorem :: GLIB_001:123
for G being _Graph
for W being Walk of G
for e, x, y, z being set st W is directed & W is_Walk_from x,y & e DJoins y,z,G holds
( W .addEdge e is directed & W .addEdge e is_Walk_from x,z ) by Lm52;

theorem :: GLIB_001:124
for G being _Graph
for W being DWalk of G
for m, n being Element of NAT holds W .cut (m,n) is directed ;

theorem :: GLIB_001:125
for G being _Graph
for W being Walk of G holds
( W is V5() iff 3 <= len W ) by Lm54;

theorem :: GLIB_001:126
for G being _Graph
for W being Walk of G holds
( W is V5() iff len W <> 1 ) by Lm55;

theorem :: GLIB_001:127
for G being _Graph
for W being Walk of G st W .first() <> W .last() holds
not W is V5() by Lm55;

theorem :: GLIB_001:128
for G being _Graph
for W being Walk of G holds
( W is V5() iff ex v being Vertex of G st W = G .walkOf v ) by Lm56;

theorem :: GLIB_001:129
for G being _Graph
for W being Walk of G holds
( W is V5() iff W .reverse() is V5() )
proof end;

theorem :: GLIB_001:130
for G being _Graph
for W1, W2 being Walk of G st W2 is V5() holds
W1 .append W2 = W1
proof end;

theorem :: GLIB_001:131
for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W holds
( W .cut (m,n) is V5() iff m = n )
proof end;

theorem Th130: :: GLIB_001:132
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
not W .addEdge e is V5()
proof end;

theorem Th131: :: GLIB_001:133
for G being _Graph
for W being Walk of G st W is V5() holds
ex lenW2 being odd Element of NAT st
( lenW2 = (len W) - 2 & (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W )
proof end;

theorem Th132: :: GLIB_001:134
for G being _Graph
for W1, W2 being Walk of G st W2 is V5() & W2 .edges() c= W1 .edges() holds
W2 .vertices() c= W1 .vertices()
proof end;

theorem :: GLIB_001:135
for G being _Graph
for W being Walk of G st W is V5() holds
for v being Vertex of G st v in W .vertices() holds
not v is isolated
proof end;

theorem :: GLIB_001:136
for G being _Graph
for W being Walk of G holds
( W is V5() iff W .edges() = {} )
proof end;

theorem :: GLIB_001:137
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is V5() holds
W2 is V5() ;

theorem :: GLIB_001:138
for G being _Graph
for W being Walk of G holds
( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . n ) by Lm57;

theorem :: GLIB_001:139
for G being _Graph
for W being Walk of G st len W <= 3 holds
W is Trail-like by Lm61;

theorem :: GLIB_001:140
for G being _Graph
for W being Walk of G holds
( W is Trail-like iff W .reverse() is Trail-like ) by Lm58;

theorem :: GLIB_001:141
for G being _Graph
for W being Trail of G
for m, n being Element of NAT holds W .cut (m,n) is Trail-like ;

theorem :: GLIB_001:142
for G being _Graph
for W being Trail of G
for e being set st e in () .edgesInOut() & not e in W .edges() holds
W .addEdge e is Trail-like by Lm60;

theorem :: GLIB_001:143
for G being _Graph
for W being Trail of G
for v being Vertex of G st v in W .vertices() & v is endvertex & not v = W .first() holds
v = W .last()
proof end;

theorem :: GLIB_001:144
for G being _finite _Graph
for W being Trail of G holds len () <= G .size()
proof end;

theorem :: GLIB_001:145
for G being _Graph
for W being Walk of G st len W <= 3 holds
W is Path-like by Lm69;

theorem :: GLIB_001:146
for G being _Graph
for W being Walk of G st ( for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds
m = n ) holds
W is Path-like by Lm66;

theorem :: GLIB_001:147
for G being _Graph
for W being Path of G st W is open holds
for m, n being odd Element of NAT st m < n & n <= len W holds
W . m <> W . n
proof end;

theorem :: GLIB_001:148
for G being _Graph
for W being Walk of G holds
( W is Path-like iff W .reverse() is Path-like ) by Lm63;

theorem :: GLIB_001:149
for G being _Graph
for W being Path of G
for m, n being Element of NAT holds W .cut (m,n) is Path-like ;

theorem Th148: :: GLIB_001:150
for G being _Graph
for W being Path of G
for e, v being object st e Joins W .last() ,v,G & not e in W .edges() & ( not W is V5() or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v ) holds
proof end;

theorem :: GLIB_001:151
for G being _Graph
for W being Path of G
for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() & ( not W is V5() or W is open ) holds
W .addEdge e is Path-like by Lm68;

theorem :: GLIB_001:152
for G being _Graph
for W being Walk of G st ( for n being odd Element of NAT st n <= len W holds
W .find (W . n) = W .rfind (W . n) ) holds
W is Path-like
proof end;

theorem :: GLIB_001:153
for G being _Graph
for W being Walk of G st ( for n being odd Element of NAT st n <= len W holds
W .rfind n = n ) holds
W is Path-like by Lm67;

theorem :: GLIB_001:154
for G being _finite _Graph
for W being Path of G holds len () <= () + 1
proof end;

theorem :: GLIB_001:155
for G being _Graph
for W being vertex-distinct Walk of G
for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds
proof end;

theorem :: GLIB_001:156
for G being _Graph
for e, x being object st e Joins x,x,G holds
G .walkOf (x,e,x) is Cycle-like
proof end;

theorem :: GLIB_001:157
for G being _Graph
for W1 being Walk of G
for e, x, y being set st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )
proof end;

theorem :: GLIB_001:158
for G being _Graph
for W being Walk of G holds W is Subwalk of W by Lm70;

theorem :: GLIB_001:159
for G being _Graph
for W1 being Walk of G
for W2 being Subwalk of W1
for W3 being Subwalk of W2 holds W3 is Subwalk of W1 by Lm71;

theorem :: GLIB_001:160
for G being _Graph
for W1, W2 being Walk of G
for x, y being set st W1 is Subwalk of W2 holds
( W1 is_Walk_from x,y iff W2 is_Walk_from x,y )
proof end;

theorem Th159: :: GLIB_001:161
for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
( W1 .first() = W2 .first() & W1 .last() = W2 .last() )
proof end;

theorem :: GLIB_001:162
for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
len W1 <= len W2 by Lm72;

theorem Th161: :: GLIB_001:163
for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
( W1 .edges() c= W2 .edges() & W1 .vertices() c= W2 .vertices() )
proof end;

theorem Th162: :: GLIB_001:164
for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
for m being odd Element of NAT st m <= len W1 holds
ex n being odd Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )
proof end;

theorem :: GLIB_001:165
for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
for m being even Element of NAT st 1 <= m & m <= len W1 holds
ex n being even Element of NAT st
( m <= n & n <= len W2 & W1 . m = W2 . n )
proof end;

theorem :: GLIB_001:166
for G being _Graph
for W1 being Trail of G st W1 is V5() holds
ex W2 being Path of W1 st W2 is V5()
proof end;

theorem Th165: :: GLIB_001:167
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G2 holds W is Walk of G1
proof end;

theorem Th166: :: GLIB_001:168
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G1 st W is V5() & W .first() in the_Vertices_of G2 holds
W is Walk of G2
proof end;

theorem Th167: :: GLIB_001:169
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G1 st W is V5() & W .edges() c= the_Edges_of G2 holds
W is Walk of G2
proof end;

theorem Th168: :: GLIB_001:170
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 & W .edges() c= the_Edges_of G2 holds
W is Walk of G2
proof end;

theorem :: GLIB_001:171
for G1 being non _trivial _Graph
for W being Walk of G1
for v being Vertex of G1
for G2 being removeVertex of G1,v st not v in W .vertices() holds
W is Walk of G2
proof end;

theorem :: GLIB_001:172
for G1 being _Graph
for W being Walk of G1
for e being set
for G2 being removeEdge of G1,e st not e in W .edges() holds
W is Walk of G2
proof end;

theorem Th171: :: GLIB_001:173
for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e Joins x,y,G2 holds
G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)
proof end;

theorem :: GLIB_001:174
for G1 being _Graph
for G2 being Subgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2
for e being set st W1 = W2 & e in (W2 .last()) .edgesInOut() holds
proof end;

theorem Th173: :: GLIB_001:175
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G2 holds
( ( W is closed implies W is closed Walk of G1 ) & ( W is directed implies W is directed Walk of G1 ) & ( W is V5() implies W is V5() Walk of G1 ) & ( W is Trail-like implies W is Trail-like Walk of G1 ) & ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )
proof end;

theorem Th174: :: GLIB_001:176
for G1 being _Graph
for G2 being Subgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
proof end;

theorem :: GLIB_001:177
for G1, G2 being _Graph
for x being set st G1 == G2 & x is VertexSeq of G1 holds
x is VertexSeq of G2
proof end;

theorem :: GLIB_001:178
for G1, G2 being _Graph
for x being set st G1 == G2 & x is EdgeSeq of G1 holds
x is EdgeSeq of G2
proof end;

theorem :: GLIB_001:179
for G1, G2 being _Graph
for x being set st G1 == G2 & x is Walk of G1 holds
x is Walk of G2
proof end;

theorem :: GLIB_001:180
for G1, G2 being _Graph
for e, x, y being set st G1 == G2 holds
G1 .walkOf (x,e,y) = G2 .walkOf (x,e,y)
proof end;

theorem :: GLIB_001:181
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st G1 == G2 & W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
proof end;