:: by Yatsuka Nakamura and Piotr Rudnicki

::

:: Received July 29, 1997

:: Copyright (c) 1997-2021 Association of Mizar Users

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 b_{1} being Element of S holds b_{1} is FinSequence of D

end;
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 b

proof end;

registration
end;

theorem :: GRAPH_3:1

Lm1: for p being FinSequence

for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds

( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds

((m,n) -cut p) . (i + 1) = p . (m + i) ) )

proof end;

theorem Th2: :: GRAPH_3:2

for p being FinSequence

for m, n, a being Nat st a in dom ((m,n) -cut p) holds

ex k being Nat st

( k in dom p & p . k = ((m,n) -cut p) . a & k + 1 = m + a & m <= k & k <= n )

for m, n, a being Nat st a in dom ((m,n) -cut p) holds

ex k being Nat st

( k in dom p & p . k = ((m,n) -cut p) . a & k + 1 = m + a & m <= k & k <= n )

proof end;

theorem :: 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 ;

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 ;

Lm2: for G being Graph

for p being Path of G

for n, m being Nat st 1 <= n & n <= len p & 1 <= m & m <= len p & n <> m holds

p . n <> p . m

proof end;

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 & vs1 is_vertex_seq_of p1 & vs2 is_vertex_seq_of p2 & vs1 . (len vs1) = vs2 . 1 holds

p1 ^ p2 is Path of G

for p1, p2 being Path of G

for vs1, vs2 being FinSequence of the carrier of G st rng p1 misses rng p2 & vs1 is_vertex_seq_of p1 & vs2 is_vertex_seq_of p2 & vs1 . (len vs1) = vs2 . 1 holds

p1 ^ p2 is Path of G

proof end;

registration

let G be Graph;

ex b_{1} being Path of G st b_{1} is cyclic

end;
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 b

proof end;

theorem Th8: :: GRAPH_3:8

for G being Graph

for m being Nat

for p being cyclic Path of G holds (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G

for m being Nat

for p being cyclic Path of G holds (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G

proof end;

theorem Th9: :: GRAPH_3:9

for G being Graph

for p being Path of G

for m being Nat st m + 1 in dom p holds

( 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) )

for p being Path of G

for m being Nat st m + 1 in dom p holds

( 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) )

proof end;

theorem Th10: :: GRAPH_3:10

for G being Graph

for n being 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 & len p9 = len p & rng p9 = rng p )

for n being 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 & len p9 = len p & rng p9 = rng p )

proof end;

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 & t = the Target of G . e holds

<*t,s*> is_vertex_seq_of <*e*>

for e being set

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*>

proof end;

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 & vs is_vertex_seq_of c & vs . (len vs) = the Source of G . e holds

( 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 ) )

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 & vs is_vertex_seq_of c & vs . (len vs) = the Source of G . e holds

( 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 ) )

proof end;

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 & vs is_vertex_seq_of c & vs . (len vs) = the Target of G . e holds

( 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 ) )

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 & vs is_vertex_seq_of c & vs . (len vs) = the Target of G . e holds

( 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 ) )

proof end;

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 & n <= len c holds

( 1 <= n & n <= len vs & 1 <= n + 1 & n + 1 <= len vs & ( ( 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) ) ) )

proof end;

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) & 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) ) )

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) & 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) ) )

proof end;

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 & e in rng c holds

( the Target of G . e in rng vs & the Source of G . e in rng vs )

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 & e in rng c holds

( the Target of G . e in rng vs & the Source of G . e in rng vs )

proof end;

definition

let G be Graph;

let X be set ;

:: original: -VSet

redefine func G -VSet X -> Subset of the carrier of G;

coherence

G -VSet X is Subset of the carrier of G

end;
let X be set ;

:: original: -VSet

redefine func G -VSet X -> Subset of the carrier of G;

coherence

G -VSet X is Subset of the carrier of G

proof end;

theorem Th17: :: GRAPH_3:17

for G being Graph

for e, X being set st e in the carrier' of G & e in X holds

not G -VSet X is empty

for e, X being set st e in the carrier' of G & e in X holds

not G -VSet X is empty

