:: Euler circuits and paths
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received July 29, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem :: GRAPH_3:1
Lm1:
for p being FinSequence
for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds
( (len (m,n -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) ) )
theorem Th2: :: GRAPH_3:2
theorem Th3: :: GRAPH_3:3
Lm2:
for G being Graph
for p being Path of G
for n, m being Element of NAT st 1 <= n & n <= len p & 1 <= m & m <= len p & n <> m holds
p . n <> p . m
theorem :: GRAPH_3:4
canceled;
theorem :: GRAPH_3:5
canceled;
theorem :: GRAPH_3:6
canceled;
theorem Th7: :: GRAPH_3:7
theorem Th8: :: GRAPH_3:8
theorem Th9: :: GRAPH_3:9
theorem :: GRAPH_3:10
canceled;
theorem :: GRAPH_3:11
canceled;
theorem Th12: :: GRAPH_3:12
theorem Th13: :: GRAPH_3:13
theorem Th14: :: GRAPH_3:14
theorem Th15: :: GRAPH_3:15
theorem Th16: :: GRAPH_3:16
theorem Th17: :: GRAPH_3:17
theorem Th18: :: GRAPH_3:18
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) ) ) )
theorem :: GRAPH_3:19
theorem Th20: :: GRAPH_3:20
theorem Th21: :: GRAPH_3:21
theorem Th22: :: GRAPH_3:22
theorem Th23: :: GRAPH_3:23
theorem Th24: :: GRAPH_3:24
:: deftheorem Def1 defines Edges_In GRAPH_3:def 1 :
:: deftheorem Def2 defines Edges_Out GRAPH_3:def 2 :
:: deftheorem defines Edges_At GRAPH_3:def 3 :
:: deftheorem defines Edges_In GRAPH_3:def 4 :
:: deftheorem defines Edges_Out GRAPH_3:def 5 :
theorem Th25: :: GRAPH_3:25
theorem Th26: :: GRAPH_3:26
theorem Th27: :: GRAPH_3:27
theorem Th28: :: GRAPH_3:28
:: deftheorem defines Degree GRAPH_3:def 6 :
theorem Th29: :: GRAPH_3:29
theorem Th30: :: GRAPH_3:30
theorem Th31: :: GRAPH_3:31
theorem Th32: :: GRAPH_3:32
theorem Th33: :: GRAPH_3:33
theorem Th34: :: GRAPH_3:34
theorem Th35: :: GRAPH_3:35
theorem Th36: :: GRAPH_3:36
theorem Th37: :: GRAPH_3:37
theorem Th38: :: GRAPH_3:38
:: deftheorem Def7 defines AddNewEdge GRAPH_3:def 7 :
theorem Th39: :: GRAPH_3:39
theorem Th40: :: GRAPH_3:40
theorem Th41: :: GRAPH_3:41
theorem Th42: :: GRAPH_3:42
theorem :: GRAPH_3:43
theorem Th44: :: GRAPH_3:44
theorem Th45: :: GRAPH_3:45
theorem Th46: :: GRAPH_3:46
theorem Th47: :: GRAPH_3:47
theorem Th48: :: GRAPH_3:48
theorem Th49: :: GRAPH_3:49
theorem Th50: :: GRAPH_3:50
theorem Th51: :: GRAPH_3:51
theorem Th52: :: GRAPH_3:52
theorem Th53: :: GRAPH_3:53
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
theorem Th54: :: GRAPH_3:54
theorem Th55: :: GRAPH_3:55
:: deftheorem Def8 defines -CycleSet GRAPH_3:def 8 :
theorem Th56: :: GRAPH_3:56
theorem Th57: :: GRAPH_3:57
:: deftheorem Def9 defines Rotate GRAPH_3:def 9 :
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
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))) &
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))) & b1 = (Rotate c1,v) ^ (Rotate c2,v) )
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))) & b1 = (Rotate c1,v) ^ (Rotate c2,v) ) & ex v being Vertex of G st
( v = choose ((G -VSet (rng c1)) /\ (G -VSet (rng c2))) & b2 = (Rotate c1,v) ^ (Rotate c2,v) ) holds
b1 = b2;
;
end;
:: deftheorem Def10 defines CatCycles GRAPH_3:def 10 :
theorem Th58: :: GRAPH_3:58
:: deftheorem Def11 defines -PathSet GRAPH_3:def 11 :
theorem Th59: :: GRAPH_3:59
:: deftheorem Def12 defines -CycleSet GRAPH_3:def 12 :
theorem Th60: :: GRAPH_3:60
theorem Th61: :: GRAPH_3:61
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
c' being
Element of
G -CycleSet ex
v being
Vertex of
G st
(
v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } &
c' = choose ((the carrier' of G \ (rng c)) -CycleSet v) &
it = CatCycles c,
c' );
existence
ex b1, c' being Element of G -CycleSet ex v being Vertex of G st
( v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } & c' = choose ((the carrier' of G \ (rng c)) -CycleSet v) & b1 = CatCycles c,c' )
uniqueness
for b1, b2 being Element of G -CycleSet st ex c' being Element of G -CycleSet ex v being Vertex of G st
( v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } & c' = choose ((the carrier' of G \ (rng c)) -CycleSet v) & b1 = CatCycles c,c' ) & ex c' being Element of G -CycleSet ex v being Vertex of G st
( v = choose { v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } & c' = choose ((the carrier' of G \ (rng c)) -CycleSet v) & b2 = CatCycles c,c' ) holds
b1 = b2
;
end;
:: deftheorem Def13 defines ExtendCycle GRAPH_3:def 13 :
theorem Th62: :: GRAPH_3:62
:: deftheorem Def14 defines Eulerian GRAPH_3:def 14 :
theorem Th63: :: GRAPH_3:63
theorem Th64: :: GRAPH_3:64
theorem :: GRAPH_3:65