:: GRAPH_3 semantic presentation

definition

let c₁ be set ;
let c₂ be FinSequence-DOMAIN of c₁;
let c₃ be non empty Subset of c₂;
redefine mode Element as Element of c₃ -> FinSequence of a₁;
coherence

proof end;

end;

registration

let c₁, c₂ be even Integer;
cluster a₁ - a₂ -> even ;
coherence

proof end;

end;

theorem Th1: :: GRAPH_3:1

for b₁, b₂ being Integer holds
( ( b₁ is even iff b₂ is even ) iff b₁ - b₂ is even )

proof end;

theorem Th2: :: GRAPH_3:2

for b₁ being FinSequence
for b₂, b₃, b₄ being Nat st b₄ in dom (b₂,b₃ -cut b₁) holds
ex b₅ being Nat st
( b₅ in dom b₁ & b₁ . b₅ = (b₂,b₃ -cut b₁) . b₄ & b₅ + 1 = b₂ + b₄ & b₂ <= b₅ & b₅ <= b₃ )

proof end;

definition

let c₁ be Graph;
mode Vertex of a₁ is Element of the Vertices of a₁;

end;

theorem Th3: :: GRAPH_3:3

for b₁ being Graph
for b₂ being Chain of b₁
for b₃ being FinSequence of the Vertices of b₁ st b₃ is_vertex_seq_of b₂ holds
not b₃ is empty

proof end;

Lemma4: for b₁ being Graph
for b₂ being Path of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ <= len b₂ & 1 <= b₄ & b₄ <= len b₂ & b₃ <> b₄ holds
b₂ . b₃ <> b₂ . b₄

proof end;

theorem Th4: :: GRAPH_3:4

canceled;

theorem Th5: :: GRAPH_3:5

canceled;

theorem Th6: :: GRAPH_3:6

canceled;

theorem Th7: :: GRAPH_3:7

for b₁ being Graph
for b₂ being set st b₂ in the Edges of b₁ holds
<*b₂*> is Path of b₁

proof end;

theorem Th8: :: GRAPH_3:8

for b₁ being Graph
for b₂ being Path of b₁
for b₃, b₄ being Nat holds b₃,b₄ -cut b₂ is Path of b₁

proof end;

theorem Th9: :: GRAPH_3:9

for b₁ being Graph
for b₂, b₃ being Path of b₁
for b₄, b₅ being FinSequence of the Vertices of b₁ st rng b₂ misses rng b₃ & b₄ is_vertex_seq_of b₂ & b₅ is_vertex_seq_of b₃ & b₄ . (len b₄) = b₅ . 1 holds
b₂ ^ b₃ is Path of b₁

proof end;

theorem Th10: :: GRAPH_3:10

canceled;

theorem Th11: :: GRAPH_3:11

canceled;

theorem Th12: :: GRAPH_3:12

for b₁ being Graph
for b₂ being Chain of b₁ st b₂ = {} holds
b₂ is cyclic

proof end;

registration

let c₁ be Graph;
cluster cyclic Chain of a₁;
existence

proof end;

end;

theorem Th13: :: GRAPH_3:13

for b₁ being Graph
for b₂ being Nat
for b₃ being cyclic Path of b₁ holds ((b₂ + 1),(len b₃) -cut b₃) ^ (1,b₂ -cut b₃) is cyclic Path of b₁

proof end;

theorem Th14: :: GRAPH_3:14

for b₁ being Graph
for b₂ being Path of b₁
for b₃ being Nat st b₃ + 1 in dom b₂ holds
( len (((b₃ + 1),(len b₂) -cut b₂) ^ (1,b₃ -cut b₂)) = len b₂ & rng (((b₃ + 1),(len b₂) -cut b₂) ^ (1,b₃ -cut b₂)) = rng b₂ & (((b₃ + 1),(len b₂) -cut b₂) ^ (1,b₃ -cut b₂)) . 1 = b₂ . (b₃ + 1) )

proof end;

theorem Th15: :: GRAPH_3:15

