:: GRAPH_3 semantic presentation

definition

let D be set ;
let T be FinSequence-DOMAIN of D;
let S be non empty Subset of T;
:: original: Element
redefine mode Element of S -> FinSequence of D;
coherence

proof end;

end;

registration

let i, j be even Integer;
cluster i - j -> even ;
coherence

proof end;

end;

theorem Th1: :: GRAPH_3:1

for i, j being Integer holds
( ( i is even iff j is even ) iff i - j is even )

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 )

proof end;

definition

let G be Graph;
mode Vertex of G is Element of the Vertices of G;

end;

theorem Th3: :: GRAPH_3:3

for G being Graph
for c being Chain of G
for vs being FinSequence of the Vertices of G st vs is_vertex_seq_of c holds
not vs is empty

proof end;

Lm1: 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 :: GRAPH_3:4

canceled;

theorem :: GRAPH_3:5

canceled;

theorem :: GRAPH_3:6

canceled;

theorem Th7: :: GRAPH_3:7

for G being Graph
for e being set st e in the Edges of G holds
<*e*> is Path of G

proof end;

theorem Th8: :: GRAPH_3:8

for G being Graph
for p being Path of G
for m, n being Nat holds m,n -cut p is Path of G

proof end;

theorem Th9: :: GRAPH_3:9

for G being Graph
for p1, p2 being Path of G
for vs1, vs2 being FinSequence of the Vertices 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;

theorem :: GRAPH_3:10

canceled;

theorem :: GRAPH_3:11

canceled;

theorem Th12: :: GRAPH_3:12

for G being Graph
for c being Chain of G st c = {} holds
c is cyclic

proof end;

registration

let G be Graph;
cluster cyclic Chain of G;
existence

proof end;

end;

theorem Th13: :: GRAPH_3:13

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

proof end;

theorem Th14: :: GRAPH_3:14

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

proof end;

theorem Th15: :: GRAPH_3:15

for G being Graph
for n being Nat
for p being cyclic Path of G st n in dom p holds
ex p' being cyclic Path of G st
( p' . 1 = p . n & len p' = len p & rng p' = rng p )

proof end;

theorem Th16: :: GRAPH_3:16

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

proof end;

theorem Th17: :: GRAPH_3:17

for G being Graph
for c being Chain of G
for vs being FinSequence of the Vertices of G
for e being set st e in the Edges of G & vs is_vertex_seq_of c & vs . (len vs) = the Source of G . e holds
( c ^ <*e*> is Chain of G & ex vs' being FinSequence of the Vertices of G st
( vs' = vs ^' <*(the Source of G . e),(the Target of G . e)*> & vs' is_vertex_seq_of c ^ <*e*> & vs' . 1 = vs . 1 & vs' . (len vs') = the Target of G . e ) )

proof end;

theorem Th18: :: GRAPH_3:18

for G being Graph
for c being Chain of G
for vs being FinSequence of the Vertices of G
for e being set st e in the Edges of G & vs is_vertex_seq_of c & vs . (len vs) = the Target of G . e holds
( c ^ <*e*> is Chain of G & ex vs' being FinSequence of the Vertices of G st
( vs' = vs ^' <*(the Target of G . e),(the Source of G . e)*> & vs' is_vertex_seq_of c ^ <*e*> & vs' . 1 = vs . 1 & vs' . (len vs') = the Source of G . e ) )

proof end;

Lm2: for G being Graph
for c being Chain of G
for vs being FinSequence of the Vertices 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:19

for G being Graph
for c being Chain of G
for vs being FinSequence of the Vertices of G st vs is_vertex_seq_of c holds
for n being 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 Th20: :: GRAPH_3:20

for G being Graph
for c being Chain of G
for vs being FinSequence of the Vertices 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 Vertices of G;
coherence

proof end;

end;

theorem Th21: :: GRAPH_3:21

for G being Graph holds G -VSet {} = {}

proof end;

theorem Th22: :: GRAPH_3:22

for G being Graph
for e, X being set st e in the Edges of G & e in X holds
not G -VSet X is empty

proof end;

theorem Th23: :: GRAPH_3:23

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 Vertices of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )

