Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Euler Circuits and Paths

**by****Yatsuka Nakamura, and****Piotr Rudnicki**- Received July 29, 1997
- MML identifier: GRAPH_3

- [ Mizar article, MML identifier index ]

environ vocabulary FINSEQ_2, FINSEQ_1, MATRIX_2, INT_1, ARYTM_1, RELAT_1, GRAPH_2, FUNCT_1, BOOLE, GRAPH_1, MSAFREE2, ORDERS_1, RELAT_2, PARTFUN1, FINSET_1, CARD_1, FUNCT_4, CAT_1, FUNCOP_1, TARSKI, FINSEQ_6, NEWTON, SQUARE_1, GRAPH_3, FINSEQ_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, CQC_LANG, FUNCT_4, NAT_1, INT_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, GRAPH_1, GRAPH_2, MSSCYC_1, PRE_CIRC, ABIAN; constructors GRAPH_2, MSSCYC_1, WELLORD2, BINARITH, CQC_LANG, PRE_CIRC, ABIAN, WELLFND1, FINSEQ_4, INT_1; clusters SUBSET_1, GRAPH_2, RELSET_1, FINSET_1, FINSEQ_5, CARD_1, MSSCYC_1, INT_1, ABIAN, CQC_LANG, FINSEQ_1, NAT_1, XREAL_0, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Preliminaries definition let D be set, T be FinSequence-DOMAIN of D, S be non empty Subset of T; redefine mode Element of S -> FinSequence of D; end; definition 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 Vertices 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 Vertices 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; canceled 3; theorem :: GRAPH_3:7 e in the Edges of G implies <*e*> is Path of G; theorem :: GRAPH_3:8 (m,n)-cut p is Path of G; theorem :: GRAPH_3:9 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; canceled 2; theorem :: GRAPH_3:12 c = {} implies c is cyclic; definition let G be Graph; cluster cyclic Path of G; end; theorem :: GRAPH_3:13 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:14 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:15 for p being cyclic Path of G st n in dom p ex p' being cyclic Path of G st p'.1 = p.n & len p' = len p & rng p' = rng p; theorem :: GRAPH_3:16 :: 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:17 e in the Edges of G & vs is_vertex_seq_of c & vs.len vs = (the Source of G).e implies c^<*e*> is Chain of G & ex vs' being FinSequence of the Vertices of G st vs' = vs^'<*(the Source of G).e, (the Target of G).e*> & vs' is_vertex_seq_of c^<*e*> & vs'.1 = vs.1 & vs'.len vs' = (the Target of G).e; theorem :: GRAPH_3:18 e in the Edges of G & vs is_vertex_seq_of c & vs.len vs = (the Target of G).e implies c^<*e*> is Chain of G & ex vs' being FinSequence of the Vertices of G st vs' = vs^'<*(the Target of G).e, (the Source of G).e*> & vs' is_vertex_seq_of c^<*e*> & vs'.1 = vs.1 & vs'.len vs' = (the Source of G).e; theorem :: GRAPH_3:19 vs is_vertex_seq_of c implies for n being 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:20 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 Vertices of G; end; theorem :: GRAPH_3:21 G-VSet {} = {}; theorem :: GRAPH_3:22 e in the Edges of G & e in X implies G-VSet X is non empty; theorem :: GRAPH_3:23 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:24 for G being connected Graph, X being set, v being Vertex of G st X meets the Edges of G & not v in G-VSet X ex v' being Vertex of G, e being Element of the Edges of G st v' in G-VSet X & not e in X & (v' = (the Target of G).e or v' = (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 Edges of G means :: GRAPH_3:def 1 for e being set holds e in it iff e in the Edges of G & e in X & (the Target of G).e = v; func Edges_Out(v, X) -> Subset of the Edges of G means :: GRAPH_3:def 2 for e being set holds e in it iff e in the Edges 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 Edges of G equals :: GRAPH_3:def 3 Edges_In(v, X) \/ Edges_Out(v, X); end; definition 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; definition 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 Edges of G equals :: GRAPH_3:def 4 Edges_In(v, the Edges of G); func Edges_Out v -> Subset of the Edges of G equals :: GRAPH_3:def 5 Edges_Out(v, the Edges of G); end; theorem :: GRAPH_3:25 Edges_In(v, X) c= Edges_In v; theorem :: GRAPH_3:26 Edges_Out(v, X) c= Edges_Out v; definition 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 Vertices of G, X1, X2 for set; theorem :: GRAPH_3:27 card Edges_In v = EdgesIn v; theorem :: GRAPH_3:28 card Edges_Out v = EdgesOut v; definition let G be finite Graph, v be Vertex of G, X be set; func Degree(v, X) -> Nat equals :: GRAPH_3:def 6 card Edges_In(v, X) + card Edges_Out(v, X); end; theorem :: GRAPH_3:29 Degree v = Degree(v, the Edges of G); theorem :: GRAPH_3:30 Degree(v, X) <> 0 implies Edges_At(v, X) is non empty; theorem :: GRAPH_3:31 e in the Edges 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:32 X2 c= X1 implies card Edges_In(v, X1\X2) = card Edges_In(v, X1) - card Edges_In(v, X2); theorem :: GRAPH_3:33 X2 c= X1 implies card Edges_Out(v, X1\X2) = card Edges_Out(v, X1) - card Edges_Out(v, X2); theorem :: GRAPH_3:34 X2 c= X1 implies Degree(v, X1 \ X2) = Degree(v, X1) - Degree(v, X2); theorem :: GRAPH_3:35 Edges_In(v, X) = Edges_In(v, X/\the Edges of G) & Edges_Out(v, X) = Edges_Out(v, X/\the Edges of G); theorem :: GRAPH_3:36 Degree(v, X) = Degree(v, X/\the Edges of G); theorem :: GRAPH_3:37 c is non empty & vs is_vertex_seq_of c implies (v in rng vs iff Degree(v, rng c) <> 0); theorem :: GRAPH_3:38 for G being non empty 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 Vertices of it = the Vertices of G & the Edges of it = (the Edges of G) \/ {the Edges of G} & the Source of it = (the Source of G) +* ((the Edges of G) .--> v1) & the Target of it = (the Target of G) +* ((the Edges of G) .--> v2); end; definition 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 Vertices of G, v' for Vertex of AddNewEdge(v1, v2), p' for Path of AddNewEdge(v1, v2), vs' for FinSequence of the Vertices of AddNewEdge(v1, v2); theorem :: GRAPH_3:39 (the Edges of G) in the Edges of AddNewEdge(v1, v2) & the Edges of G = (the Edges of AddNewEdge(v1, v2)) \ {the Edges of G} & (the Source of AddNewEdge(v1, v2)).(the Edges of G) = v1 & (the Target of AddNewEdge(v1, v2)).(the Edges of G) = v2; theorem :: GRAPH_3:40 e in the Edges 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:41 vs' = vs & vs is_vertex_seq_of c implies vs' is_vertex_seq_of c; theorem :: GRAPH_3:42 c is Chain of AddNewEdge(v1, v2); theorem :: GRAPH_3:43 p is Path of AddNewEdge(v1, v2); theorem :: GRAPH_3:44 v' = v1 & v1 <> v2 implies Edges_In(v', X) = Edges_In(v1, X); theorem :: GRAPH_3:45 v' = v2 & v1 <> v2 implies Edges_Out(v', X) = Edges_Out(v2, X); theorem :: GRAPH_3:46 v' = v1 & v1 <> v2 & (the Edges of G) in X implies Edges_Out(v', X) = Edges_Out(v1, X) \/ {the Edges of G} & Edges_Out(v1, X) misses {the Edges of G}; theorem :: GRAPH_3:47 v' = v2 & v1 <> v2 & (the Edges of G) in X implies Edges_In(v', X) = Edges_In(v2, X) \/ {the Edges of G} & Edges_In(v2, X) misses {the Edges of G}; theorem :: GRAPH_3:48 v' = v & v <> v1 & v <> v2 implies Edges_In(v', X) = Edges_In(v, X); theorem :: GRAPH_3:49 v' = v & v <> v1 & v <> v2 implies Edges_Out(v', X) = Edges_Out(v, X); theorem :: GRAPH_3:50 not (the Edges of G) in rng p' implies p' is Path of G; theorem :: GRAPH_3:51 not (the Edges of G) in rng p' & vs = vs' & vs' is_vertex_seq_of p' implies vs is_vertex_seq_of p'; definition 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 Vertices of G, v' for Vertex of AddNewEdge(v1, v2); theorem :: GRAPH_3:52 v' = v & v1 <> v2 & (v = v1 or v = v2) & (the Edges of G) in X implies Degree(v', X) = Degree(v, X) +1; theorem :: GRAPH_3:53 v' = v & v <> v1 & v <> v2 implies Degree(v', X) = Degree(v, X); begin theorem :: GRAPH_3:54 :: CycVerDeg1 for c being cyclic Path of G holds Degree(v, rng c) is even; theorem :: GRAPH_3:55 :: 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 Vertices of G; definition let G be Graph; func G-CycleSet -> FinSequence-DOMAIN of the Edges 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:56 {} is Element of G-CycleSet; theorem :: GRAPH_3:57 for c being Element of G-CycleSet st v in G-VSet rng c holds { c' where c' is Element of G-CycleSet : rng c' = rng c & ex vs st vs is_vertex_seq_of c' & 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 choose { c' where c' is Element of G-CycleSet : rng c' = rng c & ex vs st vs is_vertex_seq_of c' & 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 = choose ((G-VSet rng c1) /\ (G-VSet rng c2)) & it = Rotate(c1, v)^Rotate(c2, v); end; theorem :: GRAPH_3:58 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 Vertices of G; definition let G, v; let X be set; assume that Degree(v, X) <> 0; func X-PathSet v -> FinSequence-DOMAIN of the Edges 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:59 for p being Element of X-PathSet v, Y being finite set st Y = the Edges 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:60 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:61 for G be finite connected Graph, c be Element of G-CycleSet st rng c <> the Edges of G & c is non empty holds {v' where v' is Vertex of G : v' in G-VSet rng c & Degree v' <> Degree(v', rng c)} is non empty Subset of the Vertices of G; definition let G be finite connected Graph, c be Element of G-CycleSet; assume that rng c <> the Edges of G and c is non empty; func ExtendCycle c -> Element of G-CycleSet means :: GRAPH_3:def 13 ex c' being Element of G-CycleSet, v being Vertex of G st v = choose {v' where v' is Vertex of G : v' in G-VSet rng c & Degree v' <> Degree(v', rng c)} & c' = choose (((the Edges of G) \ rng c)-CycleSet v) & it = CatCycles(c, c'); end; theorem :: GRAPH_3:62 for G being finite connected Graph, c being Element of G-CycleSet st rng c <> the Edges 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 Edges of G; end; theorem :: GRAPH_3:63 for G being connected Graph, p being Path of G, vs being FinSequence of the Vertices of G st p is Eulerian & vs is_vertex_seq_of p holds rng vs = the Vertices of G; theorem :: GRAPH_3:64 :: 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:65 :: 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);

Back to top