:: Walks in a Graph :: by Gilbert Lee :: :: Received February 22, 2005 :: Copyright (c) 2005-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, ABIAN, SUBSET_1, ARYTM_3, XXREAL_0, ARYTM_1, CARD_1, TARSKI, FINSEQ_1, RELAT_1, FUNCT_1, NAT_1, XBOOLE_0, GLIB_000, FINSEQ_5, GRAPH_2, INT_1, FINSET_1, RCOMP_1, WAYBEL_0, ZFMISC_1, MSAFREE2, ORDINAL4, GRAPH_1, FUNCT_4, FUNCOP_1, MCART_1, GLIB_001; notations TARSKI, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, XCMPLX_0, XXREAL_0, DOMAIN_1, RELAT_1, FUNCT_1, FINSEQ_1, GRAPH_2, FINSEQ_5, RELSET_1, XTUPLE_0, MCART_1, FINSET_1, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, GLIB_000, ABIAN, FINSEQ_6; constructors DOMAIN_1, FUNCT_4, NAT_D, RECDEF_1, FINSEQ_5, GLIB_000, ABIAN, GRAPH_2, XXREAL_2, RELSET_1, FINSEQ_2, RAT_1, XTUPLE_0, FINSEQ_6; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, GLIB_000, ABIAN, GRAPH_3, CARD_1, XTUPLE_0, FINSEQ_6; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin :: Preliminaries theorem :: GLIB_001:1 for x,y being odd Element of NAT holds x < y iff x + 2 <= y; ::$CT theorem :: GLIB_001:3 for X being set, fs being FinSequence of X, fss being Subset of fs holds len (Seq fss) <= len fs; theorem :: GLIB_001:4 for X being set, fs being FinSequence of X, fss being Subset of fs, 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; theorem :: GLIB_001:5 for X being set, fs being FinSequence of X, fss being Subset of fs holds len Seq fss = card fss; theorem :: GLIB_001:6 for X being set, fs being FinSequence of X, fss being Subset of fs holds dom Seq fss = dom Sgm (dom fss); begin :: Definitions definition let G be _Graph; mode VertexSeq of G -> FinSequence of the_Vertices_of G means :: 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; end; definition let G be _Graph; mode EdgeSeq of G -> FinSequence of the_Edges_of G means :: 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; end; definition let G be _Graph; mode Walk of G -> FinSequence of the_Vertices_of G \/ the_Edges_of G means :: 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; end; registration let G be _Graph, W be Walk of G; cluster len W -> odd non empty; end; definition let G be _Graph, v be Vertex of G; func G.walkOf(v) -> Walk of G equals :: GLIB_001:def 4 <*v*>; end; definition let G be _Graph, x,y,e be object; func G.walkOf(x,e,y) -> Walk of G equals :: GLIB_001:def 5 <*x,e,y*> if e Joins x,y,G otherwise G.walkOf(the Element of the_Vertices_of G); end; definition let G be _Graph, W be Walk of G; func W.first() -> Vertex of G equals :: GLIB_001:def 6 W.1; func W.last() -> Vertex of G equals :: GLIB_001:def 7 W.(len W); end; definition let G be _Graph, W be Walk of G, n be Nat; func W.vertexAt(n) -> Vertex of G equals :: GLIB_001:def 8 W.n if n is odd & n <= len W otherwise W.first(); end; definition let G be _Graph, W be Walk of G; func W.reverse() -> Walk of G equals :: GLIB_001:def 9 Rev W; involutiveness; end; definition let G be _Graph, W1, W2 be Walk of G; func W1.append(W2) -> Walk of G equals :: GLIB_001:def 10 W1 ^' W2 if W1.last() = W2 .first() otherwise W1; end; definition let G be _Graph, W be Walk of G, m, n being Nat; func W.cut(m,n) -> Walk of G equals :: GLIB_001:def 11 (m,n)-cut W if m is odd & n is odd & m <= n & n <= len W otherwise W; end; definition let G be _Graph, W be Walk of G, m, n be Element of NAT; func W.remove(m,n) -> Walk of G equals :: 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; end; definition let G be _Graph, W be Walk of G, e be object; func W.addEdge(e) -> Walk of G equals :: GLIB_001:def 13 W.append(G.walkOf(W.last(), e, W .last().adj(e))); end; definition let G be _Graph, W be Walk of G; func W.vertexSeq() -> VertexSeq of G means :: 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); end; definition let G be _Graph, W be Walk of G; func W.edgeSeq() -> EdgeSeq of G means :: 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); end; definition let G be _Graph, W be Walk of G; func W.vertices() -> finite Subset of the_Vertices_of G equals :: GLIB_001:def 16 rng W.vertexSeq(); end; definition let G be _Graph, W be Walk of G; func W.edges() -> finite Subset of the_Edges_of G equals :: GLIB_001:def 17 rng W.edgeSeq(); end; definition let G be _Graph, W be Walk of G; func W.length() -> Element of NAT equals :: GLIB_001:def 18 len W.edgeSeq(); end; definition let G be _Graph, W be Walk of G, v be set; func W.find(v) -> odd Element of NAT means :: 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; end; definition let G be _Graph, W be Walk of G, n be Element of NAT; func W.find(n) -> odd Element of NAT means :: 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; end; definition let G be _Graph, W be Walk of G, v be set; func W.rfind(v) -> odd Element of NAT means :: 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; end; definition let G be _Graph, W be Walk of G, n be Element of NAT; func W.rfind(n) -> odd Element of NAT means :: 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; end; definition let G be _Graph, u, v be object, W be Walk of G; pred W is_Walk_from u,v means :: GLIB_001:def 23 W.first() = u & W.last() = v; end; definition let G be _Graph, W be Walk of G; attr W is closed means :: GLIB_001:def 24 W.first() = W.last(); attr W is directed means :: GLIB_001:def 25 for n being odd Element of NAT st n < len W holds (the_Source_of G).(W.(n+1)) = W.n; redefine attr W is trivial means :: GLIB_001:def 26 W.length() = 0; attr W is Trail-like means :: GLIB_001:def 27 W.edgeSeq() is one-to-one; end; notation let G be _Graph, W be Walk of G; antonym W is open for W is closed; end; definition let G be _Graph, W be Walk of G; attr W is Path-like means :: GLIB_001:def 28 W is Trail-like & for m, n being odd Element of NAT st m < n & n <= len W holds W.m = W.n implies m = 1 & n = len W; end; definition let G be _Graph, W be Walk of G; attr W is vertex-distinct means :: 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; definition let G be _Graph, W be Walk of G; attr W is Circuit-like means :: GLIB_001:def 30 W is closed & W is Trail-like & W is non trivial; attr W is Cycle-like means :: GLIB_001:def 31 W is closed & W is Path-like & W is non trivial; end; registration let G be _Graph; cluster Path-like -> Trail-like for Walk of G; cluster trivial -> Path-like for Walk of G; cluster trivial -> vertex-distinct for Walk of G; cluster vertex-distinct -> Path-like for Walk of G; cluster Circuit-like -> closed Trail-like non trivial for Walk of G; cluster Cycle-like -> closed Path-like non trivial for Walk of G; end; registration let G be _Graph; cluster closed directed trivial for Walk of G; end; registration let G be _Graph; cluster vertex-distinct for Walk of G; end; definition let G be _Graph; mode Trail of G is Trail-like Walk of G; mode Path of G is Path-like Walk of G; end; definition let G be _Graph; mode DWalk of G is directed Walk of G; mode DTrail of G is directed Trail of G; mode DPath of G is directed Path of G; end; registration let G be _Graph, v be Vertex of G; cluster G.walkOf(v) -> closed directed trivial; end; registration let G be _Graph, x,e,y be object; cluster G.walkOf(x,e,y) -> Path-like; end; registration let G be _Graph, x,e be object; cluster G.walkOf(x,e,x) -> closed; end; registration let G be _Graph, W be closed Walk of G; cluster W.reverse() -> closed; end; registration let G be _Graph, W be trivial Walk of G; cluster W.reverse() -> trivial; end; registration let G be _Graph, W be Trail of G; cluster W.reverse() -> Trail-like; end; registration let G be _Graph, W be Path of G; cluster W.reverse() -> Path-like; end; registration let G be _Graph, W1,W2 be closed Walk of G; cluster W1.append(W2) -> closed; end; registration let G be _Graph, W1,W2 be DWalk of G; cluster W1.append(W2) -> directed; end; registration let G be _Graph, W1,W2 be trivial Walk of G; cluster W1.append(W2) -> trivial; end; registration let G be _Graph, W be DWalk of G, m,n be Element of NAT; cluster W.cut(m,n) -> directed; end; registration let G be _Graph, W be trivial Walk of G, m,n be Element of NAT; cluster W.cut(m,n) -> trivial; end; registration let G be _Graph, W be Trail of G, m,n be Element of NAT; cluster W.cut(m,n) -> Trail-like; end; registration let G be _Graph, W be Path of G, m,n be Element of NAT; cluster W.cut(m,n) -> Path-like; end; registration let G be _Graph, W be vertex-distinct Walk of G, m,n be Element of NAT; cluster W.cut(m,n) -> vertex-distinct; end; registration let G be _Graph, W be closed Walk of G, m,n be Element of NAT; cluster W.remove(m,n) -> closed; end; registration let G be _Graph, W be DWalk of G, m,n be Element of NAT; cluster W.remove(m,n) -> directed; end; registration let G be _Graph, W be trivial Walk of G, m,n be Element of NAT; cluster W.remove(m,n) -> trivial; end; registration let G be _Graph, W be Trail of G, m,n be Element of NAT; cluster W.remove(m,n) -> Trail-like; end; registration let G be _Graph, W be Path of G, m,n be Element of NAT; cluster W.remove(m,n) -> Path-like; end; definition let G be _Graph, W be Walk of G; mode Subwalk of W -> Walk of G means :: GLIB_001:def 32 it is_Walk_from W.first(), W .last() & ex es being Subset of W.edgeSeq() st it.edgeSeq() = Seq es; end; definition let G be _Graph, W be Walk of G, m,n being Element of NAT; redefine func W.remove(m,n) -> Subwalk of W; end; registration let G be _Graph, W be Walk of G; cluster Trail-like Path-like for Subwalk of W; end; definition let G be _Graph, 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, W be DWalk of G; cluster directed for Path of W; end; definition let G be _Graph, 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 ((the_Vertices_of G)\/(the_Edges_of G))* equals :: GLIB_001:def 33 the set of all W where W is Walk of G ; end; definition let G be _Graph; func G.allTrails() -> non empty Subset of G.allWalks() equals :: GLIB_001:def 34 the set of all W where W is Trail of G ; end; definition let G be _Graph; func G.allPaths() -> non empty Subset of G.allTrails() equals :: GLIB_001:def 35 the set of all W where W is Path of G ; end; definition let G be _Graph; func G.allDWalks() -> non empty Subset of G.allWalks() equals :: GLIB_001:def 36 the set of all W where W is DWalk of G ; end; definition let G be _Graph; func G.allDTrails() -> non empty Subset of G.allTrails() equals :: GLIB_001:def 37 the set of all W where W is DTrail of G ; end; definition let G be _Graph; func G.allDPaths() -> non empty Subset of G.allDTrails() equals :: GLIB_001:def 38 the set of all W where W is directed Path of G ; end; registration let G be _finite _Graph; cluster G.allTrails() -> finite; end; definition let G be _Graph, X be non empty Subset of G.allWalks(); redefine mode Element of X -> Walk of G; end; definition let G be _Graph, X be non empty Subset of G.allTrails(); redefine mode Element of X -> Trail of G; end; definition let G be _Graph, X be non empty Subset of G.allPaths(); redefine mode Element of X -> Path of G; end; definition let G be _Graph, X be non empty Subset of G.allDWalks(); redefine mode Element of X -> DWalk of G; end; definition let G be _Graph, X be non empty Subset of G.allDTrails(); redefine mode Element of X -> DTrail of G; end; definition let G be _Graph, X be non empty Subset of G.allDPaths(); redefine mode Element of X -> DPath of G; end; begin :: Theorems reserve G,G1,G2 for _Graph; reserve W,W1,W2 for Walk of G; reserve e,x,y,z for set; reserve v for Vertex of G; reserve n,m for Element of NAT; theorem :: GLIB_001:7 for n being odd Element of NAT st n <= len W holds W.n in the_Vertices_of G; theorem :: GLIB_001:8 for n being even Element of NAT st n in dom W holds W.n in the_Edges_of G; theorem :: GLIB_001:9 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; theorem :: GLIB_001:10 for n being odd Element of NAT st n < len W holds W.(n+1) in W .vertexAt(n).edgesInOut(); theorem :: GLIB_001:11 for n being odd Element of NAT st 1 < n & n <= len W holds W.(n- 1) in W.vertexAt(n).edgesInOut(); theorem :: GLIB_001:12 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; theorem :: GLIB_001:13 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; theorem :: GLIB_001:14 for e,x,y being object holds e Joins x,y,G implies len G.walkOf(x,e,y) = 3; theorem :: GLIB_001:15 for e,x,y being object holds e Joins x,y,G implies G.walkOf(x,e,y).first() = x & G.walkOf(x,e ,y).last() = y & G.walkOf(x,e,y) is_Walk_from x,y; theorem :: GLIB_001:16 for W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 .first() = W2.first() & W1.last() = W2.last(); theorem :: GLIB_001:17 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 x,y being object holds W is_Walk_from x,y implies x is Vertex of G & y is Vertex of G; theorem :: GLIB_001:19 for x,y being object holds for W1 being Walk of G1, 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 W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds for n being Element of NAT holds W1.vertexAt(n) = W2.vertexAt(n); theorem :: GLIB_001:21 len W = len W.reverse() & dom W = dom W.reverse() & rng W = rng W .reverse(); theorem :: GLIB_001:22 W.first() = W.reverse().last() & W.last() = W.reverse().first(); theorem :: GLIB_001:23 for x,y being object holds W is_Walk_from x,y iff W.reverse() is_Walk_from y, x; theorem :: GLIB_001:24 n in dom W implies W.n = W.reverse().(len W - n + 1) & (len W - n + 1) in dom W.reverse(); theorem :: GLIB_001:25 n in dom W.reverse() implies W.reverse().n = W.(len W - n + 1) & (len W - n + 1) in dom W; ::$CT theorem :: GLIB_001:27 for W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 .reverse() = W2.reverse(); theorem :: GLIB_001:28 W1.last() = W2.first() implies len W1.append(W2) + 1 = len W1 + len W2; theorem :: GLIB_001:29 W1.last() = W2.first() implies len W1 <= len W1.append(W2) & len W2 <= len W1.append(W2); theorem :: GLIB_001:30 W1.last() = W2.first() implies W1.append(W2).first() = W1.first() & W1 .append(W2).last() = W2.last() & W1.append(W2) is_Walk_from W1.first(), W2 .last(); theorem :: GLIB_001:31 for x,y,z being object holds W1 is_Walk_from x,y & W2 is_Walk_from y,z implies W1.append(W2) is_Walk_from x,z; theorem :: GLIB_001:32 n in dom W1 implies W1.append(W2).n = W1.n & n in dom W1.append(W2); theorem :: GLIB_001:33 W1.last() = W2.first() implies 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); theorem :: GLIB_001:34 n in dom W1.append(W2) implies n in dom W1 or ex k being Element of NAT st k < len W2 & n = len W1 + k; theorem :: GLIB_001:35 for W1A, W1B being Walk of G1, W2A,W2B being Walk of G2 st W1A = W2A & W1B = W2B holds W1A.append(W1B) = W2A.append(W2B); theorem :: GLIB_001:36 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; theorem :: GLIB_001:37 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; theorem :: GLIB_001:38 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); theorem :: GLIB_001:39 W.cut(1,len W) = W; theorem :: GLIB_001:40 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); theorem :: GLIB_001:41 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); theorem :: GLIB_001:42 for n being odd Element of NAT st n <= len W holds W.cut(n,n) = <* W .vertexAt(n) *>; theorem :: GLIB_001:43 m is odd & m <= n implies W.cut(1,n).cut(1,m) = W.cut(1,m); theorem :: GLIB_001:44 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); theorem :: GLIB_001:45 for m being odd Element of NAT st m <= len W holds len W.cut(1,m) = m; theorem :: GLIB_001:46 for m being odd Element of NAT, x being Element of NAT st x in dom W .cut(1,m) & m <= len W holds W.cut(1,m).x = W.x; theorem :: GLIB_001:47 for m,n being odd Element of NAT, 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; theorem :: GLIB_001:48 for W1 being Walk of G1, W2 being Walk of G2, m, n being Element of NAT st W1 = W2 holds W1.cut(m,n) = W2.cut(m,n); theorem :: GLIB_001:49 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; theorem :: GLIB_001:50 W is_Walk_from x,y implies W.remove(m,n) is_Walk_from x,y; theorem :: GLIB_001:51 len W.remove(m,n) <= len W; theorem :: GLIB_001:52 W.remove(m,m) = W; theorem :: GLIB_001:53 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(); theorem :: GLIB_001:54 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; theorem :: GLIB_001:55 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; theorem :: GLIB_001:56 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; theorem :: GLIB_001:57 for m being Element of NAT st W.m = W.last() holds W.remove(m, len W) = W.cut(1,m); theorem :: GLIB_001:58 for m being Element of NAT st W.first() = W.m holds W.remove(1,m) = W .cut(m, len W); theorem :: GLIB_001:59 W.remove(m,n).first() = W.first() & W.remove(m,n).last() = W.last(); theorem :: GLIB_001:60 for m,n being odd Element of NAT, x being Element of NAT st m <= n & n <= len W & W.m = W.n & x in dom W.remove(m,n) holds x in Seg m or m <= x & x <= len W.remove(m,n); theorem :: GLIB_001:61 for W1 being Walk of G1, W2 being Walk of G2, m, n being Element of NAT st W1 = W2 holds W1.remove(m,n) = W2.remove(m,n); theorem :: GLIB_001:62 for e,x being object holds e Joins W.last(), x, G implies W.addEdge(e) = W^<*e,x*>; theorem :: GLIB_001:63 for e,x being object holds e Joins W.last(),x,G implies W.addEdge(e).first() = W.first() & W .addEdge(e).last() = x & W.addEdge(e) is_Walk_from W.first(), x; theorem :: GLIB_001:64 for e,x being object holds e Joins W.last(),x,G implies len W.addEdge(e) = len W + 2; theorem :: GLIB_001:65 for e,x being object holds e Joins W.last(),x,G implies 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; theorem :: GLIB_001:66 for e,x,y,z being object holds W is_Walk_from x,y & e Joins y,z,G implies W.addEdge(e) is_Walk_from x ,z; theorem :: GLIB_001:67 1 <= len W.vertexSeq(); theorem :: GLIB_001:68 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 W.vertexSeq(); theorem :: GLIB_001:69 G.walkOf(v).vertexSeq() = <*v*>; theorem :: GLIB_001:70 for e,x,y being object holds e Joins x,y,G implies G.walkOf(x,e,y).vertexSeq() = <*x,y*>; theorem :: GLIB_001:71 W.first() = W.vertexSeq().1 & W.last() = W.vertexSeq().(len W .vertexSeq()); theorem :: GLIB_001:72 for n being odd Element of NAT st n <= len W holds W.vertexAt(n) = W .vertexSeq().((n+1) div 2); theorem :: GLIB_001:73 n in dom W.vertexSeq() iff 2*n-1 in dom W; theorem :: GLIB_001:74 W.cut(1,n).vertexSeq() c= W.vertexSeq(); theorem :: GLIB_001:75 e Joins W.last(),x,G implies W.addEdge(e).vertexSeq() = W .vertexSeq() ^ <*x*>; theorem :: GLIB_001:76 for W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 .vertexSeq() = W2.vertexSeq(); theorem :: GLIB_001:77 for n being even Element of NAT st 1 <= n & n <= len W holds n div 2 in dom W.edgeSeq() & W.n = W.edgeSeq().(n div 2); theorem :: GLIB_001:78 n in dom W.edgeSeq() iff 2*n in dom W; theorem :: GLIB_001:79 for n being Element of NAT st n in dom W.edgeSeq() holds W.edgeSeq().n in the_Edges_of G; theorem :: GLIB_001:80 ex lenWaa1 being even Element of NAT st lenWaa1 = len W - 1 & len W .edgeSeq() = lenWaa1 div 2; theorem :: GLIB_001:81 W.cut(1,n).edgeSeq() c= W.edgeSeq(); theorem :: GLIB_001:82 for e,x being object holds e Joins W.last(),x,G implies W.addEdge(e).edgeSeq() = W.edgeSeq() ^ <* e*>; theorem :: GLIB_001:83 for e,x,y being object holds e Joins x,y,G iff G.walkOf(x,e,y).edgeSeq() = <*e*>; theorem :: GLIB_001:84 W.reverse().edgeSeq() = Rev (W.edgeSeq()); theorem :: GLIB_001:85 W1.last() = W2.first() implies W1.append(W2).edgeSeq() = W1.edgeSeq() ^ W2.edgeSeq(); theorem :: GLIB_001:86 for W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 .edgeSeq() = W2.edgeSeq(); theorem :: GLIB_001:87 x in W.vertices() iff ex n being odd Element of NAT st n <= len W & W. n = x; theorem :: GLIB_001:88 W.first() in W.vertices() & W.last() in W.vertices(); theorem :: GLIB_001:89 for n being odd Element of NAT st n <= len W holds W.vertexAt(n) in W.vertices(); theorem :: GLIB_001:90 G.walkOf(v).vertices() = {v}; theorem :: GLIB_001:91 for e,x,y being object holds e Joins x,y,G implies G.walkOf(x,e,y).vertices() = {x,y}; theorem :: GLIB_001:92 W.vertices() = W.reverse().vertices(); theorem :: GLIB_001:93 W1.last() = W2.first() implies W1.append(W2).vertices() = W1 .vertices() \/ W2.vertices(); theorem :: GLIB_001:94 for m,n being odd Element of NAT st m <= n & n <= len W holds W.cut(m, n).vertices() c= W.vertices(); theorem :: GLIB_001:95 for e,x being object holds e Joins W.last(),x,G implies W.addEdge(e).vertices() = W .vertices() \/ {x}; theorem :: GLIB_001:96 for G being _Graph, W being Walk of G, e,x being set holds e Joins W.last(),x,G & not x in W.vertices() implies card W.addEdge(e).vertices() = card W.vertices() + 1; theorem :: GLIB_001:97 x in W.vertices() & y in W.vertices() implies ex W9 being Walk of G st W9 is_Walk_from x,y; theorem :: GLIB_001:98 for W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 .vertices() = W2.vertices(); theorem :: GLIB_001:99 e in W.edges() iff ex n being even Element of NAT st 1 <= n & n <= len W & W.n = e; theorem :: GLIB_001:100 e in W.edges() iff ex n being odd Element of NAT st n < len W & W.(n+1) = e; theorem :: GLIB_001:101 rng W = W.vertices() \/ W.edges(); theorem :: GLIB_001:102 W1.last() = W2.first() implies W1.append(W2).edges() = W1 .edges() \/ W2.edges(); theorem :: GLIB_001:103 e in W.edges() implies ex v1, v2 being Vertex of G, 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; theorem :: GLIB_001:104 e in W.edges() iff ex n being Element of NAT st n in dom W .edgeSeq() & W.edgeSeq().n = e; theorem :: GLIB_001:105 e in W.edges() & e Joins x,y,G implies x in W.vertices() & y in W .vertices(); theorem :: GLIB_001:106 W.cut(m,n).edges() c= W.edges(); theorem :: GLIB_001:107 W.edges() = W.reverse().edges(); theorem :: GLIB_001:108 for e,x,y being object holds e Joins x,y,G iff G.walkOf(x,e,y).edges() = {e}; theorem :: GLIB_001:109 W.edges() c= G.edgesBetween(W.vertices()); theorem :: GLIB_001:110 for W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 .edges() = W2.edges(); theorem :: GLIB_001:111 for e,x being object holds e Joins W.last(),x,G implies W.addEdge(e).edges() = W.edges() \/ {e}; theorem :: GLIB_001:112 len W = 2 * W.length() + 1; theorem :: GLIB_001:113 len W1 = len W2 iff W1.length() = W2.length(); theorem :: GLIB_001:114 for W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 .length() = W2.length(); theorem :: GLIB_001:115 for n being odd Element of NAT st n <= len W holds W.find(W.n) <= n & W.rfind(W.n) >= n; theorem :: GLIB_001:116 for W1 being Walk of G1, W2 being Walk of G2, v being set st W1 = W2 holds W1.find(v) = W2.find(v) & W1.rfind(v) = W2.rfind(v); theorem :: GLIB_001:117 for n being odd Element of NAT st n <= len W holds W.find(n) <= n & W.rfind(n) >= n; theorem :: GLIB_001:118 W is closed iff W.1 = W.(len W); theorem :: GLIB_001:119 W is closed iff ex x being set st W is_Walk_from x,x; theorem :: GLIB_001:120 W is closed iff W.reverse() is closed; theorem :: GLIB_001:121 for W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 & W1 is closed holds W2 is closed; theorem :: GLIB_001:122 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; theorem :: GLIB_001:123 W is directed & W is_Walk_from x,y & e DJoins y,z,G implies W.addEdge( e) is directed & W.addEdge(e) is_Walk_from x,z; theorem :: GLIB_001:124 for W being DWalk of G, m,n being Element of NAT holds W.cut(m,n) is directed; theorem :: GLIB_001:125 W is non trivial iff 3 <= len W; theorem :: GLIB_001:126 W is non trivial iff len W <> 1; theorem :: GLIB_001:127 W.first() <> W.last() implies W is non trivial; theorem :: GLIB_001:128 W is trivial iff ex v being Vertex of G st W = G.walkOf(v); theorem :: GLIB_001:129 W is trivial iff W.reverse() is trivial; theorem :: GLIB_001:130 W2 is trivial implies W1.append(W2) = W1; theorem :: GLIB_001:131 for m, n being odd Element of NAT st m <= n & n <= len W holds W.cut(m ,n) is trivial iff m = n; theorem :: GLIB_001:132 for e,x being object holds e Joins W.last(),x,G implies W.addEdge(e) is non trivial; theorem :: GLIB_001:133 W is non trivial implies ex lenW2 being odd Element of NAT st lenW2 = len W - 2 & W.cut(1,lenW2).addEdge(W.(lenW2+1)) = W; theorem :: GLIB_001:134 W2 is non trivial & W2.edges() c= W1.edges() implies W2 .vertices() c= W1.vertices(); theorem :: GLIB_001:135 W is non trivial implies for v being Vertex of G st v in W.vertices() holds not v is isolated; theorem :: GLIB_001:136 W is trivial iff W.edges() = {}; theorem :: GLIB_001:137 for W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 & W1 is trivial holds W2 is trivial; theorem :: GLIB_001:138 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; theorem :: GLIB_001:139 len W <= 3 implies W is Trail-like; theorem :: GLIB_001:140 W is Trail-like iff W.reverse() is Trail-like; theorem :: GLIB_001:141 for W being Trail of G, m,n being Element of NAT holds W.cut(m,n) is Trail-like; theorem :: GLIB_001:142 for W being Trail of G, e being set st e in W.last().edgesInOut() & not e in W.edges() holds W.addEdge(e) is Trail-like; theorem :: GLIB_001:143 for W being Trail of G, v being Vertex of G st v in W.vertices() & v is endvertex holds v = W.first() or v = W.last(); theorem :: GLIB_001:144 for G being _finite _Graph, W being Trail of G holds len W.edgeSeq() <= G.size(); theorem :: GLIB_001:145 len W <= 3 implies W is Path-like; theorem :: GLIB_001:146 (for m,n being odd Element of NAT st m <= len W & n <= len W & W.m = W .n holds m = n) implies W is Path-like; theorem :: GLIB_001:147 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; theorem :: GLIB_001:148 W is Path-like iff W.reverse() is Path-like; theorem :: GLIB_001:149 for W being Path of G, m, n being Element of NAT holds W.cut(m,n) is Path-like; theorem :: GLIB_001:150 for W being Path of G, e,v being object st e Joins W.last(),v,G & not e in W.edges() & (W is trivial 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; theorem :: GLIB_001:151 for W being Path of G, e, v being object st e Joins W.last(),v,G & not v in W.vertices() & (W is trivial or W is open) holds W.addEdge(e) is Path-like ; theorem :: GLIB_001:152 (for n being odd Element of NAT st n <= len W holds W.find(W.n) = W .rfind(W.n)) implies W is Path-like; theorem :: GLIB_001:153 (for n being odd Element of NAT st n <= len W holds W.rfind(n) = n) implies W is Path-like; theorem :: GLIB_001:154 for G being _finite _Graph, W being Path of G holds len W.vertexSeq() <= G.order() + 1; theorem :: GLIB_001:155 for G being _Graph, W being vertex-distinct Walk of G, e,v being object st e Joins W.last(),v,G & not v in W.vertices() holds W.addEdge(e) is vertex-distinct; theorem :: GLIB_001:156 for e,x being object holds e Joins x,x,G implies G.walkOf(x,e,x) is Cycle-like; theorem :: GLIB_001:157 e Joins x,y,G & e in W1.edges() & W1 is Cycle-like implies ex W2 being Walk of G st W2 is_Walk_from x,y & not e in W2.edges(); theorem :: GLIB_001:158 W is Subwalk of W; theorem :: GLIB_001:159 for W1 being Walk of G, W2 being Subwalk of W1, W3 being Subwalk of W2 holds W3 is Subwalk of W1; theorem :: GLIB_001:160 W1 is Subwalk of W2 implies (W1 is_Walk_from x,y iff W2 is_Walk_from x ,y); theorem :: GLIB_001:161 W1 is Subwalk of W2 implies W1.first() = W2.first() & W1.last() = W2.last(); theorem :: GLIB_001:162 W1 is Subwalk of W2 implies len W1 <= len W2; theorem :: GLIB_001:163 W1 is Subwalk of W2 implies W1.edges() c= W2.edges() & W1 .vertices() c= W2.vertices(); theorem :: GLIB_001:164 W1 is Subwalk of W2 implies 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; theorem :: GLIB_001:165 W1 is Subwalk of W2 implies 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; theorem :: GLIB_001:166 for W1 being Trail of G st W1 is non trivial holds ex W2 being Path of W1 st W2 is non trivial; theorem :: GLIB_001:167 for G1 being _Graph, G2 being Subgraph of G1, W being Walk of G2 holds W is Walk of G1; theorem :: GLIB_001:168 for G1 being _Graph, G2 being Subgraph of G1, W being Walk of G1 st W is trivial & W.first() in the_Vertices_of G2 holds W is Walk of G2; theorem :: GLIB_001:169 for G1 being _Graph, G2 being Subgraph of G1, W being Walk of G1 st W is non trivial & W.edges() c= the_Edges_of G2 holds W is Walk of G2; theorem :: GLIB_001:170 for G1 being _Graph, G2 being Subgraph of G1, 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; theorem :: GLIB_001:171 for G1 being non _trivial _Graph, W being Walk of G1, v being Vertex of G1, G2 being removeVertex of G1,v st not v in W.vertices() holds W is Walk of G2; theorem :: GLIB_001:172 for G1 being _Graph, W being Walk of G1, e being set, G2 being removeEdge of G1,e st not e in W.edges() holds W is Walk of G2; theorem :: GLIB_001:173 for G1 being _Graph, G2 being Subgraph of G1, x,y,e being set st e Joins x,y,G2 holds G1.walkOf(x, e, y) = G2.walkOf(x, e, y); theorem :: GLIB_001:174 for G1 being _Graph, G2 being Subgraph of G1, W1 being Walk of G1, W2 being Walk of G2, e being set st W1 = W2 & e in W2.last().edgesInOut() holds W1 .addEdge(e) = W2.addEdge(e); theorem :: GLIB_001:175 for G1 being _Graph, G2 being Subgraph of G1, 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 trivial implies W is trivial 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); theorem :: GLIB_001:176 for G1 being _Graph, G2 being Subgraph of G1, W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds (W1 is closed iff W2 is closed) & (W1 is directed iff W2 is directed) & (W1 is trivial iff W2 is trivial) & (W1 is Trail-like iff W2 is Trail-like) & (W1 is Path-like iff W2 is Path-like) & (W1 is vertex-distinct iff W2 is vertex-distinct); theorem :: GLIB_001:177 G1 == G2 & x is VertexSeq of G1 implies x is VertexSeq of G2; theorem :: GLIB_001:178 G1 == G2 & x is EdgeSeq of G1 implies x is EdgeSeq of G2; theorem :: GLIB_001:179 G1 == G2 & x is Walk of G1 implies x is Walk of G2; theorem :: GLIB_001:180 G1 == G2 implies G1.walkOf(x,e,y) = G2.walkOf(x,e,y); theorem :: GLIB_001:181 for W1 being Walk of G1, W2 being Walk of G2 st G1 == G2 & W1 = W2 holds (W1 is closed iff W2 is closed) & (W1 is directed iff W2 is directed) & ( W1 is trivial iff W2 is trivial) & (W1 is Trail-like iff W2 is Trail-like) & ( W1 is Path-like iff W2 is Path-like) & (W1 is vertex-distinct iff W2 is vertex-distinct);