:: by Krzysztof Hryniewiecki

::

:: Received December 5, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct MultiGraphStruct -> 2-sorted ;

aggr MultiGraphStruct(# carrier, carrier', Source, Target #) -> MultiGraphStruct ;

sel Source c_{1} -> Function of the carrier' of c_{1}, the carrier of c_{1};

sel Target c_{1} -> Function of the carrier' of c_{1}, the carrier of c_{1};

end;
struct MultiGraphStruct -> 2-sorted ;

aggr MultiGraphStruct(# carrier, carrier', Source, Target #) -> MultiGraphStruct ;

sel Source c

sel Target c

definition

let G be MultiGraphStruct ;

mode Vertex of G is Element of G;

mode Edge of G is Element of the carrier' of G;

end;
mode Vertex of G is Element of G;

mode Edge of G is Element of the carrier' of G;

registration

existence

ex b_{1} being MultiGraphStruct st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void )

end;
ex b

( b

proof end;

:: from CAT_1, 2008.07.02, A.T.

definition

let C be MultiGraphStruct ;

let f be Edge of C;

( ( not C is void & not C is empty implies the Source of C . f is Vertex of C ) & ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) )

for b_{1} being Vertex of C holds verum
;

coherence

( ( not C is void & not C is empty implies the Target of C . f is Vertex of C ) & ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) );

consistency

for b_{1} being Vertex of C holds verum;

end;
let f be Edge of C;

func dom f -> Vertex of C equals :Def1: :: GRAPH_1:def 1

the Source of C . f if ( not C is void & not C is empty )

otherwise the Vertex of C;

coherence the Source of C . f if ( not C is void & not C is empty )

otherwise the Vertex of C;

( ( not C is void & not C is empty implies the Source of C . f is Vertex of C ) & ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) )

proof end;

consistency for b

func cod f -> Vertex of C equals :Def2: :: GRAPH_1:def 2

the Target of C . f if ( not C is void & not C is empty )

otherwise the Vertex of C;

correctness the Target of C . f if ( not C is void & not C is empty )

otherwise the Vertex of C;

coherence

( ( not C is void & not C is empty implies the Target of C . f is Vertex of C ) & ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) );

consistency

for b

proof end;

:: deftheorem Def1 defines dom GRAPH_1:def 1 :

for C being MultiGraphStruct

for f being Edge of C holds

( ( not C is void & not C is empty implies dom f = the Source of C . f ) & ( ( C is void or C is empty ) implies dom f = the Vertex of C ) );

for C being MultiGraphStruct

for f being Edge of C holds

( ( not C is void & not C is empty implies dom f = the Source of C . f ) & ( ( C is void or C is empty ) implies dom f = the Vertex of C ) );

:: deftheorem Def2 defines cod GRAPH_1:def 2 :

for C being MultiGraphStruct

for f being Edge of C holds

( ( not C is void & not C is empty implies cod f = the Target of C . f ) & ( ( C is void or C is empty ) implies cod f = the Vertex of C ) );

for C being MultiGraphStruct

for f being Edge of C holds

( ( not C is void & not C is empty implies cod f = the Target of C . f ) & ( ( C is void or C is empty ) implies cod f = the Vertex of C ) );

definition

let C be non empty non void MultiGraphStruct ;

let f be Edge of C;

compatibility

for b_{1} being Vertex of C holds

( b_{1} = dom f iff b_{1} = the Source of C . f )
by Def1;

coherence

dom f is Vertex of C ;

compatibility

for b_{1} being Vertex of C holds

( b_{1} = cod f iff b_{1} = the Target of C . f )
by Def2;

coherence

cod f is Vertex of C ;

end;
let f be Edge of C;

compatibility

for b