proof end;

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 & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )

( 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 & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )

proof end;

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 & 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 & not e in X & ( v9 = the Target of G . e or v9 = the Source of G . e ) )

for X being set

for v being Vertex of G st X meets the carrier' of G & 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 & not e in X & ( v9 = the Target of G . e or v9 = the Source of G . e ) )

proof end;

definition

let G be Graph;

let v be Vertex of G;

let X be set ;

ex b_{1} being Subset of the carrier' of G st

for e being set holds

( e in b_{1} iff ( e in the carrier' of G & e in X & the Target of G . e = v ) )

for b_{1}, b_{2} being Subset of the carrier' of G st ( for e being set holds

( e in b_{1} iff ( e in the carrier' of G & e in X & the Target of G . e = v ) ) ) & ( for e being set holds

( e in b_{2} iff ( e in the carrier' of G & e in X & the Target of G . e = v ) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of the carrier' of G st

for e being set holds

( e in b_{1} iff ( e in the carrier' of G & e in X & the Source of G . e = v ) )

for b_{1}, b_{2} being Subset of the carrier' of G st ( for e being set holds

( e in b_{1} iff ( e in the carrier' of G & e in X & the Source of G . e = v ) ) ) & ( for e being set holds

( e in b_{2} iff ( e in the carrier' of G & e in X & the Source of G . e = v ) ) ) holds

b_{1} = b_{2}

end;
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 & e in X & the Target of G . e = v ) );

existence for e being set holds

( e in it iff ( e in the carrier' of G & e in X & the Target of G . e = v ) );

ex b

for e being set holds

( e in b

proof end;

uniqueness for b

( e in b

( e in b

b

proof end;

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 & e in X & the Source of G . e = v ) );

existence for e being set holds

( e in it iff ( e in the carrier' of G & e in X & the Source of G . e = v ) );

ex b

for e being set holds

( e in b

proof end;

uniqueness for b

( e in b

( e in b

b

proof 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 b_{4} being Subset of the carrier' of G holds

( b_{4} = Edges_In (v,X) iff for e being set holds

( e in b_{4} iff ( e in the carrier' of G & e in X & the Target of G . e = v ) ) );

for G being Graph

for v being Vertex of G

for X being set

for b

( b

( e in b

:: deftheorem Def2 defines Edges_Out GRAPH_3:def 2 :

for G being Graph

for v being Vertex of G

for X being set

for b_{4} being Subset of the carrier' of G holds

( b_{4} = Edges_Out (v,X) iff for e being set holds

( e in b_{4} iff ( e in the carrier' of G & e in X & the Source of G . e = v ) ) );

for G being Graph

for v being Vertex of G

for X being set

for b

( b

( e in b

definition

let G be Graph;

let v be Vertex of G;

let X be set ;

coherence

(Edges_In (v,X)) \/ (Edges_Out (v,X)) is Subset of the carrier' of G;

;

end;
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 (Edges_In (v,X)) \/ (Edges_Out (v,X));

coherence

(Edges_In (v,X)) \/ (Edges_Out (v,X)) is Subset of the carrier' of G;

;

:: 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));

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 ;

correctness

coherence

Edges_In (v,X) is finite ;

coherence

Edges_Out (v,X) is finite ;

coherence

Edges_At (v,X) is finite ;

;

end;
let v be Vertex of G;

let X be set ;

correctness

coherence

Edges_In (v,X) is finite ;

proof end;

correctness coherence

Edges_Out (v,X) is finite ;

proof end;

correctness coherence

Edges_At (v,X) is finite ;

;

registration

let G be Graph;

let v be Vertex of G;

let X be empty set ;

correctness

coherence

Edges_In (v,X) is empty ;

by Def1;

correctness

coherence

Edges_Out (v,X) is empty ;

by Def2;

correctness

coherence

Edges_At (v,X) is empty ;

;

end;
let v be Vertex of G;

let X be empty set ;

correctness

coherence

Edges_In (v,X) is empty ;

by Def1;

correctness

coherence

Edges_Out (v,X) is empty ;

by Def2;

correctness

coherence

Edges_At (v,X) is empty ;

;

definition

let G be Graph;

let v be Vertex of G;

coherence

Edges_In (v, the carrier' of G) is Subset of the carrier' of G;

;

coherence

Edges_Out (v, the carrier' of G) is Subset of the carrier' of G;

;

end;
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 Edges_In (v, the carrier' of G);

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 Edges_Out (v, the carrier' of G);

coherence

Edges_Out (v, the carrier' of G) is Subset of the carrier' of G;

;

:: 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);

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);

for G being Graph

for v being Vertex of G holds Edges_Out v = Edges_Out (v, the carrier' of G);

registration

let G be finite Graph;

let v be Vertex of G;

correctness

coherence

Edges_In v is finite ;

;

correctness

coherence

Edges_Out v is finite ;

;

end;
let v be Vertex of G;

correctness

coherence

Edges_In v is finite ;

;

correctness

coherence

Edges_Out v is finite ;

;

definition

let G be finite Graph;

let v be Vertex of G;

let X be set ;

coherence

(card (Edges_In (v,X))) + (card (Edges_Out (v,X))) is Element of NAT ;

;

end;
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 (card (Edges_In (v,X))) + (card (Edges_Out (v,X)));

coherence

(card (Edges_In (v,X))) + (card (Edges_Out (v,X))) is Element of NAT ;

;

:: 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)));

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 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

for G being finite Graph

for v being Vertex of G st Degree (v,X) <> 0 holds

not Edges_At (v,X) is empty

proof end;

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 & not e in X & ( v = the Target of G . e or v = the Source of G . e ) holds

Degree v <> Degree (v,X)

for G being finite Graph

for v being Vertex of G st e in the carrier' of G & not e in X & ( v = the Target of G . e or v = the Source of G . e ) holds

Degree v <> Degree (v,X)

proof end;

theorem Th27: :: GRAPH_3:27

for G being finite Graph

for v being Vertex of G

for X1, X2 being set st X2 c= X1 holds

card (Edges_In (v,(X1 \ X2))) = (card (Edges_In (v,X1))) - (card (Edges_In (v,X2)))

for v being Vertex of G

for X1, X2 being set st X2 c= X1 holds

card (Edges_In (v,(X1 \ X2))) = (card (Edges_In (v,X1))) - (card (Edges_In (v,X2)))

proof end;

theorem Th28: :: GRAPH_3:28

for G being finite Graph

for v being Vertex of G

for X1, X2 being set st X2 c= X1 holds

card (Edges_Out (v,(X1 \ X2))) = (card (Edges_Out (v,X1))) - (card (Edges_Out (v,X2)))

for v being Vertex of G

for X1, X2 being set st X2 c= X1 holds

card (Edges_Out (v,(X1 \ X2))) = (card (Edges_Out (v,X1))) - (card (Edges_Out (v,X2)))

proof end;

theorem Th29: :: GRAPH_3:29

for G being finite Graph

for v being Vertex of G

for X1, X2 being set st X2 c= X1 holds

Degree (v,(X1 \ X2)) = (Degree (v,X1)) - (Degree (v,X2))

for v being Vertex of G

for X1, X2 being set st X2 c= X1 holds

Degree (v,(X1 \ X2)) = (Degree (v,X1)) - (Degree (v,X2))

proof end;

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)) & Edges_Out (v,X) = Edges_Out (v,(X /\ the carrier' of G)) )

for G being finite Graph

for v being Vertex of G holds

( Edges_In (v,X) = Edges_In (v,(X /\ the carrier' of G)) & Edges_Out (v,X) = Edges_Out (v,(X /\ the carrier' of G)) )

proof end;

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))

for G being finite Graph

for v being Vertex of G holds Degree (v,X) = Degree (v,(X /\ the carrier' of G))

proof end;

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 & vs is_vertex_seq_of c holds

( v in rng vs iff Degree (v,(rng c)) <> 0 )

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 & vs is_vertex_seq_of c holds

( v in rng vs iff Degree (v,(rng c)) <> 0 )

proof end;

definition

let G be Graph;

let v1, v2 be Vertex of G;

ex b_{1} being strict Graph st

( the carrier of b_{1} = the carrier of G & the carrier' of b_{1} = the carrier' of G \/ { the carrier' of G} & the Source of b_{1} = the Source of G +* ( the carrier' of G .--> v1) & the Target of b_{1} = the Target of G +* ( the carrier' of G .--> v2) )

for b_{1}, b_{2} being strict Graph st the carrier of b_{1} = the carrier of G & the carrier' of b_{1} = the carrier' of G \/ { the carrier' of G} & the Source of b_{1} = the Source of G +* ( the carrier' of G .--> v1) & the Target of b_{1} = the Target of G +* ( the carrier' of G .--> v2) & the carrier of b_{2} = the carrier of G & the carrier' of b_{2} = the carrier' of G \/ { the carrier' of G} & the Source of b_{2} = the Source of G +* ( the carrier' of G .--> v1) & the Target of b_{2} = the Target of G +* ( the carrier' of G .--> v2) holds

b_{1} = b_{2}
;

end;
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 & 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) );

existence ( 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) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def7 defines AddNewEdge GRAPH_3:def 7 :

for G being Graph

for v1, v2 being Vertex of G

for b_{4} being strict Graph holds

( b_{4} = AddNewEdge (v1,v2) iff ( the carrier of b_{4} = the carrier of G & the carrier' of b_{4} = the carrier' of G \/ { the carrier' of G} & the Source of b_{4} = the Source of G +* ( the carrier' of G .--> v1) & the Target of b_{4} = the Target of G +* ( the carrier' of G .--> v2) ) );

for G being Graph

for v1, v2 being Vertex of G

for b

( b

registration
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)) & 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 )

for v1, v2 being Vertex of G holds

( 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 )

proof end;

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 & the Target of (AddNewEdge (v1,v2)) . e = the Target of G . e )

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 & the Target of (AddNewEdge (v1,v2)) . e = the Target of G . e )

proof end;

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 & vs is_vertex_seq_of c holds

vs9 is_vertex_seq_of c

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 & vs is_vertex_seq_of c holds

vs9 is_vertex_seq_of c

proof end;

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)

for v1, v2 being Vertex of G

for c being Chain of G holds c is Chain of AddNewEdge (v1,v2)

proof end;

theorem :: GRAPH_3:38

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 & v1 <> v2 holds

Edges_In (v9,X) = Edges_In (v1,X)

for G being Graph

for v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v1 & v1 <> v2 holds

Edges_In (v9,X) = Edges_In (v1,X)

proof end;

theorem Th40: :: GRAPH_3:40

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 & v1 <> v2 holds

Edges_Out (v9,X) = Edges_Out (v2,X)

for G being Graph

for v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v2 & v1 <> v2 holds

Edges_Out (v9,X) = Edges_Out (v2,X)

proof end;

theorem Th41: :: GRAPH_3:41

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 & the carrier' of G in X holds

( Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G} & Edges_Out (v1,X) misses { the carrier' of G} )

for G being Graph

for v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v1 & the carrier' of G in X holds

( Edges_Out (v9,X) = (Edges_Out (v1,X)) \/ { the carrier' of G} & Edges_Out (v1,X) misses { the carrier' of G} )

proof end;

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 & the carrier' of G in X holds

( Edges_In (v9,X) = (Edges_In (v2,X)) \/ { the carrier' of G} & Edges_In (v2,X) misses { the carrier' of G} )

for G being Graph

for v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v2 & the carrier' of G in X holds

( Edges_In (v9,X) = (Edges_In (v2,X)) \/ { the carrier' of G} & Edges_In (v2,X) misses { the carrier' of G} )

proof end;

theorem Th43: :: GRAPH_3:43

for X being set

for G being Graph

for v, v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v <> v2 holds

Edges_In (v9,X) = Edges_In (v,X)

for G being Graph

for v, v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v <> v2 holds

Edges_In (v9,X) = Edges_In (v,X)

proof end;

theorem Th44: :: GRAPH_3:44

for X being set

for G being Graph

for v, v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v <> v1 holds

Edges_Out (v9,X) = Edges_Out (v,X)

for G being Graph

for v, v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v <> v1 holds

Edges_Out (v9,X) = Edges_Out (v,X)

proof end;

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

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

proof end;

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 & vs = vs9 & vs9 is_vertex_seq_of p9 holds

vs is_vertex_seq_of p9

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 & vs = vs9 & vs9 is_vertex_seq_of p9 holds

vs is_vertex_seq_of p9

proof end;

registration

let G be connected Graph;

let v1, v2 be Vertex of G;

coherence

AddNewEdge (v1,v2) is connected

end;
let v1, v2 be Vertex of G;

coherence

AddNewEdge (v1,v2) is connected

proof 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 & v1 <> v2 & ( v = v1 or v = v2 ) & the carrier' of G in X holds

Degree (v9,X) = (Degree (v,X)) + 1

for G being finite Graph

for v, v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v1 <> v2 & ( v = v1 or v = v2 ) & the carrier' of G in X holds

Degree (v9,X) = (Degree (v,X)) + 1

proof end;

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 & v <> v1 & v <> v2 holds

Degree (v9,X) = Degree (v,X)

for G being finite Graph

for v, v1, v2 being Vertex of G

for v9 being Vertex of (AddNewEdge (v1,v2)) st v9 = v & v <> v1 & v <> v2 holds

Degree (v9,X) = Degree (v,X)

proof end;

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 & v in rng vs holds

Degree (v,(rng c)) is even

proof end;

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

for v being Vertex of G

for c being cyclic Path of G holds Degree (v,(rng c)) is even

proof end;

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 & vs is_vertex_seq_of c holds

( Degree (v,(rng c)) is even iff ( v <> vs . 1 & v <> vs . (len vs) ) )

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 & vs is_vertex_seq_of c holds

( Degree (v,(rng c)) is even iff ( v <> vs . 1 & v <> vs . (len vs) ) )

proof end;

definition

let G be Graph;

ex b_{1} being FinSequenceSet of the carrier' of G st

for x being set holds

( x in b_{1} iff x is cyclic Path of G )

for b_{1}, b_{2} being FinSequenceSet of the carrier' of G st ( for x being set holds

( x in b_{1} iff x is cyclic Path of G ) ) & ( for x being set holds

( x in b_{2} iff x is cyclic Path of G ) ) holds

b_{1} = b_{2}

end;
func G -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 for x being set holds

( x in it iff x is cyclic Path of G );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def8 defines -CycleSet GRAPH_3:def 8 :

for G being Graph

for b_{2} being FinSequenceSet of the carrier' of G holds

( b_{2} = G -CycleSet iff for x being set holds

( x in b_{2} iff x is cyclic Path of G ) );

for G being Graph

for b

( b

( x in b

registration
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 & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet)

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 & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet)

proof end;

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) ;

the Element of { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is Element of G -CycleSet

end;
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

the Element of { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } ;

coherence the Element of { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } ;

the Element of { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } is Element of G -CycleSet

proof 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) = the Element of { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } ;

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) = the Element of { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c9 & 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

proof end;

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 ;

ex b_{1} being Element of G -CycleSet ex v being Vertex of G st

( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & b_{1} = (Rotate (c1,v)) ^ (Rotate (c2,v)) )

uniqueness

for b_{1}, b_{2} being Element of G -CycleSet st ex v being Vertex of G st

( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & b_{1} = (Rotate (c1,v)) ^ (Rotate (c2,v)) ) & ex v being Vertex of G st

( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & b_{2} = (Rotate (c1,v)) ^ (Rotate (c2,v)) ) holds

b_{1} = b_{2};

;

end;
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 = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & it = (Rotate (c1,v)) ^ (Rotate (c2,v)) );

existence 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)) );

ex b

( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & b

proof end;

correctness uniqueness

for b

( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & b

( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & b

b

;

:: 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) & rng c1 misses rng c2 holds

for b_{4} being Element of G -CycleSet holds

( b_{4} = CatCycles (c1,c2) iff ex v being Vertex of G st

( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & b_{4} = (Rotate (c1,v)) ^ (Rotate (c2,v)) ) );

for G being Graph

for c1, c2 being Element of G -CycleSet st G -VSet (rng c1) meets G -VSet (rng c2) & rng c1 misses rng c2 holds

for b

( b

( v = the Element of (G -VSet (rng c1)) /\ (G -VSet (rng c2)) & b

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) & rng c1 misses rng c2 & ( c1 <> {} or c2 <> {} ) holds

not CatCycles (c1,c2) is empty

for c1, c2 being Element of G -CycleSet st G -VSet (rng c1) meets G -VSet (rng c2) & rng c1 misses rng c2 & ( c1 <> {} or c2 <> {} ) holds

not CatCycles (c1,c2) is empty

proof end;

definition

let G be finite Graph;

let v be Vertex of G;

let X be set ;

assume A1: Degree (v,X) <> 0 ;

{ c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } is non empty FinSequenceSet of the carrier' of G

end;
let v be Vertex of G;

let X be set ;

assume A1: Degree (v,X) <> 0 ;

func X -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 & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;

coherence { c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;

{ c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } is non empty FinSequenceSet of the carrier' of G

proof 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 & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;

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 & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & 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 & Degree (v,X) <> 0 holds

len p <= card Y

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 & Degree (v,X) <> 0 holds

len p <= card Y

proof end;

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 ;

{ c where c is Element of G -CycleSet : ( rng c c= X & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet)

end;
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 ;

func X -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 & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;

coherence { c where c is Element of G -CycleSet : ( rng c c= X & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;

{ c where c is Element of G -CycleSet : ( rng c c= X & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet)

proof 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 ) & Degree (v,X) <> 0 holds

X -CycleSet v = { c where c is Element of G -CycleSet : ( rng c c= X & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;

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 ) & Degree (v,X) <> 0 holds

X -CycleSet v = { c where c is Element of G -CycleSet : ( rng c c= X & not c is empty & ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of c & 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 & ( 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 & rng c c= X & v in G -VSet (rng c) )

for G being finite Graph

for v being Vertex of G st Degree (v,X) <> 0 & ( 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 & rng c c= X & v in G -VSet (rng c) )

proof end;

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 & not c is 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

for c being Element of G -CycleSet st rng c <> the carrier' of G & not c is 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

proof end;

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 ;

ex b_{1}, c9 being Element of G -CycleSet ex 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 & b_{1} = CatCycles (c,c9) )

for b_{1}, b_{2} being Element of G -CycleSet st ex c9 being Element of G -CycleSet ex 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 & b_{1} = CatCycles (c,c9) ) & ex c9 being Element of G -CycleSet ex 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 & b_{2} = CatCycles (c,c9) ) holds

b_{1} = b_{2}
;

end;
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 = 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) );

existence ex c9 being Element of G -CycleSet ex 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) );

ex b

( 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 & b

proof end;

uniqueness for b

( 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 & b

( 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 & b

b

:: 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 & not c is empty holds

for b_{3} being Element of G -CycleSet holds

( b_{3} = ExtendCycle c iff ex c9 being Element of G -CycleSet ex 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 & b_{3} = CatCycles (c,c9) ) );

for G being connected finite Graph

for c being Element of G -CycleSet st rng c <> the carrier' of G & not c is empty holds

for b

( b

( 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 & b

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 & not c is empty & ( for v being Vertex of G holds Degree v is even ) holds

( not ExtendCycle c is empty & card (rng c) < card (rng (ExtendCycle c)) )

for c being Element of G -CycleSet st rng c <> the carrier' of G & not c is empty & ( for v being Vertex of G holds Degree v is even ) holds

( not ExtendCycle c is empty & card (rng c) < card (rng (ExtendCycle c)) )

proof end;

:: deftheorem 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 );

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 & vs is_vertex_seq_of p holds

rng vs = the carrier of G

for p being Path of G

for 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

proof end;

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 )

( ex p being cyclic Path of G st p is Eulerian iff for v being Vertex of G holds Degree v is even )

proof end;

theorem :: GRAPH_3:60

for G being connected finite Graph holds

( ex p being Path of G st

( not p is 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 ) ) ) ) )

( ex p being Path of G st

( not p is 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 ) ) ) ) )

proof end;