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 :
:: 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:
theorem Th26:
theorem Th27:
theorem Th28:
:: deftheorem defines Degree GRAPH_3:def 6 :
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 :
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 :
theorem Th56:
theorem Th57:
:: 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:
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:
:: deftheorem Def11 defines -PathSet GRAPH_3:def 11 :
theorem Th59:
:: deftheorem Def12 defines -CycleSet GRAPH_3:def 12 :
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 :
theorem Th62:
begin
:: deftheorem Def14 defines Eulerian GRAPH_3:def 14 :
theorem Th63:
theorem Th64:
theorem