:: Euler circuits and paths :: by Yatsuka Nakamura and Piotr Rudnicki :: :: Received July 29, 1997 :: Copyright (c) 1997-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, FINSEQ_2, XBOOLE_0, SUBSET_1, FINSEQ_1, ABIAN, INT_1, ARYTM_1, RELAT_1, XXREAL_0, ARYTM_3, GRAPH_2, FUNCT_1, CARD_1, GRAPH_1, GLIB_000, STRUCT_0, TREES_2, ORDINAL4, NAT_1, PARTFUN1, TARSKI, RELAT_2, FINSET_1, FUNCT_4, FUNCOP_1, ZFMISC_1, FINSEQ_6, GRAPH_3; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, INT_1, NAT_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, XXREAL_2, STRUCT_0, GRAPH_1, GRAPH_2, MSSCYC_1, ABIAN, XXREAL_0, FINSEQ_6; constructors WELLORD2, FUNCT_4, FINSEQ_4, ABIAN, GRAPH_2, MSSCYC_1, XXREAL_2, RELSET_1, PRE_POLY, FINSEQ_6; registrations XBOOLE_0, ORDINAL1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, FINSEQ_1, ABIAN, GRAPH_2, MSSCYC_1, RELAT_1, XXREAL_2, STRUCT_0, RELSET_1, FINSEQ_2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Preliminaries definition let D be set, T be non empty FinSequenceSet of D, S be non empty Subset of T; redefine mode Element of S -> FinSequence of D; end; registration let i, j be even Integer; cluster i-j -> even; end; theorem :: GRAPH_3:1 for i, j being Integer holds (i is even iff j is even) iff (i-j) is even; theorem :: GRAPH_3:2 for p being FinSequence, m, n, a being Nat st a in dom (m, n)-cut p ex k being Nat st k in dom p & p.k = ((m,n)-cut p).a & k+1 = m+a & m <= k & k <= n; definition let G be Graph; mode Vertex of G is Element of the carrier of G; end; reserve G for Graph, v, v1, v2 for Vertex of G, c for Chain of G, p, p1, p2 for Path of G, vs, vs1, vs2 for FinSequence of the carrier of G, e, X for set, n, m for Nat; theorem :: GRAPH_3:3 vs is_vertex_seq_of c implies vs is non empty; theorem :: GRAPH_3:4 e in the carrier' of G implies <*e*> is Path of G; theorem :: GRAPH_3:5 (m,n)-cut p is Path of G; theorem :: GRAPH_3:6 rng p1 misses rng p2 & vs1 is_vertex_seq_of p1 & vs2 is_vertex_seq_of p2 & vs1.len vs1 = vs2.1 implies p1^p2 is Path of G; theorem :: GRAPH_3:7 c = {} implies c is cyclic; registration let G be Graph; cluster cyclic for Path of G; end; theorem :: GRAPH_3:8 for p being cyclic Path of G holds ((m+1,len p)-cut p)^(1,m)-cut p is cyclic Path of G; theorem :: GRAPH_3:9 m+1 in dom p implies len (((m+1,len p)-cut p)^(1,m)-cut p) = len p & rng (((m+1,len p)-cut p)^(1,m)-cut p) = rng p & (((m+1,len p)-cut p)^(1,m) -cut p).1 = p.(m+1); theorem :: GRAPH_3:10 for p being cyclic Path of G st n in dom p ex p9 being cyclic Path of G st p9.1 = p.n & len p9 = len p & rng p9 = rng p; theorem :: GRAPH_3:11 :: see MSSCYC_1:4 for s, t being Vertex of G st s = (the Source of G).e & t = (the Target of G).e holds <*t, s*> is_vertex_seq_of <*e*>; theorem :: GRAPH_3:12 e in the carrier' of G & vs is_vertex_seq_of c & vs.len vs = ( the Source of G).e implies c^<*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st vs9 = vs^'<*(the Source of G).e, (the Target of G).e*> & vs9 is_vertex_seq_of c^<*e*> & vs9.1 = vs.1 & vs9.len vs9 = (the Target of G).e ; theorem :: GRAPH_3:13 e in the carrier' of G & vs is_vertex_seq_of c & vs.len vs = ( the Target of G).e implies c^<*e*> is Chain of G & ex vs9 being FinSequence of the carrier of G st vs9 = vs^'<*(the Target of G).e, (the Source of G).e*> & vs9 is_vertex_seq_of c^<*e*> & vs9.1 = vs.1 & vs9.len vs9 = (the Source of G).e ; theorem :: GRAPH_3:14 vs is_vertex_seq_of c implies for n being Element of NAT st n in dom c holds (vs.n = (the Target of G).(c.n) & vs.(n+1) = (the Source of G).(c.n) or vs.n = (the Source of G).(c.n) & vs.(n+1) = (the Target of G).(c.n)); theorem :: GRAPH_3:15 vs is_vertex_seq_of c & e in rng c implies (the Target of G).e in rng vs & (the Source of G).e in rng vs; definition let G be Graph, X be set; redefine func G-VSet X -> Subset of the carrier of G; end; theorem :: GRAPH_3:16 G-VSet {} = {}; theorem :: GRAPH_3:17 e in the carrier' of G & e in X implies G-VSet X is non empty; theorem :: GRAPH_3:18 G is connected iff for v1, v2 st v1 <> v2 ex c, vs st c is non empty & vs is_vertex_seq_of c & vs.1 = v1 & vs.len vs = v2; theorem :: GRAPH_3:19 for G being connected Graph, X being set, v being Vertex of G st X meets the carrier' of G & not v in G-VSet X ex v9 being Vertex of G, e being Element of the carrier' of G st v9 in G-VSet X & not e in X & (v9 = (the Target of G).e or v9 = (the Source of G).e); begin :: Degree of a vertex definition let G be Graph, v be Vertex of G, X be set; func Edges_In(v, X) -> Subset of the carrier' of G means :: GRAPH_3:def 1 for e being set holds e in it iff e in the carrier' of G & e in X & (the Target of G).e = v ; func Edges_Out(v, X) -> Subset of the carrier' of G means :: GRAPH_3:def 2 for e being set holds e in it iff e in the carrier' of G & e in X & (the Source of G).e = v ; end; definition let G be Graph, v be Vertex of G, X be set; func Edges_At(v, X) -> Subset of the carrier' of G equals :: GRAPH_3:def 3 Edges_In(v, X) \/ Edges_Out(v, X); end; registration let G be finite Graph, v be Vertex of G, X be set; cluster Edges_In(v, X) -> finite; cluster Edges_Out(v, X) -> finite; cluster Edges_At(v, X) -> finite; end; registration let G be Graph, v be Vertex of G, X be empty set; cluster Edges_In(v, X) -> empty; cluster Edges_Out(v, X) -> empty; cluster Edges_At(v, X) -> empty; end; definition let G be Graph, v be Vertex of G; func Edges_In v -> Subset of the carrier' of G equals :: GRAPH_3:def 4 Edges_In(v, the carrier' of G); func Edges_Out v -> Subset of the carrier' of G equals :: GRAPH_3:def 5 Edges_Out(v, the carrier' of G); end; theorem :: GRAPH_3:20 Edges_In(v, X) c= Edges_In v; theorem :: GRAPH_3:21 Edges_Out(v, X) c= Edges_Out v; registration let G be finite Graph, v be Vertex of G; cluster Edges_In v -> finite; cluster Edges_Out v -> finite; end; reserve G for finite Graph, v for Vertex of G, c for Chain of G, vs for FinSequence of the carrier of G, X1, X2 for set; theorem :: GRAPH_3:22 card Edges_In v = EdgesIn v; theorem :: GRAPH_3:23 card Edges_Out v = EdgesOut v; definition let G be finite Graph, v be Vertex of G, X be set; func Degree(v, X) -> Element of NAT equals :: GRAPH_3:def 6 card Edges_In(v, X) + card Edges_Out(v, X); end; theorem :: GRAPH_3:24 Degree v = Degree(v, the carrier' of G); theorem :: GRAPH_3:25 Degree(v, X) <> 0 implies Edges_At(v, X) is non empty; theorem :: GRAPH_3:26 e in the carrier' of G & not e in X & (v = (the Target of G).e or v = (the Source of G).e) implies Degree v <> Degree(v, X); theorem :: GRAPH_3:27 X2 c= X1 implies card Edges_In(v, X1\X2) = card Edges_In(v, X1) - card Edges_In(v, X2); theorem :: GRAPH_3:28 X2 c= X1 implies card Edges_Out(v, X1\X2) = card Edges_Out(v, X1 ) - card Edges_Out(v, X2); theorem :: GRAPH_3:29 X2 c= X1 implies Degree(v, X1 \ X2) = Degree(v, X1) - Degree(v, X2); theorem :: GRAPH_3:30 Edges_In(v, X) = Edges_In(v, X/\the carrier' of G) & Edges_Out(v , X) = Edges_Out(v, X/\the carrier' of G); theorem :: GRAPH_3:31 Degree(v, X) = Degree(v, X/\the carrier' of G); theorem :: GRAPH_3:32 c is non empty & vs is_vertex_seq_of c implies (v in rng vs iff Degree(v, rng c) <> 0); theorem :: GRAPH_3:33 for G being non void finite connected Graph, v being Vertex of G holds Degree v <> 0; begin :: Adding an edge to a graph definition let G be Graph, v1, v2 be Vertex of G; func AddNewEdge(v1, v2) -> strict Graph means :: GRAPH_3:def 7 the carrier of it = the carrier of G & the carrier' of it = (the carrier' of G) \/ {the carrier' of G} & the Source of it = (the Source of G) +* ((the carrier' of G) .--> v1) & the Target of it = (the Target of G) +* ((the carrier' of G) .--> v2); end; registration let G be finite Graph, v1, v2 be Vertex of G; cluster AddNewEdge(v1, v2) -> finite; end; reserve G for Graph, v, v1, v2 for Vertex of G, c for Chain of G, p for Path of G, vs for FinSequence of the carrier of G, v9 for Vertex of AddNewEdge(v1, v2), p9 for Path of AddNewEdge(v1, v2), vs9 for FinSequence of the carrier of AddNewEdge(v1, v2); theorem :: GRAPH_3:34 (the carrier' of G) in the carrier' of AddNewEdge(v1, v2) & the carrier' of G = (the carrier' of AddNewEdge(v1, v2)) \ {the carrier' of G} & ( the Source of AddNewEdge(v1, v2)).(the carrier' of G) = v1 & (the Target of AddNewEdge(v1, v2)).(the carrier' of G) = v2; theorem :: GRAPH_3:35 e in the carrier' of G implies (the Source of AddNewEdge(v1, v2) ).e = (the Source of G).e & (the Target of AddNewEdge(v1, v2)).e = (the Target of G).e; theorem :: GRAPH_3:36 vs9 = vs & vs is_vertex_seq_of c implies vs9 is_vertex_seq_of c; theorem :: GRAPH_3:37 c is Chain of AddNewEdge(v1, v2); theorem :: GRAPH_3:38 p is Path of AddNewEdge(v1, v2); theorem :: GRAPH_3:39 v9 = v1 & v1 <> v2 implies Edges_In(v9, X) = Edges_In(v1, X); theorem :: GRAPH_3:40 v9 = v2 & v1 <> v2 implies Edges_Out(v9, X) = Edges_Out(v2, X); theorem :: GRAPH_3:41 v9 = v1 & (the carrier' of G) in X implies Edges_Out(v9, X) = Edges_Out(v1, X) \/ {the carrier' of G} & Edges_Out(v1, X) misses {the carrier' of G}; theorem :: GRAPH_3:42 v9 = v2 & (the carrier' of G) in X implies Edges_In(v9, X) = Edges_In(v2, X) \/ {the carrier' of G} & Edges_In(v2, X) misses {the carrier' of G}; theorem :: GRAPH_3:43 v9 = v & v <> v2 implies Edges_In(v9, X) = Edges_In(v, X); theorem :: GRAPH_3:44 v9 = v & v <> v1 implies Edges_Out(v9, X) = Edges_Out(v, X); theorem :: GRAPH_3:45 not (the carrier' of G) in rng p9 implies p9 is Path of G; theorem :: GRAPH_3:46 not (the carrier' of G) in rng p9 & vs = vs9 & vs9 is_vertex_seq_of p9 implies vs is_vertex_seq_of p9; registration let G be connected Graph, v1, v2 be Vertex of G; cluster AddNewEdge(v1, v2) -> connected; end; reserve G for finite Graph, v, v1, v2 for Vertex of G, vs for FinSequence of the carrier of G, v9 for Vertex of AddNewEdge(v1, v2); theorem :: GRAPH_3:47 v9 = v & v1 <> v2 & (v = v1 or v = v2) & (the carrier' of G) in X implies Degree(v9, X) = Degree(v, X) +1; theorem :: GRAPH_3:48 v9 = v & v <> v1 & v <> v2 implies Degree(v9, X) = Degree(v, X); begin theorem :: GRAPH_3:49 :: CycVerDeg1 for c being cyclic Path of G holds Degree(v, rng c) is even; theorem :: GRAPH_3:50 :: CycVerDeg2 for c being Path of G st c is non cyclic & vs is_vertex_seq_of c holds Degree(v, rng c) is even iff v <> vs.1 & v <> vs.len vs; reserve G for Graph, v for Vertex of G, vs for FinSequence of the carrier of G; definition let G be Graph; func G-CycleSet -> FinSequenceSet of the carrier' of G means :: GRAPH_3:def 8 for x being set holds x in it iff x is cyclic Path of G; end; theorem :: GRAPH_3:51 {} in G-CycleSet; registration let G be Graph; cluster G-CycleSet -> non empty; end; theorem :: GRAPH_3:52 for c being Element of G-CycleSet st v in G-VSet rng c holds { c9 where c9 is Element of G-CycleSet : rng c9 = rng c & ex vs st vs is_vertex_seq_of c9 & vs.1 = v} is non empty Subset of G-CycleSet; definition let G, v; let c be Element of G-CycleSet; assume v in G-VSet rng c; func Rotate(c, v) -> Element of G-CycleSet equals :: GRAPH_3:def 9 the Element of { c9 where c9 is Element of G-CycleSet : rng c9 = rng c & ex vs st vs is_vertex_seq_of c9 & vs.1 = v }; end; definition let G be Graph, c1, c2 be Element of G-CycleSet; assume that G-VSet rng c1 meets G-VSet rng c2 and rng c1 misses rng c2; func CatCycles(c1, c2) -> Element of G-CycleSet means :: GRAPH_3:def 10 ex v being Vertex of G st v = the Element of (G-VSet rng c1) /\ (G-VSet rng c2) & it = Rotate(c1 , v)^Rotate(c2, v); end; theorem :: GRAPH_3:53 for G being Graph, c1, c2 be Element of G-CycleSet st G-VSet rng c1 meets G-VSet rng c2 & rng c1 misses rng c2 & (c1 <> {} or c2 <> {}) holds CatCycles(c1, c2) is non empty; reserve G for finite Graph, v for Vertex of G, vs for FinSequence of the carrier of G; definition let G, v; let X be set; assume Degree(v, X) <> 0; func X-PathSet v -> non empty FinSequenceSet of the carrier' of G equals :: GRAPH_3:def 11 { c where c is Element of X* : c is Path of G & c is non empty & ex vs st vs is_vertex_seq_of c & vs.1 = v }; end; theorem :: GRAPH_3:54 for p being Element of X-PathSet v, Y being finite set st Y = the carrier' of G & Degree(v, X) <> 0 holds len p <= card Y; definition let G, v; let X be set; assume that for v being Vertex of G holds Degree(v, X) is even and Degree(v, X) <> 0; func X-CycleSet v -> non empty Subset of G-CycleSet equals :: GRAPH_3:def 12 { c where c is Element of G-CycleSet : rng c c= X & c is non empty & ex vs st vs is_vertex_seq_of c & vs.1 = v }; end; theorem :: GRAPH_3:55 Degree(v, X) <> 0 & (for v holds Degree(v, X) is even) implies for c being Element of X-CycleSet v holds c is non empty & rng c c= X & v in G -VSet rng c; theorem :: GRAPH_3:56 for G be finite connected Graph, c be Element of G-CycleSet st rng c <> the carrier' of G & c is non empty holds {v9 where v9 is Vertex of G : v9 in G-VSet rng c & Degree v9 <> Degree(v9, rng c)} is non empty Subset of the carrier of G; definition let G be finite connected Graph, c be Element of G-CycleSet; assume that rng c <> the carrier' of G and c is non empty; func ExtendCycle c -> Element of G-CycleSet means :: GRAPH_3:def 13 ex c9 being Element of G-CycleSet, v being Vertex of G st v = the Element of {v9 where v9 is Vertex of G : v9 in G-VSet rng c & Degree v9 <> Degree(v9, rng c)} & c9 = the Element of (( the carrier' of G) \ rng c)-CycleSet v & it = CatCycles(c, c9); end; theorem :: GRAPH_3:57 for G being finite connected Graph, c being Element of G -CycleSet st rng c <> the carrier' of G & c is non empty & for v being Vertex of G holds Degree v is even holds ExtendCycle c is non empty & card rng c < card rng ExtendCycle c; begin :: Euler paths definition let G be Graph; let p be Path of G; attr p is Eulerian means :: GRAPH_3:def 14 rng p = the carrier' of G; end; theorem :: GRAPH_3:58 for G being connected Graph, p being Path of G, vs being FinSequence of the carrier of G st p is Eulerian & vs is_vertex_seq_of p holds rng vs = the carrier of G; theorem :: GRAPH_3:59 :: Cyclic Euler paths for G being finite connected Graph holds (ex p being cyclic Path of G st p is Eulerian) iff for v being Vertex of G holds Degree v is even; theorem :: GRAPH_3:60 :: Non-cyclic Euler paths for G being finite connected Graph holds (ex p being Path of G st p is non cyclic & p is Eulerian) iff ex v1, v2 being Vertex of G st v1 <> v2 & for v being Vertex of G holds Degree v is even iff v<>v1 & v <> v2;