for b₁ being Graph
for b₂ being Nat
for b₃ being cyclic Path of b₁ st b₂ in dom b₃ holds
ex b₄ being cyclic Path of b₁ st
( b₄ . 1 = b₃ . b₂ & len b₄ = len b₃ & rng b₄ = rng b₃ )

proof end;

theorem Th16: :: GRAPH_3:16

for b₁ being Graph
for b₂ being set
for b₃, b₄ being Vertex of b₁ st b₃ = the Source of b₁ . b₂ & b₄ = the Target of b₁ . b₂ holds
<*b₄,b₃*> is_vertex_seq_of <*b₂*>

proof end;

theorem Th17: :: GRAPH_3:17

for b₁ being Graph
for b₂ being Chain of b₁
for b₃ being FinSequence of the Vertices of b₁
for b₄ being set st b₄ in the Edges of b₁ & b₃ is_vertex_seq_of b₂ & b₃ . (len b₃) = the Source of b₁ . b₄ holds
( b₂ ^ <*b₄*> is Chain of b₁ & ex b₅ being FinSequence of the Vertices of b₁ st
( b₅ = b₃ ^' <*(the Source of b₁ . b₄),(the Target of b₁ . b₄)*> & b₅ is_vertex_seq_of b₂ ^ <*b₄*> & b₅ . 1 = b₃ . 1 & b₅ . (len b₅) = the Target of b₁ . b₄ ) )

proof end;

theorem Th18: :: GRAPH_3:18

for b₁ being Graph
for b₂ being Chain of b₁
for b₃ being FinSequence of the Vertices of b₁
for b₄ being set st b₄ in the Edges of b₁ & b₃ is_vertex_seq_of b₂ & b₃ . (len b₃) = the Target of b₁ . b₄ holds
( b₂ ^ <*b₄*> is Chain of b₁ & ex b₅ being FinSequence of the Vertices of b₁ st
( b₅ = b₃ ^' <*(the Target of b₁ . b₄),(the Source of b₁ . b₄)*> & b₅ is_vertex_seq_of b₂ ^ <*b₄*> & b₅ . 1 = b₃ . 1 & b₅ . (len b₅) = the Source of b₁ . b₄ ) )

proof end;

Lemma15: for b₁ being Graph
for b₂ being Chain of b₁
for b₃ being FinSequence of the Vertices of b₁ st b₃ is_vertex_seq_of b₂ holds
for b₄ being Nat st 1 <= b₄ & b₄ <= len b₂ holds
( 1 <= b₄ & b₄ <= len b₃ & 1 <= b₄ + 1 & b₄ + 1 <= len b₃ & ( ( b₃ . b₄ = the Target of b₁ . (b₂ . b₄) & b₃ . (b₄ + 1) = the Source of b₁ . (b₂ . b₄) ) or ( b₃ . b₄ = the Source of b₁ . (b₂ . b₄) & b₃ . (b₄ + 1) = the Target of b₁ . (b₂ . b₄) ) ) )

proof end;

theorem Th19: :: GRAPH_3:19

for b₁ being Graph
for b₂ being Chain of b₁
for b₃ being FinSequence of the Vertices of b₁ st b₃ is_vertex_seq_of b₂ holds
for b₄ being Nat holds
( not b₄ in dom b₂ or ( b₃ . b₄ = the Target of b₁ . (b₂ . b₄) & b₃ . (b₄ + 1) = the Source of b₁ . (b₂ . b₄) ) or ( b₃ . b₄ = the Source of b₁ . (b₂ . b₄) & b₃ . (b₄ + 1) = the Target of b₁ . (b₂ . b₄) ) )

proof end;

theorem Th20: :: GRAPH_3:20

for b₁ being Graph
for b₂ being Chain of b₁
for b₃ being FinSequence of the Vertices of b₁
for b₄ being set st b₃ is_vertex_seq_of b₂ & b₄ in rng b₂ holds
( the Target of b₁ . b₄ in rng b₃ & the Source of b₁ . b₄ in rng b₃ )

proof end;

definition

let c₁ be Graph;
let c₂ be set ;
redefine func -VSet as c₁ -VSet c₂ -> Subset of the Vertices of a₁;
coherence

proof end;

end;

theorem Th21: :: GRAPH_3:21

for b₁ being Graph holds b₁ -VSet {} = {}

proof end;

theorem Th22: :: GRAPH_3:22

for b₁ being Graph
for b₂, b₃ being set st b₂ in the Edges of b₁ & b₂ in b₃ holds
not b₁ -VSet b₃ is empty

proof end;

theorem Th23: :: GRAPH_3:23

for b₁ being Graph holds
( b₁ is connected iff for b₂, b₃ being Vertex of b₁ st b₂ <> b₃ holds
ex b₄ being Chain of b₁ex b₅ being FinSequence of the Vertices of b₁ st
( not b₄ is empty & b₅ is_vertex_seq_of b₄ & b₅ . 1 = b₂ & b₅ . (len b₅) = b₃ ) )

proof end;

theorem Th24: :: GRAPH_3:24

for b₁ being connected Graph
for b₂ being set
for b₃ being Vertex of b₁ st b₂ meets the Edges of b₁ & not b₃ in b₁ -VSet b₂ holds
ex b₄ being Vertex of b₁ex b₅ being Element of the Edges of b₁ st
( b₄ in b₁ -VSet b₂ & not b₅ in b₂ & ( b₄ = the Target of b₁ . b₅ or b₄ = the Source of b₁ . b₅ ) )

proof end;

definition

let c₁ be Graph;
let c₂ be Vertex of c₁;
let c₃ be set ;
func Edges_In c₂,c₃ -> Subset of the Edges of a₁ means :Def1: :: GRAPH_3:def 1
for b₁ being set holds
( b₁ in a₄ iff ( b₁ in the Edges of a₁ & b₁ in a₃ & the Target of a₁ . b₁ = a₂ ) );
existence

proof end;

uniqueness

proof end;

func Edges_Out c₂,c₃ -> Subset of the Edges of a₁ means :Def2: :: GRAPH_3:def 2
for b₁ being set holds
( b₁ in a₄ iff ( b₁ in the Edges of a₁ & b₁ in a₃ & the Source of a₁ . b₁ = a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Edges_In GRAPH_3:def 1 :

:: deftheorem Def2 defines Edges_Out GRAPH_3:def 2 :

definition

let c₁ be Graph;
let c₂ be Vertex of c₁;
let c₃ be set ;
func Edges_At c₂,c₃ -> Subset of the Edges of a₁ equals :: GRAPH_3:def 3
(Edges_In a₂,a₃) \/ (Edges_Out a₂,a₃);
correctness ;

end;

:: deftheorem Def3 defines Edges_At GRAPH_3:def 3 :

registration

let c₁ be finite Graph;
let c₂ be Vertex of c₁;
let c₃ be set ;
cluster Edges_In a₂,a₃ -> finite ;
correctness

proof end;

cluster Edges_Out a₂,a₃ -> finite ;
correctness

proof end;

cluster Edges_At a₂,a₃ -> finite ;
correctness ;

end;

registration

let c₁ be Graph;
let c₂ be Vertex of c₁;
let c₃ be empty set ;
cluster Edges_In a₂,a₃ -> empty ;
correctness

proof end;

cluster Edges_Out a₂,a₃ -> empty ;
correctness

proof end;

cluster Edges_At a₂,a₃ -> empty ;
correctness ;

end;

definition

let c₁ be Graph;
let c₂ be Vertex of c₁;
func Edges_In c₂ -> Subset of the Edges of a₁ equals :: GRAPH_3:def 4
Edges_In a₂,the Edges of a₁;
correctness ;
func Edges_Out c₂ -> Subset of the Edges of a₁ equals :: GRAPH_3:def 5
Edges_Out a₂,the Edges of a₁;
correctness ;

end;

:: deftheorem Def4 defines Edges_In GRAPH_3:def 4 :

:: deftheorem Def5 defines Edges_Out GRAPH_3:def 5 :

theorem Th25: :: GRAPH_3:25

for b₁ being Graph
for b₂ being Vertex of b₁
for b₃ being set holds Edges_In b₂,b₃ c= Edges_In b₂

proof end;

theorem Th26: :: GRAPH_3:26

for b₁ being Graph
for b₂ being Vertex of b₁
for b₃ being set holds Edges_Out b₂,b₃ c= Edges_Out b₂

proof end;

registration

let c₁ be finite Graph;
let c₂ be Vertex of c₁;
cluster Edges_In a₂ -> finite ;
correctness ;
cluster Edges_Out a₂ -> finite ;
correctness ;

end;

theorem Th27: :: GRAPH_3:27

for b₁ being finite Graph
for b₂ being Vertex of b₁ holds card (Edges_In b₂) = EdgesIn b₂

proof end;

theorem Th28: :: GRAPH_3:28

for b₁ being finite Graph
for b₂ being Vertex of b₁ holds card (Edges_Out b₂) = EdgesOut b₂

proof end;

definition

let c₁ be finite Graph;
let c₂ be Vertex of c₁;
let c₃ be set ;
func Degree c₂,c₃ -> Nat equals :: GRAPH_3:def 6
(card (Edges_In a₂,a₃)) + (card (Edges_Out a₂,a₃));
correctness ;

end;

:: deftheorem Def6 defines Degree GRAPH_3:def 6 :

theorem Th29: :: GRAPH_3:29

for b₁ being finite Graph
for b₂ being Vertex of b₁ holds Degree b₂ = Degree b₂,the Edges of b₁

proof end;

theorem Th30: :: GRAPH_3:30

for b₁ being set
for b₂ being finite Graph
for b₃ being Vertex of b₂ st Degree b₃,b₁ <> 0 holds
not Edges_At b₃,b₁ is empty

proof end;

theorem Th31: :: GRAPH_3:31

for b₁, b₂ being set
for b₃ being finite Graph
for b₄ being Vertex of b₃ st b₁ in the Edges of b₃ & not b₁ in b₂ & ( b₄ = the Target of b₃ . b₁ or b₄ = the Source of b₃ . b₁ ) holds
Degree b₄ <> Degree b₄,b₂

proof end;

theorem Th32: :: GRAPH_3:32

for b₁ being finite Graph
for b₂ being Vertex of b₁
for b₃, b₄ being set st b₃ c= b₄ holds
card (Edges_In b₂,(b₄ \ b₃)) = (card (Edges_In b₂,b₄)) - (card (Edges_In b₂,b₃))

proof end;

theorem Th33: :: GRAPH_3:33

for b₁ being finite Graph
for b₂ being Vertex of b₁
for b₃, b₄ being set st b₃ c= b₄ holds
card (Edges_Out b₂,(b₄ \ b₃)) = (card (Edges_Out b₂,b₄)) - (card (Edges_Out b₂,b₃))

proof end;

theorem Th34: :: GRAPH_3:34

for b₁ being finite Graph
for b₂ being Vertex of b₁
for b₃, b₄ being set st b₃ c= b₄ holds
Degree b₂,(b₄ \ b₃) = (Degree b₂,b₄) - (Degree b₂,b₃)

proof end;

theorem Th35: :: GRAPH_3:35

for b₁ being set
for b₂ being finite Graph
for b₃ being Vertex of b₂ holds
( Edges_In b₃,b₁ = Edges_In b₃,(b₁ /\ the Edges of b₂) & Edges_Out b₃,b₁ = Edges_Out b₃,(b₁ /\ the Edges of b₂) )

proof end;

theorem Th36: :: GRAPH_3:36

for b₁ being set
for b₂ being finite Graph
for b₃ being Vertex of b₂ holds Degree b₃,b₁ = Degree b₃,(b₁ /\ the Edges of b₂)

proof end;

theorem Th37: :: GRAPH_3:37

for b₁ being finite Graph
for b₂ being Vertex of b₁
for b₃ being Chain of b₁
for b₄ being FinSequence of the Vertices of b₁ st not b₃ is empty & b₄ is_vertex_seq_of b₃ holds
( b₂ in rng b₄ iff Degree b₂,(rng b₃) <> 0 )

proof end;

theorem Th38: :: GRAPH_3:38

for b₁ being connected finite non empty Graph
for b₂ being Vertex of b₁ holds Degree b₂ <> 0

proof end;

definition

let c₁ be Graph;
let c₂, c₃ be Vertex of c₁;
func AddNewEdge c₂,c₃ -> strict Graph means :Def7: :: GRAPH_3:def 7
( the Vertices of a₄ = the Vertices of a₁ & the Edges of a₄ = the Edges of a₁ \/ {the Edges of a₁} & the Source of a₄ = the Source of a₁ +* (the Edges of a₁ .--> a₂) & the Target of a₄ = the Target of a₁ +* (the Edges of a₁ .--> a₃) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines AddNewEdge GRAPH_3:def 7 :

registration

let c₁ be finite Graph;
let c₂, c₃ be Vertex of c₁;
cluster AddNewEdge a₂,a₃ -> strict finite ;
coherence

proof end;

end;

theorem Th39: :: GRAPH_3:39

for b₁ being Graph
for b₂, b₃ being Vertex of b₁ holds
( the Edges of b₁ in the Edges of (AddNewEdge b₂,b₃) & the Edges of b₁ = the Edges of (AddNewEdge b₂,b₃) \ {the Edges of b₁} & the Source of (AddNewEdge b₂,b₃) . the Edges of b₁ = b₂ & the Target of (AddNewEdge b₂,b₃) . the Edges of b₁ = b₃ )

proof end;

theorem Th40: :: GRAPH_3:40

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Vertex of b₂ st b₁ in the Edges of b₂ holds
( the Source of (AddNewEdge b₃,b₄) . b₁ = the Source of b₂ . b₁ & the Target of (AddNewEdge b₃,b₄) . b₁ = the Target of b₂ . b₁ )

proof end;

theorem Th41: :: GRAPH_3:41

for b₁ being Graph
for b₂, b₃ being Vertex of b₁
for b₄ being Chain of b₁
for b₅ being FinSequence of the Vertices of b₁
for b₆ being FinSequence of the Vertices of (AddNewEdge b₂,b₃) st b₆ = b₅ & b₅ is_vertex_seq_of b₄ holds
b₆ is_vertex_seq_of b₄

proof end;

theorem Th42: :: GRAPH_3:42

for b₁ being Graph
for b₂, b₃ being Vertex of b₁
for b₄ being Chain of b₁ holds b₄ is Chain of AddNewEdge b₂,b₃

proof end;

theorem Th43: :: GRAPH_3:43

for b₁ being Graph
for b₂, b₃ being Vertex of b₁
for b₄ being Path of b₁ holds b₄ is Path of AddNewEdge b₂,b₃ by Th42;

theorem Th44: :: GRAPH_3:44

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Vertex of b₂
for b₅ being Vertex of (AddNewEdge b₃,b₄) st b₅ = b₃ & b₃ <> b₄ holds
Edges_In b₅,b₁ = Edges_In b₃,b₁

proof end;

theorem Th45: :: GRAPH_3:45

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Vertex of b₂
for b₅ being Vertex of (AddNewEdge b₄,b₃) st b₅ = b₃ & b₄ <> b₃ holds
Edges_Out b₅,b₁ = Edges_Out b₃,b₁

proof end;

theorem Th46: :: GRAPH_3:46

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Vertex of b₂
for b₅ being Vertex of (AddNewEdge b₃,b₄) st b₅ = b₃ & b₃ <> b₄ & the Edges of b₂ in b₁ holds
( Edges_Out b₅,b₁ = (Edges_Out b₃,b₁) \/ {the Edges of b₂} & Edges_Out b₃,b₁ misses {the Edges of b₂} )

proof end;

theorem Th47: :: GRAPH_3:47

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Vertex of b₂
for b₅ being Vertex of (AddNewEdge b₄,b₃) st b₅ = b₃ & b₄ <> b₃ & the Edges of b₂ in b₁ holds
( Edges_In b₅,b₁ = (Edges_In b₃,b₁) \/ {the Edges of b₂} & Edges_In b₃,b₁ misses {the Edges of b₂} )

proof end;

theorem Th48: :: GRAPH_3:48

for b₁ being set
for b₂ being Graph
for b₃, b₄, b₅ being Vertex of b₂
for b₆ being Vertex of (AddNewEdge b₄,b₅) st b₆ = b₃ & b₃ <> b₄ & b₃ <> b₅ holds
Edges_In b₆,b₁ = Edges_In b₃,b₁

proof end;

theorem Th49: :: GRAPH_3:49

for b₁ being set
for b₂ being Graph
for b₃, b₄, b₅ being Vertex of b₂
for b₆ being Vertex of (AddNewEdge b₄,b₅) st b₆ = b₃ & b₃ <> b₄ & b₃ <> b₅ holds
Edges_Out b₆,b₁ = Edges_Out b₃,b₁

proof end;

theorem Th50: :: GRAPH_3:50

for b₁ being Graph
for b₂, b₃ being Vertex of b₁
for b₄ being Path of AddNewEdge b₂,b₃ st not the Edges of b₁ in rng b₄ holds
b₄ is Path of b₁

proof end;

theorem Th51: :: GRAPH_3:51

for b₁ being Graph
for b₂, b₃ being Vertex of b₁
for b₄ being FinSequence of the Vertices of b₁
for b₅ being Path of AddNewEdge b₂,b₃
for b₆ being FinSequence of the Vertices of (AddNewEdge b₂,b₃) st not the Edges of b₁ in rng b₅ & b₄ = b₆ & b₆ is_vertex_seq_of b₅ holds
b₄ is_vertex_seq_of b₅

proof end;

registration

let c₁ be connected Graph;
let c₂, c₃ be Vertex of c₁;
cluster AddNewEdge a₂,a₃ -> strict connected ;
coherence

proof end;

end;

theorem Th52: :: GRAPH_3:52

for b₁ being set
for b₂ being finite Graph
for b₃, b₄, b₅ being Vertex of b₂
for b₆ being Vertex of (AddNewEdge b₄,b₅) st b₆ = b₃ & b₄ <> b₅ & ( b₃ = b₄ or b₃ = b₅ ) & the Edges of b₂ in b₁ holds
Degree b₆,b₁ = (Degree b₃,b₁) + 1

proof end;

theorem Th53: :: GRAPH_3:53

for b₁ being set
for b₂ being finite Graph
for b₃, b₄, b₅ being Vertex of b₂
for b₆ being Vertex of (AddNewEdge b₄,b₅) st b₆ = b₃ & b₃ <> b₄ & b₃ <> b₅ holds
Degree b₆,b₁ = Degree b₃,b₁

proof end;

Lemma52: for b₁ being finite Graph
for b₂ being cyclic Path of b₁
for b₃ being FinSequence of the Vertices of b₁
for b₄ being Vertex of b₁ st b₃ is_vertex_seq_of b₂ & b₄ in rng b₃ holds
Degree b₄,(rng b₂) is even

proof end;

theorem Th54: :: GRAPH_3:54

for b₁ being finite Graph
for b₂ being Vertex of b₁
for b₃ being cyclic Path of b₁ holds Degree b₂,(rng b₃) is even

proof end;

theorem Th55: :: GRAPH_3:55

for b₁ being finite Graph
for b₂ being Vertex of b₁
for b₃ being FinSequence of the Vertices of b₁
for b₄ being Path of b₁ st not b₄ is cyclic & b₃ is_vertex_seq_of b₄ holds
( Degree b₂,(rng b₄) is even iff ( b₂ <> b₃ . 1 & b₂ <> b₃ . (len b₃) ) )

proof end;

definition

let c₁ be Graph;
func c₁ -CycleSet -> FinSequence-DOMAIN of the Edges of a₁ means :Def8: :: GRAPH_3:def 8
for b₁ being set holds
( b₁ in a₂ iff b₁ is cyclic Path of a₁ );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th56: :: GRAPH_3:56

for b₁ being Graph holds {} is Element of b₁ -CycleSet

proof end;

theorem Th57: :: GRAPH_3:57

for b₁ being Graph
for b₂ being Vertex of b₁
for b₃ being Element of b₁ -CycleSet st b₂ in b₁ -VSet (rng b₃) holds
{ b₄ where B is Element of b₁ -CycleSet : ( rng b₄ = rng b₃ & ex b₁ being FinSequence of the Vertices of b₁ st
( b₅ is_vertex_seq_of b₄ & b₅ . 1 = b₂ ) ) } is non empty Subset of (b₁ -CycleSet )

proof end;

definition

let c₁ be Graph;
let c₂ be Vertex of c₁;
let c₃ be Element of c₁ -CycleSet ;
assume E58: c₂ in c₁ -VSet (rng c₃) ;
func Rotate c₃,c₂ -> Element of a₁ -CycleSet equals :Def9: :: GRAPH_3:def 9
choose { b₁ where B is Element of a₁ -CycleSet : ( rng b₁ = rng a₃ & ex b₁ being FinSequence of the Vertices of a₁ st
( b₂ is_vertex_seq_of b₁ & b₂ . 1 = a₂ ) ) } ;
coherence

proof end;

end;

:: deftheorem Def9 defines Rotate GRAPH_3:def 9 :

Lemma59: for b₁ being Graph
for b₂ being Element of b₁ -CycleSet
for b₃ being Vertex of b₁ st b₃ in b₁ -VSet (rng b₂) holds
rng (Rotate b₂,b₃) = rng b₂

proof end;

definition

let c₁ be Graph;
let c₂, c₃ be Element of c₁ -CycleSet ;
assume that
E60: c₁ -VSet (rng c₂) meets c₁ -VSet (rng c₃) and
E61: rng c₂ misses rng c₃ ;
func CatCycles c₂,c₃ -> Element of a₁ -CycleSet means :Def10: :: GRAPH_3:def 10
ex b₁ being Vertex of a₁ st
( b₁ = choose ((a₁ -VSet (rng a₂)) /\ (a₁ -VSet (rng a₃))) & a₄ = (Rotate a₂,b₁) ^ (Rotate a₃,b₁) );
existence

proof end;

correctness ;

end;

:: deftheorem Def10 defines CatCycles GRAPH_3:def 10 :

theorem Th58: :: GRAPH_3:58

for b₁ being Graph
for b₂, b₃ being Element of b₁ -CycleSet st b₁ -VSet (rng b₂) meets b₁ -VSet (rng b₃) & rng b₂ misses rng b₃ & ( b₂ <> {} or b₃ <> {} ) holds
not CatCycles b₂,b₃ is empty

proof end;

definition

let c₁ be finite Graph;
let c₂ be Vertex of c₁;
let c₃ be set ;
assume E62: Degree c₂,c₃ <> 0 ;
func c₃ -PathSet c₂ -> FinSequence-DOMAIN of the Edges of a₁ equals :Def11: :: GRAPH_3:def 11
{ b₁ where B is Element of a₃ * : ( b₁ is Path of a₁ & not b₁ is empty & ex b₁ being FinSequence of the Vertices of a₁ st
( b₂ is_vertex_seq_of b₁ & b₂ . 1 = a₂ ) ) } ;
coherence

proof end;

end;

:: deftheorem Def11 defines -PathSet GRAPH_3:def 11 :

theorem Th59: :: GRAPH_3:59

for b₁ being set
for b₂ being finite Graph
for b₃ being Vertex of b₂
for b₄ being Element of b₁ -PathSet b₃
for b₅ being finite set st b₅ = the Edges of b₂ & Degree b₃,b₁ <> 0 holds
len b₄ <= card b₅

proof end;

definition

let c₁ be finite Graph;
let c₂ be Vertex of c₁;
let c₃ be set ;
assume that
E64: for b₁ being Vertex of c₁ holds Degree b₁,c₃ is even and
E65: Degree c₂,c₃ <> 0 ;
func c₃ -CycleSet c₂ -> non empty Subset of (a₁ -CycleSet ) equals :Def12: :: GRAPH_3:def 12
{ b₁ where B is Element of a₁ -CycleSet : ( rng b₁ c= a₃ & not b₁ is empty & ex b₁ being FinSequence of the Vertices of a₁ st
( b₂ is_vertex_seq_of b₁ & b₂ . 1 = a₂ ) ) } ;
coherence

proof end;

end;

:: deftheorem Def12 defines -CycleSet GRAPH_3:def 12 :

theorem Th60: :: GRAPH_3:60

for b₁ being set
for b₂ being finite Graph
for b₃ being Vertex of b₂ st Degree b₃,b₁ <> 0 & ( for b₄ being Vertex of b₂ holds Degree b₄,b₁ is even ) holds
for b₄ being Element of b₁ -CycleSet b₃ holds
( not b₄ is empty & rng b₄ c= b₁ & b₃ in b₂ -VSet (rng b₄) )

proof end;

theorem Th61: :: GRAPH_3:61

for b₁ being connected finite Graph
for b₂ being Element of b₁ -CycleSet st rng b₂ <> the Edges of b₁ & not b₂ is empty holds
{ b₃ where B is Vertex of b₁ : ( b₃ in b₁ -VSet (rng b₂) & Degree b₃ <> Degree b₃,(rng b₂) ) } is non empty Subset of the Vertices of b₁

proof end;

definition

let c₁ be connected finite Graph;
let c₂ be Element of c₁ -CycleSet ;
assume that
E67: rng c₂ <> the Edges of c₁ and
E68: not c₂ is empty ;
func ExtendCycle c₂ -> Element of a₁ -CycleSet means :Def13: :: GRAPH_3:def 13
ex b₁ being Element of a₁ -CycleSet ex b₂ being Vertex of a₁ st
( b₂ = choose { b₃ where B is Vertex of a₁ : ( b₃ in a₁ -VSet (rng a₂) & Degree b₃ <> Degree b₃,(rng a₂) ) } & b₁ = choose ((the Edges of a₁ \ (rng a₂)) -CycleSet b₂) & a₃ = CatCycles a₂,b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def13 defines ExtendCycle GRAPH_3:def 13 :

theorem Th62: :: GRAPH_3:62

for b₁ being connected finite Graph
for b₂ being Element of b₁ -CycleSet st rng b₂ <> the Edges of b₁ & not b₂ is empty & ( for b₃ being Vertex of b₁ holds Degree b₃ is even ) holds
( not ExtendCycle b₂ is empty & card (rng b₂) < card (rng (ExtendCycle b₂)) )

proof end;

definition

let c₁ be Graph;
let c₂ be Path of c₁;
attr a₂ is Eulerian means :Def14: :: GRAPH_3:def 14
rng a₂ = the Edges of a₁;

end;

:: deftheorem Def14 defines Eulerian GRAPH_3:def 14 :

theorem Th63: :: GRAPH_3:63

for b₁ being connected Graph
for b₂ being Path of b₁
for b₃ being FinSequence of the Vertices of b₁ st b₂ is Eulerian & b₃ is_vertex_seq_of b₂ holds
rng b₃ = the Vertices of b₁

proof end;

theorem Th64: :: GRAPH_3:64

for b₁ being connected finite Graph holds
( ex b₂ being cyclic Path of b₁ st b₂ is Eulerian iff for b₂ being Vertex of b₁ holds Degree b₂ is even )

proof end;

theorem Th65: :: GRAPH_3:65

for b₁ being connected finite Graph holds
( ex b₂ being Path of b₁ st
( not b₂ is cyclic & b₂ is Eulerian ) iff ex b₂, b₃ being Vertex of b₁ st
( b₂ <> b₃ & ( for b₄ being Vertex of b₁ holds
( Degree b₄ is even iff ( b₄ <> b₂ & b₄ <> b₃ ) ) ) ) )

proof end;