:: Euler circuits and paths
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received July 29, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

definition
let D be set ;
let T be non empty FinSequenceSet of D;
let S be non empty Subset of T;
:: original:Element
redefine mode Element of S ->  FinSequence of D;
coherence
 for b1 being Element of S holds b1 is FinSequence of D
proofend;
end;

registration
let i, j be even Integer;
clusteri - j ->  even ;
coherence
 i - j is even
proofend;
end;

theorem :: GRAPH_3:1
for i, j being Integer holds
( ( i is even iff j is even ) iff i - j is even ) ;

Lm1:  for p being FinSequence
for m, n being Element of NAT st 1 <= m &amp; m <= n + 1 &amp; n <= len p holds
( (len ((m,n) -cut p)) + m = n + 1 &amp; ( for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
proofend;

theorem Th2: :: GRAPH_3:2
for p being FinSequence
for m, n, a being Element of NAT st a in dom ((m,n) -cut p) holds
ex k being Element of NAT st
( k in dom p &amp; p . k = ((m,n) -cut p) . a &amp; k + 1 = m + a &amp; m <= k &amp; k <= n )
proofend;

definition
let G be Graph;
mode Vertex of G is Element of the carrier of G;
end;

theorem Th3: :: GRAPH_3:3
for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G st vs is_vertex_seq_of c holds
not vs is empty
proofend;

Lm2:  for G being Graph
for p being Path of G
for n, m being Element of NAT st 1 <= n &amp; n <= len p &amp; 1 <= m &amp; m <= len p &amp; n <> m holds
p . n <> p . m
proofend;

theorem Th4: :: GRAPH_3:4
for G being Graph
for e being set st e in the carrier' of G holds
<*e*> is Path of G
proofend;

theorem Th5: :: GRAPH_3:5
for G being Graph
for p being Path of G
for m, n being Element of NAT holds (m,n) -cut p is Path of G
proofend;

theorem Th6: :: GRAPH_3:6
for G being Graph
for p1, p2 being Path of G
for vs1, vs2 being FinSequence of the carrier of G st rng p1 misses rng p2 &amp; vs1 is_vertex_seq_of p1 &amp; vs2 is_vertex_seq_of p2 &amp; vs1 . (len vs1) = vs2 . 1 holds
p1 ^ p2 is Path of G
proofend;

theorem Th7: :: GRAPH_3:7
for G being Graph
for c being Chain of G st c = {} holds
c is cyclic
proofend;

registration
let G be Graph;
cluster Relation-like NAT -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like cyclic for Chain of G;
existence
 ex b1 being Path of G st b1 is cyclic
proofend;
end;

theorem Th8: :: GRAPH_3:8
for G being Graph
for m being Element of NAT
for p being cyclic Path of G holds (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G
proofend;

theorem Th9: :: GRAPH_3:9
for G being Graph
for p being Path of G
for m being Element of NAT st m + 1 in dom p holds
( len ((((m + 1),(len p)) -cut p) ^ ((1,m) -cut p)) = len p &amp; rng ((((m + 1),(len p)) -cut p) ^ ((1,m) -cut p)) = rng p &amp; ((((m + 1),(len p)) -cut p) ^ ((1,m) -cut p)) . 1 = p . (m + 1) )
proofend;

theorem Th10: :: GRAPH_3:10
for G being Graph
for n being Element of NAT
for p being cyclic Path of G st n in dom p holds
ex p9 being cyclic Path of G st
( p9 . 1 = p . n &amp; len p9 = len p &amp; rng p9 = rng p )
proofend;

theorem Th11: :: GRAPH_3:11
for G being Graph
for e being set
for s, t being Vertex of G st s = the Source of G . e &amp; t = the Target of G . e holds
<*t,s*> is_vertex_seq_of <*e*>
proofend;

theorem Th12: :: GRAPH_3:12
for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G
for e being set st e in the carrier' of G &amp; vs is_vertex_seq_of c &amp; vs . (len vs) = the Source of G . e holds
( c ^ <*e*> is Chain of G &amp; ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> &amp; vs9 is_vertex_seq_of c ^ <*e*> &amp; vs9 . 1 = vs . 1 &amp; vs9 . (len vs9) = the Target of G . e ) )
proofend;

theorem Th13: :: GRAPH_3:13
for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G
for e being set st e in the carrier' of G &amp; vs is_vertex_seq_of c &amp; vs . (len vs) = the Target of G . e holds
( c ^ <*e*> is Chain of G &amp; ex vs9 being FinSequence of the carrier of G st
( vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> &amp; vs9 is_vertex_seq_of c ^ <*e*> &amp; vs9 . 1 = vs . 1 &amp; vs9 . (len vs9) = the Source of G . e ) )
proofend;

Lm3:  for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G st vs is_vertex_seq_of c holds
for n being Nat st 1 <= n &amp; n <= len c holds
( 1 <= n &amp; n <= len vs &amp; 1 <= n + 1 &amp; n + 1 <= len vs &amp; ( ( vs . n = the Target of G . (c . n) &amp; vs . (n + 1) = the Source of G . (c . n) ) or ( vs . n = the Source of G . (c . n) &amp; vs . (n + 1) = the Target of G . (c . n) ) ) )
proofend;

theorem :: GRAPH_3:14
for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G st vs is_vertex_seq_of c holds
for n being Element of NAT holds
( not n in dom c or ( vs . n = the Target of G . (c . n) &amp; vs . (n + 1) = the Source of G . (c . n) ) or ( vs . n = the Source of G . (c . n) &amp; vs . (n + 1) = the Target of G . (c . n) ) )
proofend;

theorem Th15: :: GRAPH_3:15
for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G
for e being set st vs is_vertex_seq_of c &amp; e in rng c holds
( the Target of G . e in rng vs &amp; the Source of G . e in rng vs )
proofend;

definition
let G be Graph;
let X be set ;
:: original:-VSet
redefine funcG -VSet X ->  Subset of the carrier of G;
coherence
 G -VSet X is Subset of the carrier of G
proofend;
end;

theorem Th16: :: GRAPH_3:16
for G being Graph holds G -VSet {} = {}
proofend;

theorem Th17: :: GRAPH_3:17
for G being Graph
for e, X being set st e in the carrier' of G &amp; e in X holds
not G -VSet X is empty
proofend;

theorem Th18: :: GRAPH_3:18
for G being Graph holds
( G is connected iff for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty &amp; vs is_vertex_seq_of c &amp; vs . 1 = v1 &amp; vs . (len vs) = v2 ) )
proofend;

theorem Th19: :: GRAPH_3:19
for G being connected Graph
for X being set
for v being Vertex of G st X meets the carrier' of G &amp; not v in G -VSet X holds
ex v9 being Vertex of G ex e being Element of the carrier' of G st
( v9 in G -VSet X &amp; not e in X &amp; ( v9 = the Target of G . e or v9 = the Source of G . e ) )
proofend;

begin

definition
let G be Graph;
let v be Vertex of G;
let X be set ;
func Edges_In (v,X) ->  Subset of the carrier' of G means :Def1: :: GRAPH_3:def 1
 for e being set holds
( e in it iff ( e in the carrier' of G &amp; e in X &amp; the Target of G . e = v ) );
existence
 ex b1 being Subset of the carrier' of G st
for e being set holds
( e in b1 iff ( e in the carrier' of G &amp; e in X &amp; the Target of G . e = v ) )
proofend;
uniqueness
 for b1, b2 being Subset of the carrier' of G st ( for e being set holds
( e in b1 iff ( e in the carrier' of G &amp; e in X &amp; the Target of G . e = v ) ) ) &amp; ( for e being set holds
( e in b2 iff ( e in the carrier' of G &amp; e in X &amp; the Target of G . e = v ) ) ) holds
b1 = b2
proofend;
func Edges_Out (v,X) ->  Subset of the carrier' of G means :Def2: :: GRAPH_3:def 2
 for e being set holds
( e in it iff ( e in the carrier' of G &amp; e in X &amp; the Source of G . e = v ) );
existence
 ex b1 being Subset of the carrier' of G st
for e being set holds
( e in b1 iff ( e in the carrier' of G &amp; e in X &amp; the Source of G . e = v ) )
proofend;
uniqueness
 for b1, b2 being Subset of the carrier' of G st ( for e being set holds
( e in b1 iff ( e in the carrier' of G &amp; e in X &amp; the Source of G . e = v ) ) ) &amp; ( for e being set holds
( e in b2 iff ( e in the carrier' of G &amp; e in X &amp; the Source of G . e = v ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Edges_In GRAPH_3:def_1_:_
 for G being Graph
for v being Vertex of G
for X being set
for b4 being Subset of the carrier' of G holds
( b4 = Edges_In (v,X) iff for e being set holds
( e in b4 iff ( e in the carrier' of G &amp; e in X &amp; the Target of G . e = v ) ) );

:: deftheorem Def2 defines Edges_Out GRAPH_3:def_2_:_
 for G being Graph
for v being Vertex of G
for X being set
for b4 being Subset of the carrier' of G holds
( b4 = Edges_Out (v,X) iff for e being set holds
( e in b4 iff ( e in the carrier' of G &amp; e in X &amp; the Source of G . e = v ) ) );

definition
let G be Graph;
let v be Vertex of G;
let 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));
correctness
coherence
(Edges_In (v,X)) \/ (Edges_Out (v,X)) is Subset of the carrier' of G;
;
end;

:: deftheorem  defines Edges_At GRAPH_3:def_3_:_
 for G being Graph
for v being Vertex of G
for X being set holds Edges_At (v,X) = (Edges_In (v,X)) \/ (Edges_Out (v,X));

registration
let G be finite Graph;
let v be Vertex of G;
let X be set ;
cluster Edges_In (v,X) ->  finite ;
correctness
coherence
Edges_In (v,X) is finite ;
proofend;
cluster Edges_Out (v,X) ->  finite ;
correctness
coherence
Edges_Out (v,X) is finite ;
proofend;
cluster Edges_At (v,X) ->  finite ;
correctness
coherence
Edges_At (v,X) is finite ;
;
end;

registration
let G be Graph;
let v be Vertex of G;
let X be empty set ;
cluster Edges_In (v,X) ->  empty ;
correctness
coherence
Edges_In (v,X) is empty ;
proofend;
cluster Edges_Out (v,X) ->  empty ;
correctness
coherence
Edges_Out (v,X) is empty ;
proofend;
cluster Edges_At (v,X) ->  empty ;
correctness
coherence
Edges_At (v,X) is empty ;
;
end;

definition
let G be Graph;
let 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);
correctness
coherence
Edges_In (v, the carrier' of G) is Subset of 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);
correctness
coherence
Edges_Out (v, the carrier' of G) is Subset of the carrier' of G;
;
end;

:: deftheorem  defines Edges_In GRAPH_3:def_4_:_
 for G being Graph
for v being Vertex of G holds Edges_In v = Edges_In (v, the carrier' of G);

:: deftheorem  defines Edges_Out GRAPH_3:def_5_:_
 for G being Graph
for v being Vertex of G holds Edges_Out v = Edges_Out (v, the carrier' of G);

theorem Th20: :: GRAPH_3:20
for G being Graph
for v being Vertex of G
for X being set holds Edges_In (v,X) c= Edges_In v
proofend;

theorem Th21: :: GRAPH_3:21
for G being Graph
for v being Vertex of G
for X being set holds Edges_Out (v,X) c= Edges_Out v
proofend;

registration
let G be finite Graph;
let v be Vertex of G;
cluster Edges_In v ->  finite ;
correctness
coherence
Edges_In v is finite ;
;
cluster Edges_Out v ->  finite ;
correctness
coherence
Edges_Out v is finite ;
;
end;

theorem Th22: :: GRAPH_3:22
for G being finite Graph
for v being Vertex of G holds card (Edges_In v) = EdgesIn v
proofend;

theorem Th23: :: GRAPH_3:23
for G being finite Graph
for v being Vertex of G holds card (Edges_Out v) = EdgesOut v
proofend;

definition
let G be finite Graph;
let v be Vertex of G;
let 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)));
correctness
coherence
(card (Edges_In (v,X))) + (card (Edges_Out (v,X))) is Element of NAT ;
;
end;

:: deftheorem  defines Degree GRAPH_3:def_6_:_
 for G being finite Graph
for v being Vertex of G
for X being set holds Degree (v,X) = (card (Edges_In (v,X))) + (card (Edges_Out (v,X)));

theorem Th24: :: GRAPH_3:24
for G being finite Graph
for v being Vertex of G holds Degree v = Degree (v, the carrier' of G)
proofend;

theorem Th25: :: GRAPH_3:25
for X being set
for G being finite Graph
for v being Vertex of G st Degree (v,X) <> 0 holds
not Edges_At (v,X) is empty
proofend;

theorem Th26: :: GRAPH_3:26
for e, X being set
for G being finite Graph
for v being Vertex of G st e in the carrier' of G &amp; not e in X &amp; ( v = the Target of G . e or v = the Source of G . e ) holds
Degree v <> Degree (v,X)
proofend;

theorem Th27: :: GRAPH_3:27
for G being finite Graph
for v being Vertex of G
for X2, X1 being set st X2 c= X1 holds
card (Edges_In (v,(X1 \ X2))) = (card (Edges_In (v,X1))) - (card (Edges_In (v,X2)))
proofend;

theorem Th28: :: GRAPH_3:28
for G being finite Graph
for v being Vertex of G
for X2, X1 being set st X2 c= X1 holds
card (Edges_Out (v,(X1 \ X2))) = (card (Edges_Out (v,X1))) - (card (Edges_Out (v,X2)))
proofend;

theorem Th29: :: GRAPH_3:29
for G being finite Graph
for v being Vertex of G
for X2, X1 being set st X2 c= X1 holds
Degree (v,(X1 \ X2)) = (Degree (v,X1)) - (Degree (v,X2))
proofend;

theorem Th30: :: GRAPH_3:30
for X being set
for G being finite Graph
for v being Vertex of G holds
( Edges_In (v,X) = Edges_In (v,(X /\ the carrier' of G)) &amp; Edges_Out (v,X) = Edges_Out (v,(X /\ the carrier' of G)) )
proofend;

theorem Th31: :: GRAPH_3:31
for X being set
for G being finite Graph
for v being Vertex of G holds Degree (v,X) = Degree (v,(X /\ the carrier' of G))
proofend;

theorem Th32: :: GRAPH_3:32
for G being finite Graph
for v being Vertex of G
for c being Chain of G
for vs being FinSequence of the carrier of G st not c is empty &amp; vs is_vertex_seq_of c holds
( v in rng vs iff Degree (v,(rng c)) <> 0 )
proofend;

theorem Th33: :: GRAPH_3:33
for G being non void connected finite Graph
for v being Vertex of G holds Degree v <> 0
proofend;

begin

definition
let G be Graph;
let v1, v2 be Vertex of G;
func AddNewEdge (v1,v2) ->  strict Graph means :Def7: :: GRAPH_3:def 7
( the carrier of it = the carrier of G &amp; the carrier' of it = the carrier' of G \/ { the carrier' of G} &amp; the Source of it = the Source of G +* ( the carrier' of G .--> v1) &amp; the Target of it = the Target of G +* ( the carrier' of G .--> v2) );
existence
 ex b1 being strict Graph st
( the carrier of b1 = the carrier of G &amp; the carrier' of b1 = the carrier' of G \/ { the carrier' of G} &amp; the Source of b1 = the Source of G +* ( the carrier' of G .--> v1) &amp; the Target of b1 = the Target of G +* ( the carrier' of G .--> v2) )
proofend;
uniqueness
 for b1, b2 being strict Graph st the carrier of b1 = the carrier of G &amp; the carrier' of b1 = the carrier' of G \/ { the carrier' of G} &amp; the Source of b1 = the Source of G +* ( the carrier' of G .--> v1) &amp; the Target of b1 = the Target of G +* ( the carrier' of G .--> v2) &amp; the carrier of b2 = the carrier of G &amp; the carrier' of b2 = the carrier' of G \/ { the carrier' of G} &amp; the Source of b2 = the Source of G +* ( the carrier' of G .--> v1) &amp; the Target of b2 = the Target of G +* ( the carrier' of G .--> v2) holds
b1 = b2 ;
end;

:: deftheorem Def7 defines AddNewEdge GRAPH_3:def_7_:_
 for G being Graph
for v1, v2 being Vertex of G
for b4 being strict Graph holds
( b4 = AddNewEdge (v1,v2) iff ( the carrier of b4 = the carrier of G &amp; the carrier' of b4 = the carrier' of G \/ { the carrier' of G} &amp; the Source of b4 = the Source of G +* ( the carrier' of G .--> v1) &amp; the Target of b4 = the Target of G +* ( the carrier' of G .--> v2) ) );

registration
let G be finite Graph;
let v1, v2 be Vertex of G;
cluster AddNewEdge (v1,v2) ->  strict finite ;
coherence
 AddNewEdge (v1,v2) is finite
proofend;
end;

theorem Th34: :: GRAPH_3:34
for G being Graph
for v1, v2 being Vertex of G holds
( the carrier' of G in the carrier' of (AddNewEdge (v1,v2)) &amp; the carrier' of G = the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} &amp; the Source of (AddNewEdge (v1,v2)) . the carrier' of G = v1 &amp; the Target of (AddNewEdge (v1,v2)) . the carrier' of G = v2 )
proofend;

theorem Th35: :: GRAPH_3:35
for e being set
for G being Graph
for v1, v2 being Vertex of G st e in the carrier' of G holds
( the Source of (AddNewEdge (v1,v2)) . e = the Source of G . e &amp; the Target of (AddNewEdge (v1,v2)) . e = the Target of G . e )
proofend;

theorem Th36: :: GRAPH_3:36
for G being Graph
for v1, v2 being Vertex of G
for c being Chain of G
for vs being FinSequence of the carrier of G
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st vs9 = vs &amp; vs is_vertex_seq_of c holds
vs9 is_vertex_seq_of c
proofend;

theorem Th37: :: GRAPH_3:37
for G being Graph
for v1, v2 being Vertex of G
for c being Chain of G holds c is Chain of AddNewEdge (v1,v2)
proofend;

theorem :: GRAPH_3:38
for G being Graph
for v1, v2 being Vertex of G
for p being Path of G holds p is Path of AddNewEdge (v1,v2) by Th37;

theorem Th39: :: GRAPH_3:39
for X being set
for G being Graph
for v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v1 &amp; v1 <> v2 holds
Edges_In (v9,X) = Edges_In (v1,X)
proofend;

theorem Th40: :: GRAPH_3:40
for X being set
for G being Graph
for v2, v1 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v2 &amp; v1 <> v2 holds
Edges_Out (v9,X) = Edges_Out (v2,X)
proofend;

theorem Th41: :: GRAPH_3:41
for X being set
for G being Graph
for v2, v1 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v1 &amp; the carrier' of G in X holds
( Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G} &amp; Edges_Out (v1,X) misses { the carrier' of G} )
proofend;

theorem Th42: :: GRAPH_3:42
for X being set
for G being Graph
for v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v2 &amp; the carrier' of G in X holds
( Edges_In (v9,X) = (Edges_In (v2,X)) \/ { the carrier' of G} &amp; Edges_In (v2,X) misses { the carrier' of G} )
proofend;

theorem Th43: :: GRAPH_3:43
for X being set
for G being Graph
for v1, v, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v &amp; v <> v2 holds
Edges_In (v9,X) = Edges_In (v,X)
proofend;

theorem Th44: :: GRAPH_3:44
for X being set
for G being Graph
for v2, v, v1 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v &amp; v <> v1 holds
Edges_Out (v9,X) = Edges_Out (v,X)
proofend;

theorem Th45: :: GRAPH_3:45
for G being Graph
for v1, v2 being Vertex of G
for p9 being Path of AddNewEdge (v1,v2) st not the carrier' of G in rng p9 holds
p9 is Path of G
proofend;

theorem Th46: :: GRAPH_3:46
for G being Graph
for v1, v2 being Vertex of G
for vs being FinSequence of the carrier of G
for p9 being Path of AddNewEdge (v1,v2)
for vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) st not the carrier' of G in rng p9 &amp; vs = vs9 &amp; vs9 is_vertex_seq_of p9 holds
vs is_vertex_seq_of p9
proofend;

registration
let G be connected Graph;
let v1, v2 be Vertex of G;
cluster AddNewEdge (v1,v2) ->  strict connected ;
coherence
 AddNewEdge (v1,v2) is connected
proofend;
end;

theorem Th47: :: GRAPH_3:47
for X being set
for G being finite Graph
for v, v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v &amp; v1 <> v2 &amp; ( v = v1 or v = v2 ) &amp; the carrier' of G in X holds
Degree (v9,X) = (Degree (v,X)) + 1
proofend;

theorem Th48: :: GRAPH_3:48
for X being set
for G being finite Graph
for v, v1, v2 being Vertex of G
for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v &amp; v <> v1 &amp; v <> v2 holds
Degree (v9,X) = Degree (v,X)
proofend;

begin

Lm4:  for G being finite Graph
for c being cyclic Path of G
for vs being FinSequence of the carrier of G
for v being Vertex of G st vs is_vertex_seq_of c &amp; v in rng vs holds
Degree (v,(rng c)) is even
proofend;

theorem Th49: :: GRAPH_3:49
for G being finite Graph
for v being Vertex of G
for c being cyclic Path of G holds Degree (v,(rng c)) is even
proofend;

theorem Th50: :: GRAPH_3:50
for G being finite Graph
for v being Vertex of G
for vs being FinSequence of the carrier of G
for c being Path of G st not c is cyclic &amp; vs is_vertex_seq_of c holds
( Degree (v,(rng c)) is even iff ( v <> vs . 1 &amp; v <> vs . (len vs) ) )
proofend;

definition
let G be Graph;
funcG -CycleSet  ->  FinSequenceSet of the carrier' of G means :Def8: :: GRAPH_3:def 8
 for x being set holds
( x in it iff x is cyclic Path of G );
existence
 ex b1 being FinSequenceSet of the carrier' of G st
for x being set holds
( x in b1 iff x is cyclic Path of G )
proofend;
uniqueness
 for b1, b2 being FinSequenceSet of the carrier' of G st ( for x being set holds
( x in b1 iff x is cyclic Path of G ) ) &amp; ( for x being set holds
( x in b2 iff x is cyclic Path of G ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines -CycleSet GRAPH_3:def_8_:_
 for G being Graph
for b2 being FinSequenceSet of the carrier' of G holds
( b2 = G -CycleSet iff for x being set holds
( x in b2 iff x is cyclic Path of G ) );

theorem Th51: :: GRAPH_3:51
for G being Graph holds {} in G -CycleSet
proofend;

registration
let G be Graph;
clusterG -CycleSet  ->  non empty ;
coherence
 not G -CycleSet is empty by Th51;
end;

theorem Th52: :: GRAPH_3:52
for G being Graph
for v being Vertex of G
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 &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 &amp; vs . 1 = v ) )  }  is non empty Subset of (G -CycleSet)
proofend;

definition
let G be Graph;
let v be Vertex of G;
let c be Element of G -CycleSet ;
assume A1: v in G -VSet (rng c) ;
func Rotate (c,v) ->  Element of G -CycleSet  equals :Def9: :: GRAPH_3:def 9
 choose  {  c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 &amp; vs . 1 = v ) )  }  ;
coherence
 choose  {  c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 &amp; vs . 1 = v ) )  }  is Element of G -CycleSet
proofend;
end;

:: deftheorem Def9 defines Rotate GRAPH_3:def_9_:_
 for G being Graph
for v being Vertex of G
for c being Element of G -CycleSet st v in G -VSet (rng c) holds
Rotate (c,v) = choose  {  c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 &amp; vs . 1 = v ) )  }  ;

Lm5:  for G being Graph
for c being Element of G -CycleSet
for v being Vertex of G st v in G -VSet (rng c) holds
rng (Rotate (c,v)) = rng c
proofend;

definition
let G be Graph;
let c1, c2 be Element of G -CycleSet ;
assume that
A1: G -VSet (rng c1) meets G -VSet (rng c2) and
A2: rng c1 misses rng c2 ;
func CatCycles (c1,c2) ->  Element of G -CycleSet  means :Def10: :: GRAPH_3:def 10
 ex v being Vertex of G st
( v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) &amp; it = (Rotate (c1,v)) ^ (Rotate (c2,v)) );
existence
 ex b1 being Element of G -CycleSet ex v being Vertex of G st
( v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) &amp; b1 = (Rotate (c1,v)) ^ (Rotate (c2,v)) )
proofend;
correctness
uniqueness
for b1, b2 being Element of G -CycleSet st ex v being Vertex of G st
( v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) &amp; b1 = (Rotate (c1,v)) ^ (Rotate (c2,v)) ) &amp; ex v being Vertex of G st
( v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) &amp; b2 = (Rotate (c1,v)) ^ (Rotate (c2,v)) ) holds
b1 = b2;
;
end;

:: deftheorem Def10 defines CatCycles GRAPH_3:def_10_:_
 for G being Graph
for c1, c2 being Element of G -CycleSet st G -VSet (rng c1) meets G -VSet (rng c2) &amp; rng c1 misses rng c2 holds
for b4 being Element of G -CycleSet holds
( b4 = CatCycles (c1,c2) iff ex v being Vertex of G st
( v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) &amp; b4 = (Rotate (c1,v)) ^ (Rotate (c2,v)) ) );

theorem Th53: :: GRAPH_3:53
for G being Graph
for c1, c2 being Element of G -CycleSet st G -VSet (rng c1) meets G -VSet (rng c2) &amp; rng c1 misses rng c2 &amp; ( c1 <> {} or c2 <> {} ) holds
not CatCycles (c1,c2) is empty
proofend;

definition
let G be finite Graph;
let v be Vertex of G;
let X be set ;
assume A1: Degree (v,X) <> 0 ;
funcX -PathSet v ->  non empty FinSequenceSet of the carrier' of G equals :Def11: :: GRAPH_3:def 11
 {  c where c is Element of X * : ( c is Path of G &amp; not c is empty &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c &amp; vs . 1 = v ) )  }  ;
coherence
  {  c where c is Element of X * : ( c is Path of G &amp; not c is empty &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c &amp; vs . 1 = v ) )  }  is non empty FinSequenceSet of the carrier' of G
proofend;
end;

:: deftheorem Def11 defines -PathSet GRAPH_3:def_11_:_
 for G being finite Graph
for v being Vertex of G
for X being set st Degree (v,X) <> 0 holds
X -PathSet v =  {  c where c is Element of X * : ( c is Path of G &amp; not c is empty &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c &amp; vs . 1 = v ) )  }  ;

theorem Th54: :: GRAPH_3:54
for X being set
for G being finite Graph
for v being Vertex of G
for p being Element of X -PathSet v
for Y being finite set st Y = the carrier' of G &amp; Degree (v,X) <> 0 holds
len p <= card Y
proofend;

definition
let G be finite Graph;
let v be Vertex of G;
let X be set ;
assume that
A1: for v being Vertex of G holds Degree (v,X) is even and
A2: Degree (v,X) <> 0 ;
funcX -CycleSet v ->  non empty Subset of (G -CycleSet) equals :Def12: :: GRAPH_3:def 12
 {  c where c is Element of G -CycleSet : ( rng c c= X &amp; not c is empty &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c &amp; vs . 1 = v ) )  }  ;
coherence
  {  c where c is Element of G -CycleSet : ( rng c c= X &amp; not c is empty &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c &amp; vs . 1 = v ) )  }  is non empty Subset of (G -CycleSet)
proofend;
end;

:: deftheorem Def12 defines -CycleSet GRAPH_3:def_12_:_
 for G being finite Graph
for v being Vertex of G
for X being set st ( for v being Vertex of G holds Degree (v,X) is even ) &amp; Degree (v,X) <> 0 holds
X -CycleSet v =  {  c where c is Element of G -CycleSet : ( rng c c= X &amp; not c is empty &amp; ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c &amp; vs . 1 = v ) )  }  ;

theorem Th55: :: GRAPH_3:55
for X being set
for G being finite Graph
for v being Vertex of G st Degree (v,X) <> 0 &amp; ( for v being Vertex of G holds Degree (v,X) is even ) holds
for c being Element of X -CycleSet v holds
( not c is empty &amp; rng c c= X &amp; v in G -VSet (rng c) )
proofend;

theorem Th56: :: GRAPH_3:56
for G being connected finite Graph
for c being Element of G -CycleSet st rng c <> the carrier' of G &amp; not c is empty holds
{  v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) &amp; Degree v9 <> Degree (v9,(rng c)) )  }  is non empty Subset of the carrier of G
proofend;

definition
let G be connected finite Graph;
let c be Element of G -CycleSet ;
assume that
A1: rng c <> the carrier' of G and
A2: not c is empty ;
func ExtendCycle c ->  Element of G -CycleSet  means :Def13: :: GRAPH_3:def 13
 ex c9 being Element of G -CycleSet ex v being Vertex of G st
( v = choose  {  v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) &amp; Degree v9 <> Degree (v9,(rng c)) )  }  &amp; c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) &amp; it = CatCycles (c,c9) );
existence
 ex b1, c9 being Element of G -CycleSet ex v being Vertex of G st
( v = choose  {  v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) &amp; Degree v9 <> Degree (v9,(rng c)) )  }  &amp; c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) &amp; b1 = CatCycles (c,c9) )
proofend;
uniqueness
 for b1, b2 being Element of G -CycleSet st ex c9 being Element of G -CycleSet ex v being Vertex of G st
( v = choose  {  v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) &amp; Degree v9 <> Degree (v9,(rng c)) )  }  &amp; c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) &amp; b1 = CatCycles (c,c9) ) &amp; ex c9 being Element of G -CycleSet ex v being Vertex of G st
( v = choose  {  v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) &amp; Degree v9 <> Degree (v9,(rng c)) )  }  &amp; c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) &amp; b2 = CatCycles (c,c9) ) holds
b1 = b2 ;
end;

