begin
theorem
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:
theorem Th3:
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
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem Th8:
theorem Th9:
theorem
canceled;
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
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
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
begin
:: 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 & e in X & 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 & e in X & the Source of G . e = v ) ) );
:: 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));
:: 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 Th25:
theorem Th26:
theorem Th27:
theorem Th28:
:: 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 Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
begin
:: 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 & the carrier' of b4 = the carrier' of G \/ { the carrier' of G} & the Source of b4 = the Source of G +* ( the carrier' of G .--> v1) & the Target of b4 = the Target of G +* ( the carrier' of G .--> v2) ) );
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
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 & v in rng vs holds
Degree (v,(rng c)) is even
theorem Th54:
theorem Th55:
:: deftheorem Def8 defines -CycleSet GRAPH_3:def 8 :
for G being Graph
for b2 being FinSequence-DOMAIN 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 Th56:
theorem Th57:
:: 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 & 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
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:
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 :
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 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))) & b4 = (Rotate (c1,v)) ^ (Rotate (c2,v)) ) );
theorem Th58:
:: 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 ) ) } ;
theorem Th59:
:: 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 ) ) } ;
theorem Th60:
theorem Th61:
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:
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) & Degree v9 <> Degree (v9,(rng c)) ) } &
c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) &
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) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) & b1 = CatCycles (c,c9) )
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) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) & b1 = CatCycles (c,c9) ) & 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) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) & 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 & 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) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = choose (( the carrier' of G \ (rng c)) -CycleSet v) & b3 = CatCycles (c,c9) ) );
theorem Th62:
begin
:: 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 Th63:
theorem Th64:
theorem