( b

coherence

dom f is Vertex of C ;

compatibility

for b

( b

coherence

cod f is Vertex of C ;

:: deftheorem defines dom GRAPH_1:def 3 :

for C being non empty non void MultiGraphStruct

for f being Edge of C holds dom f = the Source of C . f;

for C being non empty non void MultiGraphStruct

for f being Edge of C holds dom f = the Source of C . f;

:: deftheorem defines cod GRAPH_1:def 4 :

for C being non empty non void MultiGraphStruct

for f being Edge of C holds cod f = the Target of C . f;

for C being non empty non void MultiGraphStruct

for f being Edge of C holds cod f = the Target of C . f;

definition

let G1, G2 be Graph;

assume that

A1: the Source of G1 tolerates the Source of G2 and

A2: the Target of G1 tolerates the Target of G2 ;

ex b_{1} being strict Graph st

( the carrier of b_{1} = the carrier of G1 \/ the carrier of G2 & the carrier' of b_{1} = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds

( the Source of b_{1} . v = the Source of G1 . v & the Target of b_{1} . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds

( the Source of b_{1} . v = the Source of G2 . v & the Target of b_{1} . v = the Target of G2 . v ) ) )

for b_{1}, b_{2} being strict Graph st the carrier of b_{1} = the carrier of G1 \/ the carrier of G2 & the carrier' of b_{1} = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds

( the Source of b_{1} . v = the Source of G1 . v & the Target of b_{1} . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds

( the Source of b_{1} . v = the Source of G2 . v & the Target of b_{1} . v = the Target of G2 . v ) ) & the carrier of b_{2} = the carrier of G1 \/ the carrier of G2 & the carrier' of b_{2} = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds

( the Source of b_{2} . v = the Source of G1 . v & the Target of b_{2} . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds

( the Source of b_{2} . v = the Source of G2 . v & the Target of b_{2} . v = the Target of G2 . v ) ) holds

b_{1} = b_{2}

end;
assume that

A1: the Source of G1 tolerates the Source of G2 and

A2: the Target of G1 tolerates the Target of G2 ;

func G1 \/ G2 -> strict Graph means :Def5: :: GRAPH_1:def 5

( the carrier of it = the carrier of G1 \/ the carrier of G2 & the carrier' of it = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds

( the Source of it . v = the Source of G1 . v & the Target of it . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds

( the Source of it . v = the Source of G2 . v & the Target of it . v = the Target of G2 . v ) ) );

existence ( the carrier of it = the carrier of G1 \/ the carrier of G2 & the carrier' of it = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds

( the Source of it . v = the Source of G1 . v & the Target of it . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds

( the Source of it . v = the Source of G2 . v & the Target of it . v = the Target of G2 . v ) ) );

ex b

( the carrier of b

( the Source of b

( the Source of b

proof end;

uniqueness for b

( the Source of b

( the Source of b

( the Source of b

( the Source of b

b

proof end;

:: deftheorem Def5 defines \/ GRAPH_1:def 5 :

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds

for b_{3} being strict Graph holds

( b_{3} = G1 \/ G2 iff ( the carrier of b_{3} = the carrier of G1 \/ the carrier of G2 & the carrier' of b_{3} = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds

( the Source of b_{3} . v = the Source of G1 . v & the Target of b_{3} . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds

( the Source of b_{3} . v = the Source of G2 . v & the Target of b_{3} . v = the Target of G2 . v ) ) ) );

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds

for b

( b

( the Source of b

( the Source of b

:: deftheorem Def6 defines is_sum_of GRAPH_1:def 6 :

for G, G1, G2 being Graph holds

( G is_sum_of G1,G2 iff ( the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 ) );

for G, G1, G2 being Graph holds

( G is_sum_of G1,G2 iff ( the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 ) );

definition

let IT be Graph;

end;
attr IT is oriented means :Def7: :: GRAPH_1:def 7

for x, y being set st x in the carrier' of IT & y in the carrier' of IT & the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y holds

x = y;

for x, y being set st x in the carrier' of IT & y in the carrier' of IT & the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y holds

x = y;

attr IT is non-multi means :Def8: :: GRAPH_1:def 8

for x, y being set st x in the carrier' of IT & y in the carrier' of IT & ( ( the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y ) or ( the Source of IT . x = the Target of IT . y & the Source of IT . y = the Target of IT . x ) ) holds

x = y;

for x, y being set st x in the carrier' of IT & y in the carrier' of IT & ( ( the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y ) or ( the Source of IT . x = the Target of IT . y & the Source of IT . y = the Target of IT . x ) ) holds

x = y;

attr IT is simple means :Def9: :: GRAPH_1:def 9

for x being set holds

( not x in the carrier' of IT or not the Source of IT . x = the Target of IT . x );

for x being set holds

( not x in the carrier' of IT or not the Source of IT . x = the Target of IT . x );

:: deftheorem Def7 defines oriented GRAPH_1:def 7 :

for IT being Graph holds

( IT is oriented iff for x, y being set st x in the carrier' of IT & y in the carrier' of IT & the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y holds

x = y );

for IT being Graph holds

( IT is oriented iff for x, y being set st x in the carrier' of IT & y in the carrier' of IT & the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y holds

x = y );

:: deftheorem Def8 defines non-multi GRAPH_1:def 8 :

for IT being Graph holds

( IT is non-multi iff for x, y being set st x in the carrier' of IT & y in the carrier' of IT & ( ( the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y ) or ( the Source of IT . x = the Target of IT . y & the Source of IT . y = the Target of IT . x ) ) holds

x = y );

for IT being Graph holds

( IT is non-multi iff for x, y being set st x in the carrier' of IT & y in the carrier' of IT & ( ( the Source of IT . x = the Source of IT . y & the Target of IT . x = the Target of IT . y ) or ( the Source of IT . x = the Target of IT . y & the Source of IT . y = the Target of IT . x ) ) holds

x = y );

:: deftheorem Def9 defines simple GRAPH_1:def 9 :

for IT being Graph holds

( IT is simple iff for x being set holds

( not x in the carrier' of IT or not the Source of IT . x = the Target of IT . x ) );

for IT being Graph holds

( IT is simple iff for x being set holds

( not x in the carrier' of IT or not the Source of IT . x = the Target of IT . x ) );

:: deftheorem Def10 defines connected GRAPH_1:def 10 :

for IT being Graph holds

( IT is connected iff for G1, G2 being Graph holds

( not the carrier of G1 misses the carrier of G2 or not IT is_sum_of G1,G2 ) );

for IT being Graph holds

( IT is connected iff for G1, G2 being Graph holds

( not the carrier of G1 misses the carrier of G2 or not IT is_sum_of G1,G2 ) );

:: deftheorem Def11 defines finite GRAPH_1:def 11 :

for IT being MultiGraphStruct holds

( IT is finite iff ( the carrier of IT is finite & the carrier' of IT is finite ) );

for IT being MultiGraphStruct holds

( IT is finite iff ( the carrier of IT is finite & the carrier' of IT is finite ) );

registration

existence

ex b_{1} being MultiGraphStruct st b_{1} is finite

ex b_{1} being Graph st

( b_{1} is finite & b_{1} is non-multi & b_{1} is oriented & b_{1} is simple & b_{1} is connected )

end;
ex b

proof end;

existence ex b

( b

proof end;

registration

let G be finite MultiGraphStruct ;

coherence

the carrier of G is finite by Def11;

coherence

the carrier' of G is finite by Def11;

end;
coherence

the carrier of G is finite by Def11;

coherence

the carrier' of G is finite by Def11;

:: deftheorem defines joins GRAPH_1:def 12 :

for G being Graph

for x, y being Element of the carrier of G

for v being set holds

( v joins x,y iff ( ( the Source of G . v = x & the Target of G . v = y ) or ( the Source of G . v = y & the Target of G . v = x ) ) );

for G being Graph

for x, y being Element of the carrier of G

for v being set holds

( v joins x,y iff ( ( the Source of G . v = x & the Target of G . v = y ) or ( the Source of G . v = y & the Target of G . v = x ) ) );

definition

let G be Graph;

let x, y be Element of the carrier of G;

end;
let x, y be Element of the carrier of G;

pred x,y are_incident means :: GRAPH_1:def 13

ex v being set st

( v in the carrier' of G & v joins x,y );

ex v being set st

( v in the carrier' of G & v joins x,y );

:: deftheorem defines are_incident GRAPH_1:def 13 :

for G being Graph

for x, y being Element of the carrier of G holds

( x,y are_incident iff ex v being set st

( v in the carrier' of G & v joins x,y ) );

for G being Graph

for x, y being Element of the carrier of G holds

( x,y are_incident iff ex v being set st

( v in the carrier' of G & v joins x,y ) );

definition

let G be Graph;

ex b_{1} being FinSequence st

( ( for n being Element of NAT st 1 <= n & n <= len b_{1} holds

b_{1} . n in the carrier' of G ) & ex p being FinSequence st

( len p = (len b_{1}) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len b_{1} holds

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & b_{1} . n joins x9,y9 ) ) ) )

end;
mode Chain of G -> FinSequence means :Def14: :: GRAPH_1:def 14

( ( for n being Element of NAT st 1 <= n & n <= len it holds

it . n in the carrier' of G ) & ex p being FinSequence st

( len p = (len it) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len it holds

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & it . n joins x9,y9 ) ) ) );

existence ( ( for n being Element of NAT st 1 <= n & n <= len it holds

it . n in the carrier' of G ) & ex p being FinSequence st

( len p = (len it) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len it holds

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & it . n joins x9,y9 ) ) ) );

ex b

( ( for n being Element of NAT st 1 <= n & n <= len b

b

( len p = (len b

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len b

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & b

proof end;

:: deftheorem Def14 defines Chain GRAPH_1:def 14 :

for G being Graph

for b_{2} being FinSequence holds

( b_{2} is Chain of G iff ( ( for n being Element of NAT st 1 <= n & n <= len b_{2} holds

b_{2} . n in the carrier' of G ) & ex p being FinSequence st

( len p = (len b_{2}) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len b_{2} holds

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & b_{2} . n joins x9,y9 ) ) ) ) );

for G being Graph

for b

( b

b

( len p = (len b

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len b

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & b

Lm1: for G being Graph holds {} is Chain of G

proof end;

definition

let G be Graph;

:: original: Chain

redefine mode Chain of G -> FinSequence of the carrier' of G;

coherence

for b_{1} being Chain of G holds b_{1} is FinSequence of the carrier' of G

end;
:: original: Chain

redefine mode Chain of G -> FinSequence of the carrier' of G;

coherence

for b

proof end;

:: deftheorem defines oriented GRAPH_1:def 15 :

for G being Graph

for IT being Chain of G holds

( IT is oriented iff for n being Element of NAT st 1 <= n & n < len IT holds

the Source of G . (IT . (n + 1)) = the Target of G . (IT . n) );

for G being Graph

for IT being Chain of G holds

( IT is oriented iff for n being Element of NAT st 1 <= n & n < len IT holds

the Source of G . (IT . (n + 1)) = the Target of G . (IT . n) );

registration

let G be Graph;

ex b_{1} being Chain of G st b_{1} is empty

end;
cluster Relation-like NAT -defined the carrier' of G -valued Function-like empty finite FinSequence-like FinSubsequence-like for Chain of G;

existence ex b

proof end;

registration

let G be Graph;

coherence

for b_{1} being Chain of G st b_{1} is empty holds

b_{1} is oriented

end;
coherence

for b

b

proof end;

definition

let G be Graph;

let IT be Chain of G;

( IT is one-to-one iff for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds

IT . n <> IT . m )

end;
let IT be Chain of G;

:: original: one-to-one

redefine attr IT is one-to-one means :: GRAPH_1:def 16

for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds

IT . n <> IT . m;

compatibility redefine attr IT is one-to-one means :: GRAPH_1:def 16

for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds

IT . n <> IT . m;

( IT is one-to-one iff for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds

IT . n <> IT . m )

proof end;

:: deftheorem defines one-to-one GRAPH_1:def 16 :

for G being Graph

for IT being Chain of G holds

( IT is one-to-one iff for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds

IT . n <> IT . m );

for G being Graph

for IT being Chain of G holds

( IT is one-to-one iff for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds

IT . n <> IT . m );

definition

let G be Graph;

let IT be Path of G;

end;
let IT be Path of G;

attr IT is cyclic means :: GRAPH_1:def 17

ex p being FinSequence st

( len p = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len IT holds

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & IT . n joins x9,y9 ) ) & p . 1 = p . (len p) );

ex p being FinSequence st

( len p = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len IT holds

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & IT . n joins x9,y9 ) ) & p . 1 = p . (len p) );

:: deftheorem defines cyclic GRAPH_1:def 17 :

for G being Graph

for IT being Path of G holds

( IT is cyclic iff ex p being FinSequence st

( len p = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len IT holds

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & IT . n joins x9,y9 ) ) & p . 1 = p . (len p) ) );

for G being Graph

for IT being Path of G holds

( IT is cyclic iff ex p being FinSequence st

( len p = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds

p . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len IT holds

ex x9, y9 being Vertex of G st

( x9 = p . n & y9 = p . (n + 1) & IT . n joins x9,y9 ) ) & p . 1 = p . (len p) ) );

registration

let G be Graph;

coherence

for b_{1} being Path of G st b_{1} is empty holds

b_{1} is cyclic

end;
coherence

for b

b

proof end;

definition

let G be Graph;

ex b_{1} being Graph st

( the carrier of b_{1} c= the carrier of G & the carrier' of b_{1} c= the carrier' of G & ( for v being set st v in the carrier' of b_{1} holds

( the Source of b_{1} . v = the Source of G . v & the Target of b_{1} . v = the Target of G . v & the Source of G . v in the carrier of b_{1} & the Target of G . v in the carrier of b_{1} ) ) )

end;
mode Subgraph of G -> Graph means :Def18: :: GRAPH_1:def 18

( the carrier of it c= the carrier of G & the carrier' of it c= the carrier' of G & ( for v being set st v in the carrier' of it holds

( the Source of it . v = the Source of G . v & the Target of it . v = the Target of G . v & the Source of G . v in the carrier of it & the Target of G . v in the carrier of it ) ) );

existence ( the carrier of it c= the carrier of G & the carrier' of it c= the carrier' of G & ( for v being set st v in the carrier' of it holds

( the Source of it . v = the Source of G . v & the Target of it . v = the Target of G . v & the Source of G . v in the carrier of it & the Target of G . v in the carrier of it ) ) );

ex b

( the carrier of b

( the Source of b

proof end;

:: deftheorem Def18 defines Subgraph GRAPH_1:def 18 :

for G, b_{2} being Graph holds

( b_{2} is Subgraph of G iff ( the carrier of b_{2} c= the carrier of G & the carrier' of b_{2} c= the carrier' of G & ( for v being set st v in the carrier' of b_{2} holds

( the Source of b_{2} . v = the Source of G . v & the Target of b_{2} . v = the Target of G . v & the Source of G . v in the carrier of b_{2} & the Target of G . v in the carrier of b_{2} ) ) ) );

for G, b

( b

( the Source of b

registration
end;

definition

let G be finite Graph;

ex b_{1} being Element of NAT ex B being finite set st

( B = the carrier of G & b_{1} = card B )

for b_{1}, b_{2} being Element of NAT st ex B being finite set st

( B = the carrier of G & b_{1} = card B ) & ex B being finite set st

( B = the carrier of G & b_{2} = card B ) holds

b_{1} = b_{2}
;

ex b_{1} being Element of NAT ex B being finite set st

( B = the carrier' of G & b_{1} = card B )

for b_{1}, b_{2} being Element of NAT st ex B being finite set st

( B = the carrier' of G & b_{1} = card B ) & ex B being finite set st

( B = the carrier' of G & b_{2} = card B ) holds

b_{1} = b_{2}
;

end;
func VerticesCount G -> Element of NAT means :: GRAPH_1:def 19

ex B being finite set st

( B = the carrier of G & it = card B );

existence ex B being finite set st

( B = the carrier of G & it = card B );

ex b

( B = the carrier of G & b

proof end;

uniqueness for b

( B = the carrier of G & b

( B = the carrier of G & b

b

func EdgesCount G -> Element of NAT means :: GRAPH_1:def 20

ex B being finite set st

( B = the carrier' of G & it = card B );

existence ex B being finite set st

( B = the carrier' of G & it = card B );

ex b

( B = the carrier' of G & b

proof end;

uniqueness for b

( B = the carrier' of G & b

( B = the carrier' of G & b

b

:: deftheorem defines VerticesCount GRAPH_1:def 19 :

for G being finite Graph

for b_{2} being Element of NAT holds

( b_{2} = VerticesCount G iff ex B being finite set st

( B = the carrier of G & b_{2} = card B ) );

for G being finite Graph

for b

( b

( B = the carrier of G & b

:: deftheorem defines EdgesCount GRAPH_1:def 20 :

for G being finite Graph

for b_{2} being Element of NAT holds

( b_{2} = EdgesCount G iff ex B being finite set st

( B = the carrier' of G & b_{2} = card B ) );

for G being finite Graph

for b

( b

( B = the carrier' of G & b

definition

let G be finite Graph;

let x be Vertex of G;

ex b_{1} being Element of NAT ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b_{1} = card X )

for b_{1}, b_{2} being Element of NAT st ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b_{1} = card X ) & ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b_{2} = card X ) holds

b_{1} = b_{2}

ex b_{1} being Element of NAT ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b_{1} = card X )

for b_{1}, b_{2} being Element of NAT st ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b_{1} = card X ) & ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b_{2} = card X ) holds

b_{1} = b_{2}

end;
let x be Vertex of G;

func EdgesIn x -> Element of NAT means :: GRAPH_1:def 21

ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & it = card X );

existence ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & it = card X );

ex b

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b

proof end;

uniqueness for b

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b

b

proof end;

func EdgesOut x -> Element of NAT means :: GRAPH_1:def 22

ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & it = card X );

existence ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & it = card X );

ex b

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b

proof end;

uniqueness for b

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b

b

proof end;

:: deftheorem defines EdgesIn GRAPH_1:def 21 :

for G being finite Graph

for x being Vertex of G

for b_{3} being Element of NAT holds

( b_{3} = EdgesIn x iff ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b_{3} = card X ) );

for G being finite Graph

for x being Vertex of G

for b

( b

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & b

:: deftheorem defines EdgesOut GRAPH_1:def 22 :

for G being finite Graph

for x being Vertex of G

for b_{3} being Element of NAT holds

( b_{3} = EdgesOut x iff ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b_{3} = card X ) );

for G being finite Graph

for x being Vertex of G

for b

( b

( ( for z being set holds

( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & b

definition

let G be finite Graph;

let x be Vertex of G;

correctness

coherence

(EdgesIn x) + (EdgesOut x) is Element of NAT ;

;

end;
let x be Vertex of G;

correctness

coherence

(EdgesIn x) + (EdgesOut x) is Element of NAT ;

;

:: deftheorem defines Degree GRAPH_1:def 23 :

for G being finite Graph

for x being Vertex of G holds Degree x = (EdgesIn x) + (EdgesOut x);

for G being finite Graph

for x being Vertex of G holds Degree x = (EdgesIn x) + (EdgesOut x);

Lm2: for n being Element of NAT

for G being Graph

for p being Chain of G holds p | (Seg n) is Chain of G

proof end;

Lm3: for G being Graph

for H1, H2 being strict Subgraph of G st the carrier of H1 = the carrier of H2 & the carrier' of H1 = the carrier' of H2 holds

H1 = H2

proof end;

definition
end;

:: deftheorem Def24 defines c= GRAPH_1:def 24 :

for G1, G2 being Graph holds

( G1 c= G2 iff G1 is Subgraph of G2 );

for G1, G2 being Graph holds

( G1 c= G2 iff G1 is Subgraph of G2 );

Lm4: for G being Graph

for H being Subgraph of G holds

( the Source of H in PFuncs ( the carrier' of G, the carrier of G) & the Target of H in PFuncs ( the carrier' of G, the carrier of G) )

proof end;

definition

let G be Graph;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is strict Subgraph of G )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is strict Subgraph of G ) ) & ( for x being set holds

( x in b_{2} iff x is strict Subgraph of G ) ) holds

b_{1} = b_{2}

end;
func bool G -> set means :Def25: :: GRAPH_1:def 25

for x being set holds

( x in it iff x is strict Subgraph of G );

existence for x being set holds

( x in it iff x is strict Subgraph of G );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def25 defines bool GRAPH_1:def 25 :

for G being Graph

for b_{2} being set holds

( b_{2} = bool G iff for x being set holds

( x in b_{2} iff x is strict Subgraph of G ) );

for G being Graph

for b

( b

( x in b

:: Properties of graphs ::

theorem :: GRAPH_1:1

theorem :: GRAPH_1:3

:: Chain ::

theorem :: GRAPH_1:4

:: Sum of two graphs ::

theorem Th5: :: GRAPH_1:5

for G1, G being Graph st G1 c= G holds

( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G )

( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G )

proof end;

theorem :: GRAPH_1:6

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds

( the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2 & the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2 )

( the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2 & the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2 )

proof end;

theorem Th8: :: GRAPH_1:8

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds

G1 \/ G2 = G2 \/ G1

G1 \/ G2 = G2 \/ G1

proof end;

theorem Th9: :: GRAPH_1:9

for G1, G2, G3 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G3 & the Target of G1 tolerates the Target of G3 & the Source of G2 tolerates the Source of G3 & the Target of G2 tolerates the Target of G3 holds

(G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)

(G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)

proof end;

:: Graphs' inclusion ::

theorem :: GRAPH_1:13

for G1, G2, G3 being Graph st ex G being Graph st

( G1 c= G & G2 c= G & G3 c= G ) holds

(G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)

( G1 c= G & G2 c= G & G3 c= G ) holds

(G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)

proof end;

theorem :: GRAPH_1:15

theorem Th19: :: GRAPH_1:19

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds

( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )

( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )

proof end;

theorem Th20: :: GRAPH_1:20

for G1, G2 being Graph st ex G being Graph st

( G1 c= G & G2 c= G ) holds

( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )

( G1 c= G & G2 c= G ) holds

( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )

proof end;

theorem Th24: :: GRAPH_1:24

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & ( G1 \/ G2 = G2 or G2 \/ G1 = G2 ) holds

G1 c= G2

G1 c= G2

proof end;

:: Set of all subgraphs ::

theorem :: GRAPH_1:32

for G1, G2 being strict Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 & bool (G1 \/ G2) c= (bool G1) \/ (bool G2) & not G1 c= G2 holds

G2 c= G1

G2 c= G1

proof end;

theorem :: GRAPH_1:33

for G1, G2 being Graph st the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 holds

(bool G1) \/ (bool G2) c= bool (G1 \/ G2)

(bool G1) \/ (bool G2) c= bool (G1 \/ G2)

proof end;