:: deftheorem Def13 defines ExtendCycle GRAPH_3:def_13_:_
 for G being connected finite Graph
for c being Element of G -CycleSet st rng c <> the carrier' of G &amp; not c is empty holds
for b3 being Element of G -CycleSet holds
( b3 = ExtendCycle c iff ex c9 being Element of G -CycleSet ex v being Vertex of G st
( v = choose  {  v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) &amp; Degree v9 <> Degree (v9,(rng c)) )  }  &amp; c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) &amp; b3 = CatCycles (c,c9) ) );

theorem Th57: :: GRAPH_3:57
for G being connected finite Graph
for c being Element of G -CycleSet st rng c <> the carrier' of G &amp; not c is empty &amp; ( for v being Vertex of G holds Degree v is even ) holds
( not ExtendCycle c is empty &amp; card (rng c) < card (rng (ExtendCycle c)) )
proofend;

begin

definition
let G be Graph;
let p be Path of G;
attrp is Eulerian  means :Def14: :: GRAPH_3:def 14
 rng p = the carrier' of G;
end;

:: deftheorem Def14 defines Eulerian GRAPH_3:def_14_:_
 for G being Graph
for p being Path of G holds
( p is Eulerian iff rng p = the carrier' of G );

theorem Th58: :: GRAPH_3:58
for G being connected Graph
for p being Path of G
for vs being FinSequence of the carrier of G st p is Eulerian &amp; vs is_vertex_seq_of p holds
rng vs = the carrier of G
proofend;

theorem Th59: :: GRAPH_3:59
for G being connected finite 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 )
proofend;

theorem :: GRAPH_3:60
for G being connected finite Graph holds
( ex p being Path of G st
( not p is cyclic &amp; p is Eulerian ) iff ex v1, v2 being Vertex of G st
( v1 <> v2 &amp; ( for v being Vertex of G holds
( Degree v is even iff ( v <> v1 &amp; v <> v2 ) ) ) ) )
proofend;