proof end;

theorem Th24: :: GRAPH_3:24

for G being connected Graph
for X being set
for v being Vertex of G st X meets the Edges of G & not v in G -VSet X holds
ex v' being Vertex of G ex e being Element of the Edges of G st
( v' in G -VSet X & not e in X & ( v' = the Target of G . e or v' = the Source of G . e ) )

proof end;

definition

let G be Graph;
let v be Vertex of G;
let X be set ;
func Edges_In v,X -> Subset of the Edges of G means :Def1: :: GRAPH_3:def 1
for e being set holds
( e in it iff ( e in the Edges of G & e in X & the Target of G . e = v ) );
existence

proof end;

uniqueness

proof end;

func Edges_Out v,X -> Subset of the Edges of G means :Def2: :: GRAPH_3:def 2
for e being set holds
( e in it iff ( e in the Edges of G & e in X & the Source of G . e = v ) );
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 G be Graph;
let v be Vertex of G;
let X be set ;
func Edges_At v,X -> Subset of the Edges of G equals :: GRAPH_3:def 3
(Edges_In v,X) \/ (Edges_Out v,X);
correctness ;

end;

:: deftheorem defines Edges_At GRAPH_3:def 3 :

registration

let G be finite Graph;
let v be Vertex of G;
let X be set ;
cluster Edges_In v,X -> finite ;
correctness

proof end;

cluster Edges_Out v,X -> finite ;
correctness

proof end;

cluster Edges_At v,X -> finite ;
correctness ;

end;

registration

let G be Graph;
let v be Vertex of G;
let X be empty set ;
cluster Edges_In v,X -> empty ;
correctness

proof end;

cluster Edges_Out v,X -> empty ;
correctness

proof end;

cluster Edges_At v,X -> empty ;
correctness ;

end;

definition

let G be Graph;
let v be Vertex of G;
func Edges_In v -> Subset of the Edges of G equals :: GRAPH_3:def 4
Edges_In v,the Edges of G;
correctness ;
func Edges_Out v -> Subset of the Edges of G equals :: GRAPH_3:def 5
Edges_Out v,the Edges of G;
correctness ;

end;

:: deftheorem defines Edges_In GRAPH_3:def 4 :

:: deftheorem defines Edges_Out GRAPH_3:def 5 :

theorem Th25: :: GRAPH_3:25

for G being Graph
for v being Vertex of G
for X being set holds Edges_In v,X c= Edges_In v

proof end;

theorem Th26: :: GRAPH_3:26

for G being Graph
for v being Vertex of G
for X being set holds Edges_Out v,X c= Edges_Out v

proof end;

registration

let G be finite Graph;
let v be Vertex of G;
cluster Edges_In v -> finite ;
correctness ;
cluster Edges_Out v -> finite ;
correctness ;

end;

theorem Th27: :: GRAPH_3:27

for G being finite Graph
for v being Vertex of G holds card (Edges_In v) = EdgesIn v

proof end;

theorem Th28: :: GRAPH_3:28

for G being finite Graph
for v being Vertex of G holds card (Edges_Out v) = EdgesOut v

proof end;

definition

let G be finite Graph;
let v be Vertex of G;
let X be set ;
func Degree v,X -> Nat equals :: GRAPH_3:def 6
(card (Edges_In v,X)) + (card (Edges_Out v,X));
correctness ;

end;

:: deftheorem defines Degree GRAPH_3:def 6 :

theorem Th29: :: GRAPH_3:29

for G being finite Graph
for v being Vertex of G holds Degree v = Degree v,the Edges of G

proof end;

theorem Th30: :: GRAPH_3:30

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

proof end;

theorem Th31: :: GRAPH_3:31

for e, X being set
for G being finite Graph
for v being Vertex of G st e in the Edges 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 Th32: :: GRAPH_3:32

for G being finite Graph
for v being Vertex of G
for X2, X1 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 Th33: :: GRAPH_3:33

for G being finite Graph
for v being Vertex of G
for X2, X1 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 Th34: :: GRAPH_3:34

for G being finite Graph
for v being Vertex of G
for X2, X1 being set st X2 c= X1 holds
Degree v,(X1 \ X2) = (Degree v,X1) - (Degree v,X2)

proof end;

theorem Th35: :: GRAPH_3:35

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

proof end;

theorem Th36: :: GRAPH_3:36

for X being set
for G being finite Graph
for v being Vertex of G holds Degree v,X = Degree v,(X /\ the Edges of G)

proof end;

theorem Th37: :: GRAPH_3:37

for G being finite Graph
for v being Vertex of G
for c being Chain of G
for vs being FinSequence of the Vertices 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;

theorem Th38: :: GRAPH_3:38

for G being connected finite non empty Graph
for v being Vertex of G holds Degree v <> 0

proof end;

definition

let G be Graph;
let v1, v2 be Vertex of G;
func AddNewEdge v1,v2 -> strict Graph means :Def7: :: GRAPH_3:def 7
( the Vertices of it = the Vertices of G & the Edges of it = the Edges of G \/ {the Edges of G} & the Source of it = the Source of G +* (the Edges of G .--> v1) & the Target of it = the Target of G +* (the Edges of G .--> v2) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines AddNewEdge GRAPH_3:def 7 :

registration

let G be finite Graph;
let v1, v2 be Vertex of G;
cluster AddNewEdge v1,v2 -> strict finite ;
coherence

proof end;

end;

theorem Th39: :: GRAPH_3:39

for G being Graph
for v1, v2 being Vertex of G holds
( the Edges of G in the Edges of (AddNewEdge v1,v2) & the Edges of G = the Edges of (AddNewEdge v1,v2) \ {the Edges of G} & the Source of (AddNewEdge v1,v2) . the Edges of G = v1 & the Target of (AddNewEdge v1,v2) . the Edges of G = v2 )

proof end;

theorem Th40: :: GRAPH_3:40

for e being set
for G being Graph
for v1, v2 being Vertex of G st e in the Edges 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 Th41: :: GRAPH_3:41

for G being Graph
for v1, v2 being Vertex of G
for c being Chain of G
for vs being FinSequence of the Vertices of G
for vs' being FinSequence of the Vertices of (AddNewEdge v1,v2) st vs' = vs & vs is_vertex_seq_of c holds
vs' is_vertex_seq_of c

proof end;

theorem Th42: :: GRAPH_3:42

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

proof end;

theorem :: GRAPH_3:43

for G being Graph
for v1, v2 being Vertex of G
for p being Path of G holds p is Path of AddNewEdge v1,v2 by Th42;

theorem Th44: :: GRAPH_3:44

for X being set
for G being Graph
for v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v1 & v1 <> v2 holds
Edges_In v',X = Edges_In v1,X

proof end;

theorem Th45: :: GRAPH_3:45

for X being set
for G being Graph
for v2, v1 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v2 & v1 <> v2 holds
Edges_Out v',X = Edges_Out v2,X

proof end;

theorem Th46: :: GRAPH_3:46

for X being set
for G being Graph
for v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v1 & v1 <> v2 & the Edges of G in X holds
( Edges_Out v',X = (Edges_Out v1,X) \/ {the Edges of G} & Edges_Out v1,X misses {the Edges of G} )

proof end;

theorem Th47: :: GRAPH_3:47

for X being set
for G being Graph
for v2, v1 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v2 & v1 <> v2 & the Edges of G in X holds
( Edges_In v',X = (Edges_In v2,X) \/ {the Edges of G} & Edges_In v2,X misses {the Edges of G} )

proof end;

theorem Th48: :: GRAPH_3:48

for X being set
for G being Graph
for v, v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v <> v1 & v <> v2 holds
Edges_In v',X = Edges_In v,X

proof end;

theorem Th49: :: GRAPH_3:49

for X being set
for G being Graph
for v, v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v <> v1 & v <> v2 holds
Edges_Out v',X = Edges_Out v,X

proof end;

theorem Th50: :: GRAPH_3:50

for G being Graph
for v1, v2 being Vertex of G
for p' being Path of AddNewEdge v1,v2 st not the Edges of G in rng p' holds
p' is Path of G

proof end;

theorem Th51: :: GRAPH_3:51

for G being Graph
for v1, v2 being Vertex of G
for vs being FinSequence of the Vertices of G
for p' being Path of AddNewEdge v1,v2
for vs' being FinSequence of the Vertices of (AddNewEdge v1,v2) st not the Edges of G in rng p' & vs = vs' & vs' is_vertex_seq_of p' holds
vs is_vertex_seq_of p'

proof end;

registration

let G be connected Graph;
let v1, v2 be Vertex of G;
cluster AddNewEdge v1,v2 -> strict connected ;
coherence

proof end;

end;

theorem Th52: :: GRAPH_3:52

for X being set
for G being finite Graph
for v, v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v1 <> v2 & ( v = v1 or v = v2 ) & the Edges of G in X holds
Degree v',X = (Degree v,X) + 1

proof end;

theorem Th53: :: GRAPH_3:53

for X being set
for G being finite Graph
for v, v1, v2 being Vertex of G
for v' being Vertex of (AddNewEdge v1,v2) st v' = v & v <> v1 & v <> v2 holds
Degree v',X = Degree v,X

proof end;

Lm3: for G being finite Graph
for c being cyclic Path of G
for vs being FinSequence of the Vertices 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 Th54: :: GRAPH_3:54

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

proof end;

theorem Th55: :: GRAPH_3:55

for G being finite Graph
for v being Vertex of G
for vs being FinSequence of the Vertices 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;
func G -CycleSet -> FinSequence-DOMAIN of the Edges of G means :Def8: :: GRAPH_3:def 8
for x being set holds
( x in it iff x is cyclic Path of G );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th56: :: GRAPH_3:56

for G being Graph holds {} is Element of G -CycleSet

proof end;

theorem Th57: :: GRAPH_3:57

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
{ c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the Vertices of G st
( vs is_vertex_seq_of c' & 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) ;
func Rotate c,v -> Element of G -CycleSet equals :Def9: :: GRAPH_3:def 9
choose { c' where c' is Element of G -CycleSet : ( rng c' = rng c & ex vs being FinSequence of the Vertices of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) } ;
coherence

proof end;

end;

:: deftheorem Def9 defines Rotate GRAPH_3:def 9 :

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

proof end;

correctness ;

end;

:: deftheorem Def10 defines CatCycles GRAPH_3:def 10 :

theorem Th58: :: GRAPH_3:58

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

proof end;

definition

let G be finite Graph;
let v be Vertex of G;
let X be set ;
assume A1: Degree v,X <> 0 ;
func X -PathSet v -> FinSequence-DOMAIN of the Edges 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 Vertices of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;
coherence

proof end;

end;

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

theorem Th59: :: GRAPH_3:59

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 Edges 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 ;
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 Vertices of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;
coherence

proof end;

end;

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

theorem Th60: :: GRAPH_3:60

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

proof end;

theorem Th61: :: GRAPH_3:61

for G being connected finite Graph
for c being Element of G -CycleSet st rng c <> the Edges of G & not c is empty holds
{ v' where v' is Vertex of G : ( v' in G -VSet (rng c) & Degree v' <> Degree v',(rng c) ) } is non empty Subset of the Vertices of G

proof end;

definition

let G be connected finite Graph;
let c be Element of G -CycleSet ;
assume that
A1: rng c <> the Edges 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 Edges of G \ (rng c)) -CycleSet v) & it = CatCycles c,c' );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def13 defines ExtendCycle GRAPH_3:def 13 :

theorem Th62: :: GRAPH_3:62

for G being connected finite Graph
for c being Element of G -CycleSet st rng c <> the Edges 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;

definition

let G be Graph;
let p be Path of G;
attr p is Eulerian means :Def14: :: GRAPH_3:def 14
rng p = the Edges of G;

end;

:: deftheorem Def14 defines Eulerian GRAPH_3:def 14 :

theorem Th63: :: GRAPH_3:63

for G being connected Graph
for p being Path of G
for vs being FinSequence of the Vertices of G st p is Eulerian & vs is_vertex_seq_of p holds
rng vs = the Vertices of G

proof end;

theorem Th64: :: GRAPH_3:64

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 )

proof end;

theorem :: GRAPH_3:65

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

proof end;