:: GRAPH_1 semantic presentation
begin
definition
attrc1 is strict ;
struct MultiGraphStruct -> 2-sorted ;
aggrMultiGraphStruct(# carrier, carrier', Source, Target #) -> MultiGraphStruct ;
sel Source c1 -> Function of the carrier' of c1, the carrier of c1;
sel Target c1 -> Function of the carrier' of c1, the carrier of c1;
end;
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;
registration
cluster non empty non void strict for MultiGraphStruct ;
existence
ex b1 being MultiGraphStruct st
( b1 is strict & not b1 is empty & not b1 is void )
proof
( not MultiGraphStruct(# 1,1,op1,op1 #) is empty & not MultiGraphStruct(# 1,1,op1,op1 #) is void ) ;
hence ex b1 being MultiGraphStruct st
( b1 is strict & not b1 is empty & not b1 is void ) ; ::_thesis: verum
end;
end;
definition
mode Graph is non empty MultiGraphStruct ;
end;
definition
let C be MultiGraphStruct ;
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
( ( 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
thus ( not C is void & not C is empty implies the Source of C . f is Vertex of C ) ::_thesis: ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C )
proof
assume ( not C is void & not C is empty ) ; ::_thesis: the Source of C . f is Vertex of C
then reconsider C = C as non empty non void MultiGraphStruct ;
reconsider f = f as Edge of C ;
the Source of C . f is Vertex of C ;
hence the Source of C . f is Vertex of C ; ::_thesis: verum
end;
thus ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) ; ::_thesis: verum
end;
consistency
for b1 being Vertex of C holds verum ;
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
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 b1 being Vertex of C holds verum;
proof
thus ( not C is void & not C is empty implies the Target of C . f is Vertex of C ) ::_thesis: ( ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) & ( for b1 being Vertex of C holds verum ) )
proof
assume ( not C is void & not C is empty ) ; ::_thesis: the Target of C . f is Vertex of C
then reconsider C = C as non empty non void MultiGraphStruct ;
reconsider f = f as Edge of C ;
the Target of C . f is Vertex of C ;
hence the Target of C . f is Vertex of C ; ::_thesis: verum
end;
thus ( ( ( C is void or C is empty ) implies the Vertex of C is Vertex of C ) & ( for b1 being Vertex of C holds verum ) ) ; ::_thesis: verum
end;
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 ) );
:: 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 ) );
definition
let C be non empty non void MultiGraphStruct ;
let f be Edge of C;
:: original: dom
redefine func dom f -> Vertex of C equals :: GRAPH_1:def 3
the Source of C . f;
compatibility
for b1 being Vertex of C holds
( b1 = dom f iff b1 = the Source of C . f ) by Def1;
coherence
dom f is Vertex of C ;
:: original: cod
redefine func cod f -> Vertex of C equals :: GRAPH_1:def 4
the Target of C . f;
compatibility
for b1 being Vertex of C holds
( b1 = cod f iff b1 = the Target of C . f ) by Def2;
coherence
cod f is Vertex of C ;
end;
:: 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;
:: 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;
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 ;
funcG1 \/ 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
ex b1 being strict Graph st
( the carrier of b1 = the carrier of G1 \/ the carrier of G2 & the carrier' of b1 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of b1 . v = the Source of G1 . v & the Target of b1 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of b1 . v = the Source of G2 . v & the Target of b1 . v = the Target of G2 . v ) ) )
proof
set V = the carrier of G1 \/ the carrier of G2;
set E = the carrier' of G1 \/ the carrier' of G2;
ex S being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) st
( ( for v being set st v in the carrier' of G1 holds
S . v = the Source of G1 . v ) & ( for v being set st v in the carrier' of G2 holds
S . v = the Source of G2 . v ) )
proof
defpred S1[ set , set ] means ( ( $1 in the carrier' of G1 implies $2 = the Source of G1 . $1 ) & ( $1 in the carrier' of G2 implies $2 = the Source of G2 . $1 ) );
A3: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds
ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier' of G1 \/ the carrier' of G2 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
assume A4: x in the carrier' of G1 \/ the carrier' of G2 ; ::_thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
A5: ( x in the carrier' of G1 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
proof
assume A6: x in the carrier' of G1 ; ::_thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
take y = the Source of G1 . x; ::_thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
y in the carrier of G1 by A6, FUNCT_2:5;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def_3; ::_thesis: S1[x,y]
thus ( x in the carrier' of G1 implies y = the Source of G1 . x ) ; ::_thesis: ( x in the carrier' of G2 implies y = the Source of G2 . x )
assume x in the carrier' of G2 ; ::_thesis: y = the Source of G2 . x
then A7: x in the carrier' of G1 /\ the carrier' of G2 by A6, XBOOLE_0:def_4;
dom the Source of G1 = the carrier' of G1 by FUNCT_2:def_1;
then x in (dom the Source of G1) /\ (dom the Source of G2) by A7, FUNCT_2:def_1;
hence y = the Source of G2 . x by A1, PARTFUN1:def_4; ::_thesis: verum
end;
( not x in the carrier' of G1 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
proof
assume A8: not x in the carrier' of G1 ; ::_thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
then A9: x in the carrier' of G2 by A4, XBOOLE_0:def_3;
take y = the Source of G2 . x; ::_thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
y in the carrier of G2 by A9, FUNCT_2:5;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def_3; ::_thesis: S1[x,y]
thus S1[x,y] by A8; ::_thesis: verum
end;
hence ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) by A5; ::_thesis: verum
end;
consider S being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) such that
A10: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds
S1[x,S . x] from FUNCT_2:sch_1(A3);
take S ; ::_thesis: ( ( for v being set st v in the carrier' of G1 holds
S . v = the Source of G1 . v ) & ( for v being set st v in the carrier' of G2 holds
S . v = the Source of G2 . v ) )
thus for v being set st v in the carrier' of G1 holds
S . v = the Source of G1 . v ::_thesis: for v being set st v in the carrier' of G2 holds
S . v = the Source of G2 . v
proof
let v be set ; ::_thesis: ( v in the carrier' of G1 implies S . v = the Source of G1 . v )
assume A11: v in the carrier' of G1 ; ::_thesis: S . v = the Source of G1 . v
then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def_3;
hence S . v = the Source of G1 . v by A10, A11; ::_thesis: verum
end;
let v be set ; ::_thesis: ( v in the carrier' of G2 implies S . v = the Source of G2 . v )
assume A12: v in the carrier' of G2 ; ::_thesis: S . v = the Source of G2 . v
then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def_3;
hence S . v = the Source of G2 . v by A10, A12; ::_thesis: verum
end;
then consider S being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) such that
A13: for v being set st v in the carrier' of G1 holds
S . v = the Source of G1 . v and
A14: for v being set st v in the carrier' of G2 holds
S . v = the Source of G2 . v ;
ex T being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) st
( ( for v being set st v in the carrier' of G1 holds
T . v = the Target of G1 . v ) & ( for v being set st v in the carrier' of G2 holds
T . v = the Target of G2 . v ) )
proof
defpred S1[ set , set ] means ( ( $1 in the carrier' of G1 implies $2 = the Target of G1 . $1 ) & ( $1 in the carrier' of G2 implies $2 = the Target of G2 . $1 ) );
A15: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds
ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier' of G1 \/ the carrier' of G2 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
assume A16: x in the carrier' of G1 \/ the carrier' of G2 ; ::_thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
A17: ( x in the carrier' of G1 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
proof
assume A18: x in the carrier' of G1 ; ::_thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
take y = the Target of G1 . x; ::_thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
y in the carrier of G1 by A18, FUNCT_2:5;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def_3; ::_thesis: S1[x,y]
thus ( x in the carrier' of G1 implies y = the Target of G1 . x ) ; ::_thesis: ( x in the carrier' of G2 implies y = the Target of G2 . x )
assume x in the carrier' of G2 ; ::_thesis: y = the Target of G2 . x
then A19: x in the carrier' of G1 /\ the carrier' of G2 by A18, XBOOLE_0:def_4;
dom the Target of G1 = the carrier' of G1 by FUNCT_2:def_1;
then x in (dom the Target of G1) /\ (dom the Target of G2) by A19, FUNCT_2:def_1;
hence y = the Target of G2 . x by A2, PARTFUN1:def_4; ::_thesis: verum
end;
( not x in the carrier' of G1 implies ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) )
proof
assume A20: not x in the carrier' of G1 ; ::_thesis: ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
then A21: x in the carrier' of G2 by A16, XBOOLE_0:def_3;
take y = the Target of G2 . x; ::_thesis: ( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] )
y in the carrier of G2 by A21, FUNCT_2:5;
hence y in the carrier of G1 \/ the carrier of G2 by XBOOLE_0:def_3; ::_thesis: S1[x,y]
thus S1[x,y] by A20; ::_thesis: verum
end;
hence ex y being set st
( y in the carrier of G1 \/ the carrier of G2 & S1[x,y] ) by A17; ::_thesis: verum
end;
consider S being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) such that
A22: for x being set st x in the carrier' of G1 \/ the carrier' of G2 holds
S1[x,S . x] from FUNCT_2:sch_1(A15);
take S ; ::_thesis: ( ( for v being set st v in the carrier' of G1 holds
S . v = the Target of G1 . v ) & ( for v being set st v in the carrier' of G2 holds
S . v = the Target of G2 . v ) )
thus for v being set st v in the carrier' of G1 holds
S . v = the Target of G1 . v ::_thesis: for v being set st v in the carrier' of G2 holds
S . v = the Target of G2 . v
proof
let v be set ; ::_thesis: ( v in the carrier' of G1 implies S . v = the Target of G1 . v )
assume A23: v in the carrier' of G1 ; ::_thesis: S . v = the Target of G1 . v
then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def_3;
hence S . v = the Target of G1 . v by A22, A23; ::_thesis: verum
end;
let v be set ; ::_thesis: ( v in the carrier' of G2 implies S . v = the Target of G2 . v )
assume A24: v in the carrier' of G2 ; ::_thesis: S . v = the Target of G2 . v
then v in the carrier' of G1 \/ the carrier' of G2 by XBOOLE_0:def_3;
hence S . v = the Target of G2 . v by A22, A24; ::_thesis: verum
end;
then consider T being Function of ( the carrier' of G1 \/ the carrier' of G2),( the carrier of G1 \/ the carrier of G2) such that
A25: for v being set st v in the carrier' of G1 holds
T . v = the Target of G1 . v and
A26: for v being set st v in the carrier' of G2 holds
T . v = the Target of G2 . v ;
reconsider G = MultiGraphStruct(# ( the carrier of G1 \/ the carrier of G2),( the carrier' of G1 \/ the carrier' of G2),S,T #) as strict Graph ;
take G ; ::_thesis: ( the carrier of G = the carrier of G1 \/ the carrier of G2 & the carrier' of G = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) )
thus the carrier of G = the carrier of G1 \/ the carrier of G2 ; ::_thesis: ( the carrier' of G = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) )
thus the carrier' of G = the carrier' of G1 \/ the carrier' of G2 ; ::_thesis: ( ( for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) )
thus for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) by A13, A25; ::_thesis: for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v )
let v be set ; ::_thesis: ( v in the carrier' of G2 implies ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) )
assume A27: v in the carrier' of G2 ; ::_thesis: ( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v )
hence the Source of G . v = the Source of G2 . v by A14; ::_thesis: the Target of G . v = the Target of G2 . v
thus the Target of G . v = the Target of G2 . v by A26, A27; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Graph st the carrier of b1 = the carrier of G1 \/ the carrier of G2 & the carrier' of b1 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of b1 . v = the Source of G1 . v & the Target of b1 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of b1 . v = the Source of G2 . v & the Target of b1 . v = the Target of G2 . v ) ) & the carrier of b2 = the carrier of G1 \/ the carrier of G2 & the carrier' of b2 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of b2 . v = the Source of G1 . v & the Target of b2 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of b2 . v = the Source of G2 . v & the Target of b2 . v = the Target of G2 . v ) ) holds
b1 = b2
proof
let G, G9 be strict Graph; ::_thesis: ( the carrier of G = the carrier of G1 \/ the carrier of G2 & the carrier' of G = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) ) & the carrier of G9 = the carrier of G1 \/ the carrier of G2 & the carrier' of G9 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of G9 . v = the Source of G1 . v & the Target of G9 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of G9 . v = the Source of G2 . v & the Target of G9 . v = the Target of G2 . v ) ) implies G = G9 )
assume that
A28: the carrier of G = the carrier of G1 \/ the carrier of G2 and
A29: the carrier' of G = the carrier' of G1 \/ the carrier' of G2 and
A30: for v being set st v in the carrier' of G1 holds
( the Source of G . v = the Source of G1 . v & the Target of G . v = the Target of G1 . v ) and
A31: for v being set st v in the carrier' of G2 holds
( the Source of G . v = the Source of G2 . v & the Target of G . v = the Target of G2 . v ) and
A32: the carrier of G9 = the carrier of G1 \/ the carrier of G2 and
A33: the carrier' of G9 = the carrier' of G1 \/ the carrier' of G2 and
A34: for v being set st v in the carrier' of G1 holds
( the Source of G9 . v = the Source of G1 . v & the Target of G9 . v = the Target of G1 . v ) and
A35: for v being set st v in the carrier' of G2 holds
( the Source of G9 . v = the Source of G2 . v & the Target of G9 . v = the Target of G2 . v ) ; ::_thesis: G = G9
A36: ( dom the Source of G = the carrier' of G & dom the Source of G9 = the carrier' of G ) by A29, A33, FUNCT_2:def_1;
A37: ( dom the Target of G = the carrier' of G & dom the Target of G9 = the carrier' of G ) by A29, A33, FUNCT_2:def_1;
for x being set st x in the carrier' of G holds
the Source of G . x = the Source of G9 . x
proof
let x be set ; ::_thesis: ( x in the carrier' of G implies the Source of G . x = the Source of G9 . x )
assume A38: x in the carrier' of G ; ::_thesis: the Source of G . x = the Source of G9 . x
A39: now__::_thesis:_(_x_in_the_carrier'_of_G1_implies_the_Source_of_G_._x_=_the_Source_of_G9_._x_)
assume A40: x in the carrier' of G1 ; ::_thesis: the Source of G . x = the Source of G9 . x
hence the Source of G . x = the Source of G1 . x by A30
.= the Source of G9 . x by A34, A40 ;
::_thesis: verum
end;
now__::_thesis:_(_x_in_the_carrier'_of_G2_implies_the_Source_of_G_._x_=_the_Source_of_G9_._x_)
assume A41: x in the carrier' of G2 ; ::_thesis: the Source of G . x = the Source of G9 . x
hence the Source of G . x = the Source of G2 . x by A31
.= the Source of G9 . x by A35, A41 ;
::_thesis: verum
end;
hence the Source of G . x = the Source of G9 . x by A29, A38, A39, XBOOLE_0:def_3; ::_thesis: verum
end;
then A42: the Source of G = the Source of G9 by A36, FUNCT_1:2;
for x being set st x in the carrier' of G holds
the Target of G . x = the Target of G9 . x
proof
let x be set ; ::_thesis: ( x in the carrier' of G implies the Target of G . x = the Target of G9 . x )
assume A43: x in the carrier' of G ; ::_thesis: the Target of G . x = the Target of G9 . x
A44: now__::_thesis:_(_x_in_the_carrier'_of_G1_implies_the_Target_of_G_._x_=_the_Target_of_G9_._x_)
assume A45: x in the carrier' of G1 ; ::_thesis: the Target of G . x = the Target of G9 . x
hence the Target of G . x = the Target of G1 . x by A30
.= the Target of G9 . x by A34, A45 ;
::_thesis: verum
end;
now__::_thesis:_(_x_in_the_carrier'_of_G2_implies_the_Target_of_G_._x_=_the_Target_of_G9_._x_)
assume A46: x in the carrier' of G2 ; ::_thesis: the Target of G . x = the Target of G9 . x
hence the Target of G . x = the Target of G2 . x by A31
.= the Target of G9 . x by A35, A46 ;
::_thesis: verum
end;
hence the Target of G . x = the Target of G9 . x by A29, A43, A44, XBOOLE_0:def_3; ::_thesis: verum
end;
hence G = G9 by A28, A29, A32, A33, A37, A42, FUNCT_1:2; ::_thesis: verum
end;
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 b3 being strict Graph holds
( b3 = G1 \/ G2 iff ( the carrier of b3 = the carrier of G1 \/ the carrier of G2 & the carrier' of b3 = the carrier' of G1 \/ the carrier' of G2 & ( for v being set st v in the carrier' of G1 holds
( the Source of b3 . v = the Source of G1 . v & the Target of b3 . v = the Target of G1 . v ) ) & ( for v being set st v in the carrier' of G2 holds
( the Source of b3 . v = the Source of G2 . v & the Target of b3 . v = the Target of G2 . v ) ) ) );
definition
let G, G1, G2 be Graph;
predG is_sum_of G1,G2 means :Def6: :: GRAPH_1:def 6
( 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 );
end;
:: 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 ) );
definition
let IT be Graph;
attrIT 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;
attrIT 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;
attrIT 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 );
attrIT is connected means :Def10: :: GRAPH_1:def 10
for G1, G2 being Graph holds
( not the carrier of G1 misses the carrier of G2 or not IT is_sum_of G1,G2 );
end;
:: 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 );
:: 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 );
:: 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 ) );
:: 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 ) );
definition
let IT be MultiGraphStruct ;
attrIT is finite means :Def11: :: GRAPH_1:def 11
( the carrier of IT is finite & the carrier' of IT is finite );
end;
:: 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 ) );
registration
cluster finite for MultiGraphStruct ;
existence
ex b1 being MultiGraphStruct st b1 is finite
proof
take G = MultiGraphStruct(# 1,1,op1,op1 #); ::_thesis: G is finite
thus the carrier of G is finite ; :: according to GRAPH_1:def_11 ::_thesis: the carrier' of G is finite
thus the carrier' of G is finite ; ::_thesis: verum
end;
cluster non empty feasible oriented non-multi simple connected finite for MultiGraphStruct ;
existence
ex b1 being Graph st
( b1 is finite & b1 is non-multi & b1 is oriented & b1 is simple & b1 is connected )
proof
set V = {1};
reconsider empty1 = {} as Function of {},{1} by RELSET_1:12;
reconsider G = MultiGraphStruct(# {1},{},empty1,empty1 #) as Graph ;
take G ; ::_thesis: ( G is finite & G is non-multi & G is oriented & G is simple & G is connected )
thus G is finite by Def11; ::_thesis: ( G is non-multi & G is oriented & G is simple & G is connected )
for x, y being set st x in the carrier' of G & y in the carrier' of G & ( ( the Source of G . x = the Source of G . y & the Target of G . x = the Target of G . y ) or ( the Source of G . x = the Target of G . y & the Source of G . y = the Target of G . x ) ) holds
x = y ;
hence G is non-multi by Def8; ::_thesis: ( G is oriented & G is simple & G is connected )
for x, y being set st x in the carrier' of G & y in the carrier' of G & the Source of G . x = the Source of G . y & the Target of G . x = the Target of G . y holds
x = y ;
hence G is oriented by Def7; ::_thesis: ( G is simple & G is connected )
for x being set holds
( not x in the carrier' of G or not the Source of G . x = the Target of G . x ) ;
hence G is simple by Def9; ::_thesis: G is connected
for G1, G2 being Graph holds
( not the carrier of G1 misses the carrier of G2 or not G is_sum_of G1,G2 )
proof
given G1, G2 being Graph such that A1: the carrier of G1 misses the carrier of G2 and
A2: G is_sum_of G1,G2 ; ::_thesis: contradiction
A3: the carrier of G1 /\ the carrier of G2 = {} by A1, XBOOLE_0:def_7;
A4: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) by A2, Def6;
G = G1 \/ G2 by A2, Def6;
then A5: the carrier of G1 \/ the carrier of G2 = {1} by A4, Def5;
set x = the Vertex of G1;
( the Vertex of G1 in the carrier of G1 & the Vertex of G1 in {1} ) by A5, XBOOLE_0:def_3;
then A6: 1 in the carrier of G1 by TARSKI:def_1;
set y = the Vertex of G2;
( the Vertex of G2 in the carrier of G2 & the Vertex of G2 in {1} ) by A5, XBOOLE_0:def_3;
then 1 in the carrier of G2 by TARSKI:def_1;
hence contradiction by A3, A6, XBOOLE_0:def_4; ::_thesis: verum
end;
hence G is connected by Def10; ::_thesis: verum
end;
end;
registration
let G be finite MultiGraphStruct ;
cluster the carrier of G -> finite ;
coherence
the carrier of G is finite by Def11;
cluster the carrier' of G -> finite ;
coherence
the carrier' of G is finite by Def11;
end;
definition
let G be Graph;
let x, y be Element of the carrier of G;
let v be set ;
predv joins x,y means :: GRAPH_1:def 12
( ( 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 ) );
end;
:: 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 ) ) );
definition
let G be Graph;
let x, y be Element of the carrier of G;
predx,y are_incident means :: GRAPH_1:def 13
ex v being set st
( v in the carrier' of G & v joins x,y );
end;
:: 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 ) );
definition
let G be Graph;
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
ex b1 being FinSequence st
( ( for n being Element of NAT st 1 <= n & n <= len b1 holds
b1 . n in the carrier' of G ) & ex p being FinSequence st
( len p = (len b1) + 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 b1 holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & b1 . n joins x9,y9 ) ) ) )
proof
take {} ; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n in the carrier' of G ) & ex p being FinSequence st
( len p = (len {}) + 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 {} holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & {} . n joins x9,y9 ) ) ) )
thus for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n in the carrier' of G by XXREAL_0:2; ::_thesis: ex p being FinSequence st
( len p = (len {}) + 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 {} holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & {} . n joins x9,y9 ) ) )
set x = the Vertex of G;
A1: the Vertex of G in the carrier of G ;
take <* the Vertex of G*> ; ::_thesis: ( len <* the Vertex of G*> = (len {}) + 1 & ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) )
thus len <* the Vertex of G*> = (len {}) + 1 by FINSEQ_1:39; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) )
thus for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ::_thesis: for n being Element of NAT st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 )
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <* the Vertex of G*> implies <* the Vertex of G*> . n in the carrier of G )
assume that
A2: 1 <= n and
A3: n <= len <* the Vertex of G*> ; ::_thesis: <* the Vertex of G*> . n in the carrier of G
n <= 1 by A3, FINSEQ_1:39;
then n = 1 by A2, XXREAL_0:1;
hence <* the Vertex of G*> . n in the carrier of G by A1, FINSEQ_1:40; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) )
thus ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) by XXREAL_0:2; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines Chain GRAPH_1:def_14_:_
for G being Graph
for b2 being FinSequence holds
( b2 is Chain of G iff ( ( for n being Element of NAT st 1 <= n & n <= len b2 holds
b2 . n in the carrier' of G ) & ex p being FinSequence st
( len p = (len b2) + 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 b2 holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & b2 . n joins x9,y9 ) ) ) ) );
Lm1: for G being Graph holds {} is Chain of G
proof
let G be Graph; ::_thesis: {} is Chain of G
thus for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n in the carrier' of G by XXREAL_0:2; :: according to GRAPH_1:def_14 ::_thesis: ex p being FinSequence st
( len p = (len {}) + 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 {} holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & {} . n joins x9,y9 ) ) )
set x = the Vertex of G;
A1: the Vertex of G in the carrier of G ;
take <* the Vertex of G*> ; ::_thesis: ( len <* the Vertex of G*> = (len {}) + 1 & ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) )
thus len <* the Vertex of G*> = (len {}) + 1 by FINSEQ_1:39; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) )
thus for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ::_thesis: for n being Element of NAT st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 )
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <* the Vertex of G*> implies <* the Vertex of G*> . n in the carrier of G )
assume that
A2: 1 <= n and
A3: n <= len <* the Vertex of G*> ; ::_thesis: <* the Vertex of G*> . n in the carrier of G
n <= 1 by A3, FINSEQ_1:39;
then n = 1 by A2, XXREAL_0:1;
hence <* the Vertex of G*> . n in the carrier of G by A1, FINSEQ_1:40; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) )
thus ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) by XXREAL_0:2; ::_thesis: verum
end;
definition
let G be Graph;
:: original: Chain
redefine mode Chain of G -> FinSequence of the carrier' of G;
coherence
for b1 being Chain of G holds b1 is FinSequence of the carrier' of G
proof
let c be Chain of G; ::_thesis: c is FinSequence of the carrier' of G
rng c c= the carrier' of G
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in the carrier' of G )
assume y in rng c ; ::_thesis: y in the carrier' of G
then consider x being set such that
A1: x in dom c and
A2: y = c . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A1;
( 1 <= x & x <= len c ) by A1, FINSEQ_3:25;
hence y in the carrier' of G by A2, Def14; ::_thesis: verum
end;
hence c is FinSequence of the carrier' of G by FINSEQ_1:def_4; ::_thesis: verum
end;
end;
definition
let G be Graph;
let IT be Chain of G;
attrIT is oriented means :: GRAPH_1:def 15
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);
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) );
registration
let G be Graph;
cluster Relation-like NAT -defined the carrier' of G -valued Function-like empty finite FinSequence-like FinSubsequence-like for Chain of G;
existence
ex b1 being Chain of G st b1 is empty
proof
{} is Chain of G by Lm1;
hence ex b1 being Chain of G st b1 is empty ; ::_thesis: verum
end;
end;
registration
let G be Graph;
cluster empty -> oriented for Chain of G;
coherence
for b1 being Chain of G st b1 is empty holds
b1 is oriented
proof
let C be Chain of G; ::_thesis: ( C is empty implies C is oriented )
assume A1: C is empty ; ::_thesis: C is oriented
let n be Element of NAT ; :: according to GRAPH_1:def_15 ::_thesis: ( 1 <= n & n < len C implies the Source of G . (C . (n + 1)) = the Target of G . (C . n) )
thus ( 1 <= n & n < len C implies the Source of G . (C . (n + 1)) = the Target of G . (C . n) ) by A1, CARD_1:27, XXREAL_0:2; ::_thesis: verum
end;
end;
definition
let G be Graph;
let IT be Chain of G;
:: original: one-to-one
redefine attrIT 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
( 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
thus ( IT is one-to-one implies for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m ) ::_thesis: ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m ) implies IT is one-to-one )
proof
assume A1: IT is one-to-one ; ::_thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m
let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len IT implies IT . n <> IT . m )
assume that
A2: 1 <= n and
A3: n < m and
A4: m <= len IT ; ::_thesis: IT . n <> IT . m
A5: n <= len IT by A3, A4, XXREAL_0:2;
A6: 1 <= m by A2, A3, XXREAL_0:2;
A7: n in dom IT by A2, A5, FINSEQ_3:25;
m in dom IT by A4, A6, FINSEQ_3:25;
hence IT . n <> IT . m by A1, A3, A7, FUNCT_1:def_4; ::_thesis: verum
end;
assume A8: for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m ; ::_thesis: IT is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom IT or not x2 in dom IT or not IT . x1 = IT . x2 or x1 = x2 )
assume that
A9: ( x1 in dom IT & x2 in dom IT ) and
A10: IT . x1 = IT . x2 ; ::_thesis: x1 = x2
reconsider x9 = x1, y9 = x2 as Element of NAT by A9;
A11: ( x9 <= len IT & 1 <= y9 ) by A9, FINSEQ_3:25;
A12: ( 1 <= x9 & y9 <= len IT ) by A9, FINSEQ_3:25;
percases ( x9 <> y9 or x9 = y9 ) ;
supposeA13: x9 <> y9 ; ::_thesis: x1 = x2
now__::_thesis:_x1_=_x2
percases ( x9 < y9 or y9 < x9 ) by A13, XXREAL_0:1;
suppose x9 < y9 ; ::_thesis: x1 = x2
hence x1 = x2 by A8, A10, A12; ::_thesis: verum
end;
suppose y9 < x9 ; ::_thesis: x1 = x2
hence x1 = x2 by A8, A10, A11; ::_thesis: verum
end;
end;
end;
hence x1 = x2 ; ::_thesis: verum
end;
suppose x9 = y9 ; ::_thesis: x1 = x2
hence x1 = x2 ; ::_thesis: verum
end;
end;
end;
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 );
definition
let G be Graph;
mode Path of G is V7() Chain of G;
end;
definition
let G be Graph;
mode OrientedPath of G is V7() oriented Chain of G;
end;
definition
let G be Graph;
let IT be Path of G;
attrIT 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) );
end;
:: 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) ) );
registration
let G be Graph;
cluster one-to-one empty -> cyclic for Chain of G;
coherence
for b1 being Path of G st b1 is empty holds
b1 is cyclic
proof
let p be Path of G; ::_thesis: ( p is empty implies p is cyclic )
assume A1: p is empty ; ::_thesis: p is cyclic
set x = the Vertex of G;
A2: the Vertex of G in the carrier of G ;
take <* the Vertex of G*> ; :: according to GRAPH_1:def_17 ::_thesis: ( len <* the Vertex of G*> = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) ) & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) )
thus len <* the Vertex of G*> = (len p) + 1 by A1, CARD_1:27, FINSEQ_1:39; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) ) & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) )
thus for n being Element of NAT st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) ) & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) )
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <* the Vertex of G*> implies <* the Vertex of G*> . n in the carrier of G )
assume that
A3: 1 <= n and
A4: n <= len <* the Vertex of G*> ; ::_thesis: <* the Vertex of G*> . n in the carrier of G
n <= 1 by A4, FINSEQ_1:39;
then n = 1 by A3, XXREAL_0:1;
hence <* the Vertex of G*> . n in the carrier of G by A2, FINSEQ_1:40; ::_thesis: verum
end;
thus for n being Element of NAT st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) by A1, CARD_1:27, XXREAL_0:2; ::_thesis: <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>)
thus <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) by FINSEQ_1:39; ::_thesis: verum
end;
end;
definition
let G be Graph;
mode Cycle of G is cyclic Path of G;
end;
definition
let G be Graph;
mode OrientedCycle of G is cyclic OrientedPath of G;
end;
definition
let G be Graph;
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
ex b1 being Graph st
( the carrier of b1 c= the carrier of G & the carrier' of b1 c= the carrier' of G & ( for v being set st v in the carrier' of b1 holds
( the Source of b1 . v = the Source of G . v & the Target of b1 . v = the Target of G . v & the Source of G . v in the carrier of b1 & the Target of G . v in the carrier of b1 ) ) )
proof
take G ; ::_thesis: ( the carrier of G c= the carrier of G & the carrier' of G c= the carrier' of G & ( for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) ) )
thus the carrier of G c= the carrier of G ; ::_thesis: ( the carrier' of G c= the carrier' of G & ( for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) ) )
thus the carrier' of G c= the carrier' of G ; ::_thesis: for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G )
let v be set ; ::_thesis: ( v in the carrier' of G implies ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) )
assume v in the carrier' of G ; ::_thesis: ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G )
hence ( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) by FUNCT_2:5; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines Subgraph GRAPH_1:def_18_:_
for G, b2 being Graph holds
( b2 is Subgraph of G iff ( the carrier of b2 c= the carrier of G & the carrier' of b2 c= the carrier' of G & ( for v being set st v in the carrier' of b2 holds
( the Source of b2 . v = the Source of G . v & the Target of b2 . v = the Target of G . v & the Source of G . v in the carrier of b2 & the Target of G . v in the carrier of b2 ) ) ) );
registration
let G be Graph;
cluster non empty feasible strict for Subgraph of G;
existence
ex b1 being Subgraph of G st b1 is strict
proof
reconsider S = MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) as Graph ;
for v being set st v in the carrier' of S holds
( the Source of S . v = the Source of G . v & the Target of S . v = the Target of G . v & the Source of G . v in the carrier of S & the Target of G . v in the carrier of S ) by FUNCT_2:5;
then S is Subgraph of G by Def18;
hence ex b1 being Subgraph of G st b1 is strict ; ::_thesis: verum
end;
end;
definition
let G be finite Graph;
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 b1 being Element of NAT ex B being finite set st
( B = the carrier of G & b1 = card B )
proof
set B = the carrier of G;
take card the carrier of G ; ::_thesis: ex B being finite set st
( B = the carrier of G & card the carrier of G = card B )
take the carrier of G ; ::_thesis: ( the carrier of G = the carrier of G & card the carrier of G = card the carrier of G )
thus ( the carrier of G = the carrier of G & card the carrier of G = card the carrier of G ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of NAT st ex B being finite set st
( B = the carrier of G & b1 = card B ) & ex B being finite set st
( B = the carrier of G & b2 = card B ) holds
b1 = b2 ;
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 b1 being Element of NAT ex B being finite set st
( B = the carrier' of G & b1 = card B )
proof
set B = the carrier' of G;
take card the carrier' of G ; ::_thesis: ex B being finite set st
( B = the carrier' of G & card the carrier' of G = card B )
take the carrier' of G ; ::_thesis: ( the carrier' of G = the carrier' of G & card the carrier' of G = card the carrier' of G )
thus ( the carrier' of G = the carrier' of G & card the carrier' of G = card the carrier' of G ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of NAT st ex B being finite set st
( B = the carrier' of G & b1 = card B ) & ex B being finite set st
( B = the carrier' of G & b2 = card B ) holds
b1 = b2 ;
end;
:: deftheorem defines VerticesCount GRAPH_1:def_19_:_
for G being finite Graph
for b2 being Element of NAT holds
( b2 = VerticesCount G iff ex B being finite set st
( B = the carrier of G & b2 = card B ) );
:: deftheorem defines EdgesCount GRAPH_1:def_20_:_
for G being finite Graph
for b2 being Element of NAT holds
( b2 = EdgesCount G iff ex B being finite set st
( B = the carrier' of G & b2 = card B ) );
definition
let G be finite Graph;
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 b1 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 ) ) ) & b1 = card X )
proof
defpred S1[ set ] means the Target of G . $1 = x;
consider X being set such that
A1: for z being set holds
( z in X iff ( z in the carrier' of G & S1[z] ) ) from XBOOLE_0:sch_1();
for z being set st z in X holds
z in the carrier' of G by A1;
then X c= the carrier' of G by TARSKI:def_3;
then reconsider X = X as finite set ;
take card X ; ::_thesis: 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 ) ) ) & card X = card X )
take X ; ::_thesis: ( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & card X = card X )
thus ( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Target of G . z = x ) ) ) & card X = card X ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 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 ) ) ) & b1 = 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 ) ) ) & b2 = card X ) holds
b1 = b2
proof
let n1, n2 be Element of NAT ; ::_thesis: ( 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 ) ) ) & n1 = 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 ) ) ) & n2 = card X ) implies n1 = n2 )
assume that
A2: 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 ) ) ) & n1 = card X ) and
A3: 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 ) ) ) & n2 = card X ) ; ::_thesis: n1 = n2
consider X1 being finite set such that
A4: for z being set holds
( z in X1 iff ( z in the carrier' of G & the Target of G . z = x ) ) and
A5: n1 = card X1 by A2;
consider X2 being finite set such that
A6: for z being set holds
( z in X2 iff ( z in the carrier' of G & the Target of G . z = x ) ) and
A7: n2 = card X2 by A3;
for z being set holds
( z in X1 iff z in X2 )
proof
let z be set ; ::_thesis: ( z in X1 iff z in X2 )
( z in X1 iff ( z in the carrier' of G & the Target of G . z = x ) ) by A4;
hence ( z in X1 iff z in X2 ) by A6; ::_thesis: verum
end;
hence n1 = n2 by A5, A7, TARSKI:1; ::_thesis: verum
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 b1 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 ) ) ) & b1 = card X )
proof
defpred S1[ set ] means the Source of G . $1 = x;
consider X being set such that
A8: for z being set holds
( z in X iff ( z in the carrier' of G & S1[z] ) ) from XBOOLE_0:sch_1();
for z being set st z in X holds
z in the carrier' of G by A8;
then X c= the carrier' of G by TARSKI:def_3;
then reconsider X = X as finite set ;
take card X ; ::_thesis: 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 ) ) ) & card X = card X )
take X ; ::_thesis: ( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & card X = card X )
thus ( ( for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = x ) ) ) & card X = card X ) by A8; ::_thesis: verum
end;
uniqueness
for b1, b2 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 ) ) ) & b1 = 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 ) ) ) & b2 = card X ) holds
b1 = b2
proof
let n1, n2 be Element of NAT ; ::_thesis: ( 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 ) ) ) & n1 = 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 ) ) ) & n2 = card X ) implies n1 = n2 )
assume that
A9: 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 ) ) ) & n1 = card X ) and
A10: 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 ) ) ) & n2 = card X ) ; ::_thesis: n1 = n2
consider X1 being finite set such that
A11: for z being set holds
( z in X1 iff ( z in the carrier' of G & the Source of G . z = x ) ) and
A12: n1 = card X1 by A9;
consider X2 being finite set such that
A13: for z being set holds
( z in X2 iff ( z in the carrier' of G & the Source of G . z = x ) ) and
A14: n2 = card X2 by A10;
for z being set holds
( z in X1 iff z in X2 )
proof
let z be set ; ::_thesis: ( z in X1 iff z in X2 )
( z in X1 iff ( z in the carrier' of G & the Source of G . z = x ) ) by A11;
hence ( z in X1 iff z in X2 ) by A13; ::_thesis: verum
end;
hence n1 = n2 by A12, A14, TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem defines EdgesIn GRAPH_1:def_21_:_
for G being finite Graph
for x being Vertex of G
for b3 being Element of NAT holds
( b3 = 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 ) ) ) & b3 = card X ) );
:: deftheorem defines EdgesOut GRAPH_1:def_22_:_
for G being finite Graph
for x being Vertex of G
for b3 being Element of NAT holds
( b3 = 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 ) ) ) & b3 = card X ) );
definition
let G be finite Graph;
let x be Vertex of G;
func Degree x -> Element of NAT equals :: GRAPH_1:def 23
(EdgesIn x) + (EdgesOut x);
correctness
coherence
(EdgesIn x) + (EdgesOut x) is Element of NAT ;
;
end;
:: 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);
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
let n be Element of NAT ; ::_thesis: for G being Graph
for p being Chain of G holds p | (Seg n) is Chain of G
let G be Graph; ::_thesis: for p being Chain of G holds p | (Seg n) is Chain of G
let p be Chain of G; ::_thesis: p | (Seg n) is Chain of G
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15;
A1: for n being Element of NAT st 1 <= n & n <= len q holds
q . n in the carrier' of G
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len q implies q . k in the carrier' of G )
assume that
A2: 1 <= k and
A3: k <= len q ; ::_thesis: q . k in the carrier' of G
A4: k in dom q by A2, A3, FINSEQ_3:25;
dom q c= dom p by RELAT_1:60;
then k <= len p by A4, FINSEQ_3:25;
then p . k in the carrier' of G by A2, Def14;
hence q . k in the carrier' of G by A4, FUNCT_1:47; ::_thesis: verum
end;
ex q1 being FinSequence st
( len q1 = (len q) + 1 & ( for n being Element of NAT st 1 <= n & n <= len q1 holds
q1 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds
ex x9, y9 being Vertex of G st
( x9 = q1 . n & y9 = q1 . (n + 1) & q . n joins x9,y9 ) ) )
proof
consider q1 being FinSequence such that
A5: len q1 = (len p) + 1 and
A6: for n being Element of NAT st 1 <= n & n <= len q1 holds
q1 . n in the carrier of G and
A7: for n being Element of NAT st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = q1 . n & y9 = q1 . (n + 1) & p . n joins x9,y9 ) by Def14;
reconsider q2 = q1 | (Seg (n + 1)) as FinSequence by FINSEQ_1:15;
take q2 ; ::_thesis: ( len q2 = (len q) + 1 & ( for n being Element of NAT st 1 <= n & n <= len q2 holds
q2 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds
ex x9, y9 being Vertex of G st
( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 ) ) )
thus A8: len q2 = (len q) + 1 ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len q2 holds
q2 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds
ex x9, y9 being Vertex of G st
( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 ) ) )
proof
A9: dom q2 = (dom q1) /\ (Seg (n + 1)) by RELAT_1:61
.= (Seg ((len p) + 1)) /\ (Seg (n + 1)) by A5, FINSEQ_1:def_3 ;
A10: dom q = (dom p) /\ (Seg n) by RELAT_1:61
.= (Seg (len p)) /\ (Seg n) by FINSEQ_1:def_3 ;
A11: now__::_thesis:_(_(len_p)_+_1_<=_n_+_1_implies_len_q2_=_(len_q)_+_1_)
assume A12: (len p) + 1 <= n + 1 ; ::_thesis: len q2 = (len q) + 1
then Seg ((len p) + 1) c= Seg (n + 1) by FINSEQ_1:5;
then dom q2 = Seg ((len p) + 1) by A9, XBOOLE_1:28;
then A13: len q2 = (len p) + 1 by FINSEQ_1:def_3;
len p <= n by A12, XREAL_1:6;
then Seg (len p) c= Seg n by FINSEQ_1:5;
then dom q = Seg (len p) by A10, XBOOLE_1:28;
hence len q2 = (len q) + 1 by A13, FINSEQ_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_n_+_1_<=_(len_p)_+_1_implies_len_q2_=_(len_q)_+_1_)
assume A14: n + 1 <= (len p) + 1 ; ::_thesis: len q2 = (len q) + 1
then Seg (n + 1) c= Seg ((len p) + 1) by FINSEQ_1:5;
then dom q2 = Seg (n + 1) by A9, XBOOLE_1:28;
then A15: len q2 = n + 1 by FINSEQ_1:def_3;
n <= len p by A14, XREAL_1:6;
then Seg n c= Seg (len p) by FINSEQ_1:5;
then dom q = Seg n by A10, XBOOLE_1:28;
hence len q2 = (len q) + 1 by A15, FINSEQ_1:def_3; ::_thesis: verum
end;
hence len q2 = (len q) + 1 by A11; ::_thesis: verum
end;
thus for n being Element of NAT st 1 <= n & n <= len q2 holds
q2 . n in the carrier of G ::_thesis: for n being Element of NAT st 1 <= n & n <= len q holds
ex x9, y9 being Vertex of G st
( x9 = q2 . n & y9 = q2 . (n + 1) & q . n joins x9,y9 )
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len q2 implies q2 . n in the carrier of G )
assume that
A16: 1 <= n and
A17: n <= len q2 ; ::_thesis: q2 . n in the carrier of G
A18: n in dom q2 by A16, A17, FINSEQ_3:25;
dom q2 c= dom q1 by RELAT_1:60;
then n <= len q1 by A18, FINSEQ_3:25;
then q1 . n in the carrier of G by A6, A16;
hence q2 . n in the carrier of G by A18, FUNCT_1:47; ::_thesis: verum
end;
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len q implies ex x9, y9 being Vertex of G st
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 ) )
assume that
A19: 1 <= k and
A20: k <= len q ; ::_thesis: ex x9, y9 being Vertex of G st
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 )
A21: k in dom q by A19, A20, FINSEQ_3:25;
dom q c= dom p by RELAT_1:60;
then k <= len p by A21, FINSEQ_3:25;
then consider x9, y9 being Vertex of G such that
A22: x9 = q1 . k and
A23: y9 = q1 . (k + 1) and
A24: p . k joins x9,y9 by A7, A19;
take x9 ; ::_thesis: ex y9 being Vertex of G st
( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 )
take y9 ; ::_thesis: ( x9 = q2 . k & y9 = q2 . (k + 1) & q . k joins x9,y9 )
len q <= (len q) + 1 by NAT_1:11;
then k <= len q2 by A8, A20, XXREAL_0:2;
then k in dom q2 by A19, FINSEQ_3:25;
hence x9 = q2 . k by A22, FUNCT_1:47; ::_thesis: ( y9 = q2 . (k + 1) & q . k joins x9,y9 )
A25: k + 1 <= len q2 by A8, A20, XREAL_1:7;
1 + 1 <= k + 1 by A19, XREAL_1:7;
then 1 <= k + 1 by XXREAL_0:2;
then k + 1 in dom q2 by A25, FINSEQ_3:25;
hence y9 = q2 . (k + 1) by A23, FUNCT_1:47; ::_thesis: q . k joins x9,y9
thus q . k joins x9,y9 by A21, A24, FUNCT_1:47; ::_thesis: verum
end;
hence p | (Seg n) is Chain of G by A1, Def14; ::_thesis: verum
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
let G be Graph; ::_thesis: 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
let H1, H2 be strict Subgraph of G; ::_thesis: ( the carrier of H1 = the carrier of H2 & the carrier' of H1 = the carrier' of H2 implies H1 = H2 )
assume that
A1: the carrier of H1 = the carrier of H2 and
A2: the carrier' of H1 = the carrier' of H2 ; ::_thesis: H1 = H2
A3: ( dom the Source of H1 = the carrier' of H1 & dom the Source of H2 = the carrier' of H2 ) by FUNCT_2:def_1;
A4: ( dom the Target of H1 = the carrier' of H1 & dom the Target of H2 = the carrier' of H2 ) by FUNCT_2:def_1;
for x being set st x in the carrier' of H1 holds
the Source of H1 . x = the Source of H2 . x
proof
let x be set ; ::_thesis: ( x in the carrier' of H1 implies the Source of H1 . x = the Source of H2 . x )
assume A5: x in the carrier' of H1 ; ::_thesis: the Source of H1 . x = the Source of H2 . x
hence the Source of H1 . x = the Source of G . x by Def18
.= the Source of H2 . x by A2, A5, Def18 ;
::_thesis: verum
end;
then A6: the Source of H1 = the Source of H2 by A2, A3, FUNCT_1:2;
for x being set st x in the carrier' of H1 holds
the Target of H1 . x = the Target of H2 . x
proof
let x be set ; ::_thesis: ( x in the carrier' of H1 implies the Target of H1 . x = the Target of H2 . x )
assume A7: x in the carrier' of H1 ; ::_thesis: the Target of H1 . x = the Target of H2 . x
hence the Target of H1 . x = the Target of G . x by Def18
.= the Target of H2 . x by A2, A7, Def18 ;
::_thesis: verum
end;
hence H1 = H2 by A1, A2, A4, A6, FUNCT_1:2; ::_thesis: verum
end;
definition
let G1, G2 be Graph;
predG1 c= G2 means :Def24: :: GRAPH_1:def 24
G1 is Subgraph of G2;
reflexivity
for G1 being Graph holds G1 is Subgraph of G1
proof
let G be Graph; ::_thesis: G is Subgraph of G
for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G . v & the Target of G . v = the Target of G . v & the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) by FUNCT_2:5;
hence G is Subgraph of G by Def18; ::_thesis: verum
end;
end;
:: deftheorem Def24 defines c= GRAPH_1:def_24_:_
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
let G be Graph; ::_thesis: 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) )
let H be Subgraph of G; ::_thesis: ( 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) )
set EH = the carrier' of H;
set VH = the carrier of H;
set EG = the carrier' of G;
set VG = the carrier of G;
( the carrier' of H c= the carrier' of G & the carrier of H c= the carrier of G ) by Def18;
then ( Funcs ( the carrier' of H, the carrier of H) c= PFuncs ( the carrier' of H, the carrier of H) & PFuncs ( the carrier' of H, the carrier of H) c= PFuncs ( the carrier' of G, the carrier of G) ) by FUNCT_2:72, PARTFUN1:50;
then A1: Funcs ( the carrier' of H, the carrier of H) c= PFuncs ( the carrier' of G, the carrier of G) by XBOOLE_1:1;
the Source of H in Funcs ( the carrier' of H, the carrier of H) by FUNCT_2:8;
hence the Source of H in PFuncs ( the carrier' of G, the carrier of G) by A1; ::_thesis: the Target of H in PFuncs ( the carrier' of G, the carrier of G)
the Target of H in Funcs ( the carrier' of H, the carrier of H) by FUNCT_2:8;
hence the Target of H in PFuncs ( the carrier' of G, the carrier of G) by A1; ::_thesis: verum
end;
definition
let G be Graph;
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
ex b1 being set st
for x being set holds
( x in b1 iff x is strict Subgraph of G )
proof
reconsider V = the carrier of G as non empty set ;
set E = the carrier' of G;
set Prod = [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):];
defpred S1[ set ] means ex y being Element of [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):] ex M being Graph ex v being non empty set ex e being set ex s, t being Function of e,v st
( y = $1 & v = y `1_4 & e = y `2_4 & s = y `3_4 & t = y `4_4 & M = MultiGraphStruct(# v,e,s,t #) & M is Subgraph of G );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):] & S1[x] ) ) from XBOOLE_0:sch_1();
defpred S2[ set , set ] means ex y being Element of [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):] ex M being strict Graph ex v being non empty set ex e being set ex s, t being Function of e,v st
( y = $1 & v = y `1_4 & e = y `2_4 & s = y `3_4 & t = y `4_4 & M = MultiGraphStruct(# v,e,s,t #) & M is Subgraph of G & $2 = M );
A2: for a, b, c being set st S2[a,b] & S2[a,c] holds
b = c ;
consider Y being set such that
A3: for z being set holds
( z in Y iff ex x being set st
( x in X & S2[x,z] ) ) from TARSKI:sch_1(A2);
take Y ; ::_thesis: for x being set holds
( x in Y iff x is strict Subgraph of G )
let x be set ; ::_thesis: ( x in Y iff x is strict Subgraph of G )
thus ( x in Y implies x is strict Subgraph of G ) ::_thesis: ( x is strict Subgraph of G implies x in Y )
proof
assume x in Y ; ::_thesis: x is strict Subgraph of G
then ex z being set st
( z in X & S2[z,x] ) by A3;
hence x is strict Subgraph of G ; ::_thesis: verum
end;
assume x is strict Subgraph of G ; ::_thesis: x in Y
then reconsider H = x as strict Subgraph of G ;
ex y being set st
( y in X & S2[y,x] )
proof
take y = [ the carrier of H, the carrier' of H, the Source of H, the Target of H]; ::_thesis: ( y in X & S2[y,x] )
A4: ( the carrier of H c= V & the carrier' of H c= the carrier' of G ) by Def18;
( the Source of H in PFuncs ( the carrier' of G,V) & the Target of H in PFuncs ( the carrier' of G,V) ) by Lm4;
then reconsider y9 = y as Element of [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):] by A4, MCART_1:80;
reconsider v = the carrier of H as non empty set ;
set e = the carrier' of H;
reconsider s = the Source of H as Function of the carrier' of H,v ;
reconsider t = the Target of H as Function of the carrier' of H,v ;
A5: ( v = y9 `1_4 & the carrier' of H = y9 `2_4 ) by MCART_1:def_8, MCART_1:def_9;
A6: ( s = y9 `3_4 & t = y9 `4_4 ) by MCART_1:def_10, MCART_1:def_11;
hence y in X by A1, A5; ::_thesis: S2[y,x]
thus S2[y,x] by A5, A6; ::_thesis: verum
end;
hence x in Y by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict Subgraph of G ) ) & ( for x being set holds
( x in b2 iff x is strict Subgraph of G ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is strict Subgraph of G;
let X1, X2 be set ; ::_thesis: ( ( for x being set holds
( x in X1 iff x is strict Subgraph of G ) ) & ( for x being set holds
( x in X2 iff x is strict Subgraph of G ) ) implies X1 = X2 )
assume that
A7: for x being set holds
( x in X1 iff S1[x] ) and
A8: for x being set holds
( x in X2 iff S1[x] ) ; ::_thesis: X1 = X2
thus X1 = X2 from XBOOLE_0:sch_2(A7, A8); ::_thesis: verum
end;
end;
:: deftheorem Def25 defines bool GRAPH_1:def_25_:_
for G being Graph
for b2 being set holds
( b2 = bool G iff for x being set holds
( x in b2 iff x is strict Subgraph of G ) );
scheme :: GRAPH_1:sch 1
GraphSeparation{ F1() -> Graph, P1[ set ] } :
ex X being set st
for x being set holds
( x in X iff ( x is strict Subgraph of F1() & P1[x] ) )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool F1() & P1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff ( x is strict Subgraph of F1() & P1[x] ) )
let x be set ; ::_thesis: ( x in X iff ( x is strict Subgraph of F1() & P1[x] ) )
thus ( x in X implies ( x is strict Subgraph of F1() & P1[x] ) ) ::_thesis: ( x is strict Subgraph of F1() & P1[x] implies x in X )
proof
assume A2: x in X ; ::_thesis: ( x is strict Subgraph of F1() & P1[x] )
then x in bool F1() by A1;
hence x is strict Subgraph of F1() by Def25; ::_thesis: P1[x]
thus P1[x] by A1, A2; ::_thesis: verum
end;
assume that
A3: x is strict Subgraph of F1() and
A4: P1[x] ; ::_thesis: x in X
x in bool F1() by A3, Def25;
hence x in X by A1, A4; ::_thesis: verum
end;
theorem :: GRAPH_1:1
for G being Graph holds
( dom the Source of G = the carrier' of G & dom the Target of G = the carrier' of G ) by FUNCT_2:def_1;
theorem :: GRAPH_1:2
for G being Graph
for x being Vertex of G holds x in the carrier of G ;
theorem :: GRAPH_1:3
for G being Graph
for v being set st v in the carrier' of G holds
( the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) by FUNCT_2:5;
theorem :: GRAPH_1:4
for n being Element of NAT
for G being Graph
for p being Chain of G holds p | (Seg n) is Chain of G by Lm2;
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 )
proof
let G1, G be Graph; ::_thesis: ( G1 c= G implies ( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G ) )
assume G1 c= G ; ::_thesis: ( the Source of G1 c= the Source of G & the Target of G1 c= the Target of G )
then A1: G1 is Subgraph of G by Def24;
for v being set st v in the Source of G1 holds
v in the Source of G
proof
let v be set ; ::_thesis: ( v in the Source of G1 implies v in the Source of G )
assume A2: v in the Source of G1 ; ::_thesis: v in the Source of G
then consider x, y being set such that
A3: [x,y] = v by RELAT_1:def_1;
A4: x in dom the Source of G1 by A2, A3, FUNCT_1:1;
A5: y = the Source of G1 . x by A2, A3, FUNCT_1:1;
A6: x in the carrier' of G1 by A4;
the carrier' of G1 c= the carrier' of G by A1, Def18;
then x in the carrier' of G by A6;
then A7: x in dom the Source of G by FUNCT_2:def_1;
y = the Source of G . x by A1, A4, A5, Def18;
hence v in the Source of G by A3, A7, FUNCT_1:def_2; ::_thesis: verum
end;
hence the Source of G1 c= the Source of G by TARSKI:def_3; ::_thesis: the Target of G1 c= the Target of G
for v being set st v in the Target of G1 holds
v in the Target of G
proof
let v be set ; ::_thesis: ( v in the Target of G1 implies v in the Target of G )
assume A8: v in the Target of G1 ; ::_thesis: v in the Target of G
then consider x, y being set such that
A9: [x,y] = v by RELAT_1:def_1;
A10: x in dom the Target of G1 by A8, A9, FUNCT_1:1;
A11: y = the Target of G1 . x by A8, A9, FUNCT_1:1;
A12: x in the carrier' of G1 by A10;
the carrier' of G1 c= the carrier' of G by A1, Def18;
then x in the carrier' of G by A12;
then A13: x in dom the Target of G by FUNCT_2:def_1;
y = the Target of G . x by A1, A10, A11, Def18;
hence v in the Target of G by A9, A13, FUNCT_1:def_2; ::_thesis: verum
end;
hence the Target of G1 c= the Target of G by TARSKI:def_3; ::_thesis: verum
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 )
proof
let G1, G2 be Graph; ::_thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies ( 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 ) )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: ( 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 )
set S12 = the Source of (G1 \/ G2);
set S1 = the Source of G1;
set S2 = the Source of G2;
set T12 = the Target of (G1 \/ G2);
set T1 = the Target of G1;
set T2 = the Target of G2;
for v being set holds
( v in the Source of (G1 \/ G2) iff v in the Source of G1 \/ the Source of G2 )
proof
let v be set ; ::_thesis: ( v in the Source of (G1 \/ G2) iff v in the Source of G1 \/ the Source of G2 )
thus ( v in the Source of (G1 \/ G2) implies v in the Source of G1 \/ the Source of G2 ) ::_thesis: ( v in the Source of G1 \/ the Source of G2 implies v in the Source of (G1 \/ G2) )
proof
assume A2: v in the Source of (G1 \/ G2) ; ::_thesis: v in the Source of G1 \/ the Source of G2
then consider x, y being set such that
A3: [x,y] = v by RELAT_1:def_1;
x in dom the Source of (G1 \/ G2) by A2, A3, FUNCT_1:1;
then x in the carrier' of (G1 \/ G2) ;
then A4: x in the carrier' of G1 \/ the carrier' of G2 by A1, Def5;
A5: now__::_thesis:_(_x_in_the_carrier'_of_G1_implies_[x,y]_in_the_Source_of_G1_\/_the_Source_of_G2_)
assume A6: x in the carrier' of G1 ; ::_thesis: [x,y] in the Source of G1 \/ the Source of G2
then A7: x in dom the Source of G1 by FUNCT_2:def_1;
the Source of G1 . x = the Source of (G1 \/ G2) . x by A1, A6, Def5
.= y by A2, A3, FUNCT_1:1 ;
then ( [x,y] in the Source of G1 or [x,y] in the Source of G2 ) by A7, FUNCT_1:def_2;
hence [x,y] in the Source of G1 \/ the Source of G2 by XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_x_in_the_carrier'_of_G2_implies_[x,y]_in_the_Source_of_G1_\/_the_Source_of_G2_)
assume A8: x in the carrier' of G2 ; ::_thesis: [x,y] in the Source of G1 \/ the Source of G2
then A9: x in dom the Source of G2 by FUNCT_2:def_1;
the Source of G2 . x = the Source of (G1 \/ G2) . x by A1, A8, Def5
.= y by A2, A3, FUNCT_1:1 ;
then ( [x,y] in the Source of G1 or [x,y] in the Source of G2 ) by A9, FUNCT_1:def_2;
hence [x,y] in the Source of G1 \/ the Source of G2 by XBOOLE_0:def_3; ::_thesis: verum
end;
hence v in the Source of G1 \/ the Source of G2 by A3, A4, A5, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A10: v in the Source of G1 \/ the Source of G2 ; ::_thesis: v in the Source of (G1 \/ G2)
A11: now__::_thesis:_(_v_in_the_Source_of_G1_implies_v_in_the_Source_of_(G1_\/_G2)_)
assume A12: v in the Source of G1 ; ::_thesis: v in the Source of (G1 \/ G2)
then consider x, y being set such that
A13: [x,y] = v by RELAT_1:def_1;
A14: x in dom the Source of G1 by A12, A13, FUNCT_1:1;
A15: y = the Source of G1 . x by A12, A13, FUNCT_1:1;
x in the carrier' of G1 \/ the carrier' of G2 by A14, XBOOLE_0:def_3;
then x in the carrier' of (G1 \/ G2) by A1, Def5;
then A16: x in dom the Source of (G1 \/ G2) by FUNCT_2:def_1;
the Source of (G1 \/ G2) . x = y by A1, A14, A15, Def5;
hence v in the Source of (G1 \/ G2) by A13, A16, FUNCT_1:def_2; ::_thesis: verum
end;
now__::_thesis:_(_v_in_the_Source_of_G2_implies_v_in_the_Source_of_(G1_\/_G2)_)
assume A17: v in the Source of G2 ; ::_thesis: v in the Source of (G1 \/ G2)
then consider x, y being set such that
A18: [x,y] = v by RELAT_1:def_1;
A19: x in dom the Source of G2 by A17, A18, FUNCT_1:1;
A20: y = the Source of G2 . x by A17, A18, FUNCT_1:1;
x in the carrier' of G1 \/ the carrier' of G2 by A19, XBOOLE_0:def_3;
then x in the carrier' of (G1 \/ G2) by A1, Def5;
then A21: x in dom the Source of (G1 \/ G2) by FUNCT_2:def_1;
the Source of (G1 \/ G2) . x = y by A1, A19, A20, Def5;
hence v in the Source of (G1 \/ G2) by A18, A21, FUNCT_1:def_2; ::_thesis: verum
end;
hence v in the Source of (G1 \/ G2) by A10, A11, XBOOLE_0:def_3; ::_thesis: verum
end;
hence the Source of (G1 \/ G2) = the Source of G1 \/ the Source of G2 by TARSKI:1; ::_thesis: the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2
for v being set holds
( v in the Target of (G1 \/ G2) iff v in the Target of G1 \/ the Target of G2 )
proof
let v be set ; ::_thesis: ( v in the Target of (G1 \/ G2) iff v in the Target of G1 \/ the Target of G2 )
thus ( v in the Target of (G1 \/ G2) implies v in the Target of G1 \/ the Target of G2 ) ::_thesis: ( v in the Target of G1 \/ the Target of G2 implies v in the Target of (G1 \/ G2) )
proof
assume A22: v in the Target of (G1 \/ G2) ; ::_thesis: v in the Target of G1 \/ the Target of G2
then consider x, y being set such that
A23: [x,y] = v by RELAT_1:def_1;
x in dom the Target of (G1 \/ G2) by A22, A23, FUNCT_1:1;
then x in the carrier' of (G1 \/ G2) ;
then A24: x in the carrier' of G1 \/ the carrier' of G2 by A1, Def5;
A25: now__::_thesis:_(_x_in_the_carrier'_of_G1_implies_[x,y]_in_the_Target_of_G1_\/_the_Target_of_G2_)
assume A26: x in the carrier' of G1 ; ::_thesis: [x,y] in the Target of G1 \/ the Target of G2
then A27: x in dom the Target of G1 by FUNCT_2:def_1;
the Target of G1 . x = the Target of (G1 \/ G2) . x by A1, A26, Def5
.= y by A22, A23, FUNCT_1:1 ;
then ( [x,y] in the Target of G1 or [x,y] in the Target of G2 ) by A27, FUNCT_1:def_2;
hence [x,y] in the Target of G1 \/ the Target of G2 by XBOOLE_0:def_3; ::_thesis: verum
end;
now__::_thesis:_(_x_in_the_carrier'_of_G2_implies_[x,y]_in_the_Target_of_G1_\/_the_Target_of_G2_)
assume A28: x in the carrier' of G2 ; ::_thesis: [x,y] in the Target of G1 \/ the Target of G2
then A29: x in dom the Target of G2 by FUNCT_2:def_1;
the Target of G2 . x = the Target of (G1 \/ G2) . x by A1, A28, Def5
.= y by A22, A23, FUNCT_1:1 ;
then ( [x,y] in the Target of G1 or [x,y] in the Target of G2 ) by A29, FUNCT_1:def_2;
hence [x,y] in the Target of G1 \/ the Target of G2 by XBOOLE_0:def_3; ::_thesis: verum
end;
hence v in the Target of G1 \/ the Target of G2 by A23, A24, A25, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A30: v in the Target of G1 \/ the Target of G2 ; ::_thesis: v in the Target of (G1 \/ G2)
A31: now__::_thesis:_(_v_in_the_Target_of_G1_implies_v_in_the_Target_of_(G1_\/_G2)_)
assume A32: v in the Target of G1 ; ::_thesis: v in the Target of (G1 \/ G2)
then consider x, y being set such that
A33: [x,y] = v by RELAT_1:def_1;
A34: x in dom the Target of G1 by A32, A33, FUNCT_1:1;
A35: y = the Target of G1 . x by A32, A33, FUNCT_1:1;
x in the carrier' of G1 \/ the carrier' of G2 by A34, XBOOLE_0:def_3;
then x in the carrier' of (G1 \/ G2) by A1, Def5;
then A36: x in dom the Target of (G1 \/ G2) by FUNCT_2:def_1;
the Target of (G1 \/ G2) . x = y by A1, A34, A35, Def5;
hence v in the Target of (G1 \/ G2) by A33, A36, FUNCT_1:def_2; ::_thesis: verum
end;
now__::_thesis:_(_v_in_the_Target_of_G2_implies_v_in_the_Target_of_(G1_\/_G2)_)
assume A37: v in the Target of G2 ; ::_thesis: v in the Target of (G1 \/ G2)
then consider x, y being set such that
A38: [x,y] = v by RELAT_1:def_1;
A39: x in dom the Target of G2 by A37, A38, FUNCT_1:1;
A40: y = the Target of G2 . x by A37, A38, FUNCT_1:1;
x in the carrier' of G1 \/ the carrier' of G2 by A39, XBOOLE_0:def_3;
then x in the carrier' of (G1 \/ G2) by A1, Def5;
then A41: x in dom the Target of (G1 \/ G2) by FUNCT_2:def_1;
the Target of (G1 \/ G2) . x = y by A1, A39, A40, Def5;
hence v in the Target of (G1 \/ G2) by A38, A41, FUNCT_1:def_2; ::_thesis: verum
end;
hence v in the Target of (G1 \/ G2) by A30, A31, XBOOLE_0:def_3; ::_thesis: verum
end;
hence the Target of (G1 \/ G2) = the Target of G1 \/ the Target of G2 by TARSKI:1; ::_thesis: verum
end;
theorem Th7: :: GRAPH_1:7
for G being strict Graph holds G = G \/ G
proof
let G be strict Graph; ::_thesis: G = G \/ G
A1: the carrier of (G \/ G) = the carrier of G \/ the carrier of G by Def5
.= the carrier of G ;
A2: the carrier' of (G \/ G) = the carrier' of G \/ the carrier' of G by Def5
.= the carrier' of G ;
then A3: dom the Source of G = the carrier' of (G \/ G) by FUNCT_2:def_1
.= dom the Source of (G \/ G) by FUNCT_2:def_1 ;
for v being set st v in dom the Source of G holds
the Source of G . v = the Source of (G \/ G) . v by Def5;
then A4: the Source of G = the Source of (G \/ G) by A3, FUNCT_1:2;
A5: dom the Target of G = the carrier' of (G \/ G) by A2, FUNCT_2:def_1
.= dom the Target of (G \/ G) by FUNCT_2:def_1 ;
for v being set st v in dom the Target of G holds
the Target of G . v = the Target of (G \/ G) . v by Def5;
hence G = G \/ G by A1, A2, A4, A5, FUNCT_1:2; ::_thesis: verum
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
proof
let G1, G2 be Graph; ::_thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies G1 \/ G2 = G2 \/ G1 )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: G1 \/ G2 = G2 \/ G1
then A2: the carrier of (G1 \/ G2) = the carrier of G2 \/ the carrier of G1 by Def5
.= the carrier of (G2 \/ G1) by A1, Def5 ;
A3: the carrier' of (G1 \/ G2) = the carrier' of G2 \/ the carrier' of G1 by A1, Def5
.= the carrier' of (G2 \/ G1) by A1, Def5 ;
then A4: dom the Source of (G1 \/ G2) = the carrier' of (G2 \/ G1) by FUNCT_2:def_1
.= dom the Source of (G2 \/ G1) by FUNCT_2:def_1 ;
for v being set st v in dom the Source of (G1 \/ G2) holds
the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
proof
let v be set ; ::_thesis: ( v in dom the Source of (G1 \/ G2) implies the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v )
assume v in dom the Source of (G1 \/ G2) ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
then v in the carrier' of (G1 \/ G2) ;
then A5: v in the carrier' of G1 \/ the carrier' of G2 by A1, Def5;
A6: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_(G2_\/_G1)_._v_)
assume A7: v in the carrier' of G1 ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
hence the Source of (G1 \/ G2) . v = the Source of G1 . v by A1, Def5
.= the Source of (G2 \/ G1) . v by A1, A7, Def5 ;
::_thesis: verum
end;
now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_(G2_\/_G1)_._v_)
assume A8: v in the carrier' of G2 ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v
hence the Source of (G1 \/ G2) . v = the Source of G2 . v by A1, Def5
.= the Source of (G2 \/ G1) . v by A1, A8, Def5 ;
::_thesis: verum
end;
hence the Source of (G1 \/ G2) . v = the Source of (G2 \/ G1) . v by A5, A6, XBOOLE_0:def_3; ::_thesis: verum
end;
then A9: the Source of (G1 \/ G2) = the Source of (G2 \/ G1) by A4, FUNCT_1:2;
A10: dom the Target of (G1 \/ G2) = the carrier' of (G2 \/ G1) by A3, FUNCT_2:def_1
.= dom the Target of (G2 \/ G1) by FUNCT_2:def_1 ;
for v being set st v in dom the Target of (G1 \/ G2) holds
the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
proof
let v be set ; ::_thesis: ( v in dom the Target of (G1 \/ G2) implies the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v )
assume v in dom the Target of (G1 \/ G2) ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
then v in the carrier' of (G1 \/ G2) ;
then A11: v in the carrier' of G1 \/ the carrier' of G2 by A1, Def5;
A12: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_(G2_\/_G1)_._v_)
assume A13: v in the carrier' of G1 ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
hence the Target of (G1 \/ G2) . v = the Target of G1 . v by A1, Def5
.= the Target of (G2 \/ G1) . v by A1, A13, Def5 ;
::_thesis: verum
end;
now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_(G2_\/_G1)_._v_)
assume A14: v in the carrier' of G2 ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v
hence the Target of (G1 \/ G2) . v = the Target of G2 . v by A1, Def5
.= the Target of (G2 \/ G1) . v by A1, A14, Def5 ;
::_thesis: verum
end;
hence the Target of (G1 \/ G2) . v = the Target of (G2 \/ G1) . v by A11, A12, XBOOLE_0:def_3; ::_thesis: verum
end;
hence G1 \/ G2 = G2 \/ G1 by A2, A3, A9, A10, FUNCT_1:2; ::_thesis: verum
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)
proof
let G1, G2, G3 be Graph; ::_thesis: ( 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 implies (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) )
assume that
A1: the Source of G1 tolerates the Source of G2 and
A2: the Target of G1 tolerates the Target of G2 and
A3: the Source of G1 tolerates the Source of G3 and
A4: the Target of G1 tolerates the Target of G3 and
A5: the Source of G2 tolerates the Source of G3 and
A6: the Target of G2 tolerates the Target of G3 ; ::_thesis: (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)
A7: for v being set st v in (dom the Source of (G1 \/ G2)) /\ (dom the Source of G3) holds
the Source of (G1 \/ G2) . v = the Source of G3 . v
proof
let v be set ; ::_thesis: ( v in (dom the Source of (G1 \/ G2)) /\ (dom the Source of G3) implies the Source of (G1 \/ G2) . v = the Source of G3 . v )
assume A8: v in (dom the Source of (G1 \/ G2)) /\ (dom the Source of G3) ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of G3 . v
then A9: v in dom the Source of G3 by XBOOLE_0:def_4;
v in dom the Source of (G1 \/ G2) by A8, XBOOLE_0:def_4;
then v in the carrier' of (G1 \/ G2) ;
then A10: v in the carrier' of G1 \/ the carrier' of G2 by A1, A2, Def5;
A11: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_G3_._v_)
assume A12: v in the carrier' of G1 ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of G3 . v
then v in dom the Source of G1 by FUNCT_2:def_1;
then A13: v in (dom the Source of G1) /\ (dom the Source of G3) by A9, XBOOLE_0:def_4;
thus the Source of (G1 \/ G2) . v = the Source of G1 . v by A1, A2, A12, Def5
.= the Source of G3 . v by A3, A13, PARTFUN1:def_4 ; ::_thesis: verum
end;
now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_G3_._v_)
assume A14: v in the carrier' of G2 ; ::_thesis: the Source of (G1 \/ G2) . v = the Source of G3 . v
then v in dom the Source of G2 by FUNCT_2:def_1;
then A15: v in (dom the Source of G2) /\ (dom the Source of G3) by A9, XBOOLE_0:def_4;
thus the Source of (G1 \/ G2) . v = the Source of G2 . v by A1, A2, A14, Def5
.= the Source of G3 . v by A5, A15, PARTFUN1:def_4 ; ::_thesis: verum
end;
hence the Source of (G1 \/ G2) . v = the Source of G3 . v by A10, A11, XBOOLE_0:def_3; ::_thesis: verum
end;
A16: for v being set st v in (dom the Target of (G1 \/ G2)) /\ (dom the Target of G3) holds
the Target of (G1 \/ G2) . v = the Target of G3 . v
proof
let v be set ; ::_thesis: ( v in (dom the Target of (G1 \/ G2)) /\ (dom the Target of G3) implies the Target of (G1 \/ G2) . v = the Target of G3 . v )
assume A17: v in (dom the Target of (G1 \/ G2)) /\ (dom the Target of G3) ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of G3 . v
then A18: v in dom the Target of G3 by XBOOLE_0:def_4;
v in dom the Target of (G1 \/ G2) by A17, XBOOLE_0:def_4;
then v in the carrier' of (G1 \/ G2) ;
then A19: v in the carrier' of G1 \/ the carrier' of G2 by A1, A2, Def5;
A20: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_G3_._v_)
assume A21: v in the carrier' of G1 ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of G3 . v
then v in dom the Target of G1 by FUNCT_2:def_1;
then A22: v in (dom the Target of G1) /\ (dom the Target of G3) by A18, XBOOLE_0:def_4;
thus the Target of (G1 \/ G2) . v = the Target of G1 . v by A1, A2, A21, Def5
.= the Target of G3 . v by A4, A22, PARTFUN1:def_4 ; ::_thesis: verum
end;
now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_G3_._v_)
assume A23: v in the carrier' of G2 ; ::_thesis: the Target of (G1 \/ G2) . v = the Target of G3 . v
then v in dom the Target of G2 by FUNCT_2:def_1;
then A24: v in (dom the Target of G2) /\ (dom the Target of G3) by A18, XBOOLE_0:def_4;
thus the Target of (G1 \/ G2) . v = the Target of G2 . v by A1, A2, A23, Def5
.= the Target of G3 . v by A6, A24, PARTFUN1:def_4 ; ::_thesis: verum
end;
hence the Target of (G1 \/ G2) . v = the Target of G3 . v by A19, A20, XBOOLE_0:def_3; ::_thesis: verum
end;
A25: the Source of (G1 \/ G2) tolerates the Source of G3 by A7, PARTFUN1:def_4;
A26: the Target of (G1 \/ G2) tolerates the Target of G3 by A16, PARTFUN1:def_4;
A27: for v being set st v in (dom the Source of G1) /\ (dom the Source of (G2 \/ G3)) holds
the Source of G1 . v = the Source of (G2 \/ G3) . v
proof
let v be set ; ::_thesis: ( v in (dom the Source of G1) /\ (dom the Source of (G2 \/ G3)) implies the Source of G1 . v = the Source of (G2 \/ G3) . v )
assume A28: v in (dom the Source of G1) /\ (dom the Source of (G2 \/ G3)) ; ::_thesis: the Source of G1 . v = the Source of (G2 \/ G3) . v
then A29: v in dom the Source of G1 by XBOOLE_0:def_4;
v in the carrier' of (G2 \/ G3) by A28;
then v in the carrier' of G2 \/ the carrier' of G3 by A5, A6, Def5;
then v in the carrier' of G2 \/ (dom the Source of G3) by FUNCT_2:def_1;
then A30: v in (dom the Source of G2) \/ (dom the Source of G3) by FUNCT_2:def_1;
A31: now__::_thesis:_(_v_in_dom_the_Source_of_G2_implies_the_Source_of_(G2_\/_G3)_._v_=_the_Source_of_G1_._v_)
assume A32: v in dom the Source of G2 ; ::_thesis: the Source of (G2 \/ G3) . v = the Source of G1 . v
then A33: v in (dom the Source of G1) /\ (dom the Source of G2) by A29, XBOOLE_0:def_4;
thus the Source of (G2 \/ G3) . v = the Source of G2 . v by A5, A6, A32, Def5
.= the Source of G1 . v by A1, A33, PARTFUN1:def_4 ; ::_thesis: verum
end;
now__::_thesis:_(_v_in_dom_the_Source_of_G3_implies_the_Source_of_(G2_\/_G3)_._v_=_the_Source_of_G1_._v_)
assume A34: v in dom the Source of G3 ; ::_thesis: the Source of (G2 \/ G3) . v = the Source of G1 . v
then A35: v in (dom the Source of G1) /\ (dom the Source of G3) by A29, XBOOLE_0:def_4;
thus the Source of (G2 \/ G3) . v = the Source of G3 . v by A5, A6, A34, Def5
.= the Source of G1 . v by A3, A35, PARTFUN1:def_4 ; ::_thesis: verum
end;
hence the Source of G1 . v = the Source of (G2 \/ G3) . v by A30, A31, XBOOLE_0:def_3; ::_thesis: verum
end;
A36: for v being set st v in (dom the Target of G1) /\ (dom the Target of (G2 \/ G3)) holds
the Target of G1 . v = the Target of (G2 \/ G3) . v
proof
let v be set ; ::_thesis: ( v in (dom the Target of G1) /\ (dom the Target of (G2 \/ G3)) implies the Target of G1 . v = the Target of (G2 \/ G3) . v )
assume A37: v in (dom the Target of G1) /\ (dom the Target of (G2 \/ G3)) ; ::_thesis: the Target of G1 . v = the Target of (G2 \/ G3) . v
then A38: v in dom the Target of G1 by XBOOLE_0:def_4;
v in the carrier' of (G2 \/ G3) by A37;
then v in the carrier' of G2 \/ the carrier' of G3 by A5, A6, Def5;
then v in the carrier' of G2 \/ (dom the Target of G3) by FUNCT_2:def_1;
then A39: v in (dom the Target of G2) \/ (dom the Target of G3) by FUNCT_2:def_1;
A40: now__::_thesis:_(_v_in_dom_the_Target_of_G2_implies_the_Target_of_(G2_\/_G3)_._v_=_the_Target_of_G1_._v_)
assume A41: v in dom the Target of G2 ; ::_thesis: the Target of (G2 \/ G3) . v = the Target of G1 . v
then A42: v in (dom the Target of G1) /\ (dom the Target of G2) by A38, XBOOLE_0:def_4;
thus the Target of (G2 \/ G3) . v = the Target of G2 . v by A5, A6, A41, Def5
.= the Target of G1 . v by A2, A42, PARTFUN1:def_4 ; ::_thesis: verum
end;
now__::_thesis:_(_v_in_dom_the_Target_of_G3_implies_the_Target_of_(G2_\/_G3)_._v_=_the_Target_of_G1_._v_)
assume A43: v in dom the Target of G3 ; ::_thesis: the Target of (G2 \/ G3) . v = the Target of G1 . v
then A44: v in (dom the Target of G1) /\ (dom the Target of G3) by A38, XBOOLE_0:def_4;
thus the Target of (G2 \/ G3) . v = the Target of G3 . v by A5, A6, A43, Def5
.= the Target of G1 . v by A4, A44, PARTFUN1:def_4 ; ::_thesis: verum
end;
hence the Target of G1 . v = the Target of (G2 \/ G3) . v by A39, A40, XBOOLE_0:def_3; ::_thesis: verum
end;
A45: the Source of G1 tolerates the Source of (G2 \/ G3) by A27, PARTFUN1:def_4;
A46: the Target of G1 tolerates the Target of (G2 \/ G3) by A36, PARTFUN1:def_4;
A47: the carrier' of ((G1 \/ G2) \/ G3) = the carrier' of (G1 \/ G2) \/ the carrier' of G3 by A25, A26, Def5
.= ( the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3 by A1, A2, Def5
.= the carrier' of G1 \/ ( the carrier' of G2 \/ the carrier' of G3) by XBOOLE_1:4
.= the carrier' of G1 \/ the carrier' of (G2 \/ G3) by A5, A6, Def5
.= the carrier' of (G1 \/ (G2 \/ G3)) by A45, A46, Def5 ;
A48: the carrier of ((G1 \/ G2) \/ G3) = the carrier of (G1 \/ G2) \/ the carrier of G3 by A25, A26, Def5
.= ( the carrier of G1 \/ the carrier of G2) \/ the carrier of G3 by A1, A2, Def5
.= the carrier of G1 \/ ( the carrier of G2 \/ the carrier of G3) by XBOOLE_1:4
.= the carrier of G1 \/ the carrier of (G2 \/ G3) by A5, A6, Def5
.= the carrier of (G1 \/ (G2 \/ G3)) by A45, A46, Def5 ;
A49: dom the Source of ((G1 \/ G2) \/ G3) = the carrier' of (G1 \/ (G2 \/ G3)) by A47, FUNCT_2:def_1
.= dom the Source of (G1 \/ (G2 \/ G3)) by FUNCT_2:def_1 ;
for v being set st v in dom the Source of ((G1 \/ G2) \/ G3) holds
the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
proof
let v be set ; ::_thesis: ( v in dom the Source of ((G1 \/ G2) \/ G3) implies the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v )
assume A50: v in dom the Source of ((G1 \/ G2) \/ G3) ; ::_thesis: the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
dom the Source of ((G1 \/ G2) \/ G3) = the carrier' of ((G1 \/ G2) \/ G3) by FUNCT_2:def_1
.= the carrier' of (G1 \/ G2) \/ the carrier' of G3 by A25, A26, Def5
.= ( the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3 by A1, A2, Def5 ;
then A51: ( v in the carrier' of G1 \/ the carrier' of G2 or v in the carrier' of G3 ) by A50, XBOOLE_0:def_3;
A52: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Source_of_((G1_\/_G2)_\/_G3)_._v_=_the_Source_of_(G1_\/_(G2_\/_G3))_._v_)
assume A53: v in the carrier' of G1 ; ::_thesis: the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
the carrier' of G1 c= the carrier' of G1 \/ the carrier' of G2 by XBOOLE_1:7;
then the carrier' of G1 c= the carrier' of (G1 \/ G2) by A1, A2, Def5;
hence the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ G2) . v by A25, A26, A53, Def5
.= the Source of G1 . v by A1, A2, A53, Def5
.= the Source of (G1 \/ (G2 \/ G3)) . v by A45, A46, A53, Def5 ;
::_thesis: verum
end;
A54: now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Source_of_((G1_\/_G2)_\/_G3)_._v_=_the_Source_of_(G1_\/_(G2_\/_G3))_._v_)
assume A55: v in the carrier' of G2 ; ::_thesis: the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
the carrier' of G2 c= the carrier' of G1 \/ the carrier' of G2 by XBOOLE_1:7;
then A56: the carrier' of G2 c= the carrier' of (G1 \/ G2) by A1, A2, Def5;
the carrier' of G2 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7;
then A57: the carrier' of G2 c= the carrier' of (G2 \/ G3) by A5, A6, Def5;
thus the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ G2) . v by A25, A26, A55, A56, Def5
.= the Source of G2 . v by A1, A2, A55, Def5
.= the Source of (G2 \/ G3) . v by A5, A6, A55, Def5
.= the Source of (G1 \/ (G2 \/ G3)) . v by A45, A46, A55, A57, Def5 ; ::_thesis: verum
end;
now__::_thesis:_(_v_in_the_carrier'_of_G3_implies_the_Source_of_((G1_\/_G2)_\/_G3)_._v_=_the_Source_of_(G1_\/_(G2_\/_G3))_._v_)
assume A58: v in the carrier' of G3 ; ::_thesis: the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v
the carrier' of G3 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7;
then A59: the carrier' of G3 c= the carrier' of (G2 \/ G3) by A5, A6, Def5;
thus the Source of ((G1 \/ G2) \/ G3) . v = the Source of G3 . v by A25, A26, A58, Def5
.= the Source of (G2 \/ G3) . v by A5, A6, A58, Def5
.= the Source of (G1 \/ (G2 \/ G3)) . v by A45, A46, A58, A59, Def5 ; ::_thesis: verum
end;
hence the Source of ((G1 \/ G2) \/ G3) . v = the Source of (G1 \/ (G2 \/ G3)) . v by A51, A52, A54, XBOOLE_0:def_3; ::_thesis: verum
end;
then A60: the Source of ((G1 \/ G2) \/ G3) = the Source of (G1 \/ (G2 \/ G3)) by A49, FUNCT_1:2;
A61: dom the Target of ((G1 \/ G2) \/ G3) = the carrier' of (G1 \/ (G2 \/ G3)) by A47, FUNCT_2:def_1
.= dom the Target of (G1 \/ (G2 \/ G3)) by FUNCT_2:def_1 ;
for v being set st v in dom the Target of ((G1 \/ G2) \/ G3) holds
the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
proof
let v be set ; ::_thesis: ( v in dom the Target of ((G1 \/ G2) \/ G3) implies the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v )
assume A62: v in dom the Target of ((G1 \/ G2) \/ G3) ; ::_thesis: the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
dom the Target of ((G1 \/ G2) \/ G3) = the carrier' of ((G1 \/ G2) \/ G3) by FUNCT_2:def_1
.= the carrier' of (G1 \/ G2) \/ the carrier' of G3 by A25, A26, Def5
.= ( the carrier' of G1 \/ the carrier' of G2) \/ the carrier' of G3 by A1, A2, Def5 ;
then A63: ( v in the carrier' of G1 \/ the carrier' of G2 or v in the carrier' of G3 ) by A62, XBOOLE_0:def_3;
A64: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_the_Target_of_((G1_\/_G2)_\/_G3)_._v_=_the_Target_of_(G1_\/_(G2_\/_G3))_._v_)
assume A65: v in the carrier' of G1 ; ::_thesis: the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
the carrier' of G1 c= the carrier' of G1 \/ the carrier' of G2 by XBOOLE_1:7;
then the carrier' of G1 c= the carrier' of (G1 \/ G2) by A1, A2, Def5;
hence the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ G2) . v by A25, A26, A65, Def5
.= the Target of G1 . v by A1, A2, A65, Def5
.= the Target of (G1 \/ (G2 \/ G3)) . v by A45, A46, A65, Def5 ;
::_thesis: verum
end;
A66: now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_the_Target_of_((G1_\/_G2)_\/_G3)_._v_=_the_Target_of_(G1_\/_(G2_\/_G3))_._v_)
assume A67: v in the carrier' of G2 ; ::_thesis: the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
the carrier' of G2 c= the carrier' of G1 \/ the carrier' of G2 by XBOOLE_1:7;
then A68: the carrier' of G2 c= the carrier' of (G1 \/ G2) by A1, A2, Def5;
the carrier' of G2 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7;
then A69: the carrier' of G2 c= the carrier' of (G2 \/ G3) by A5, A6, Def5;
thus the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ G2) . v by A25, A26, A67, A68, Def5
.= the Target of G2 . v by A1, A2, A67, Def5
.= the Target of (G2 \/ G3) . v by A5, A6, A67, Def5
.= the Target of (G1 \/ (G2 \/ G3)) . v by A45, A46, A67, A69, Def5 ; ::_thesis: verum
end;
now__::_thesis:_(_v_in_the_carrier'_of_G3_implies_the_Target_of_((G1_\/_G2)_\/_G3)_._v_=_the_Target_of_(G1_\/_(G2_\/_G3))_._v_)
assume A70: v in the carrier' of G3 ; ::_thesis: the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v
the carrier' of G3 c= the carrier' of G2 \/ the carrier' of G3 by XBOOLE_1:7;
then A71: the carrier' of G3 c= the carrier' of (G2 \/ G3) by A5, A6, Def5;
thus the Target of ((G1 \/ G2) \/ G3) . v = the Target of G3 . v by A25, A26, A70, Def5
.= the Target of (G2 \/ G3) . v by A5, A6, A70, Def5
.= the Target of (G1 \/ (G2 \/ G3)) . v by A45, A46, A70, A71, Def5 ; ::_thesis: verum
end;
hence the Target of ((G1 \/ G2) \/ G3) . v = the Target of (G1 \/ (G2 \/ G3)) . v by A63, A64, A66, XBOOLE_0:def_3; ::_thesis: verum
end;
hence (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) by A47, A48, A60, A61, FUNCT_1:2; ::_thesis: verum
end;
theorem Th10: :: GRAPH_1:10
for G, G1, G2 being Graph st G is_sum_of G1,G2 holds
G is_sum_of G2,G1
proof
let G, G1, G2 be Graph; ::_thesis: ( G is_sum_of G1,G2 implies G is_sum_of G2,G1 )
assume A1: G is_sum_of G1,G2 ; ::_thesis: G is_sum_of G2,G1
then A2: the Target of G1 tolerates the Target of G2 by Def6;
A3: ( 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 ) by A1, Def6;
A4: the Source of G2 tolerates the Source of G1 by A1, Def6;
MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G2 \/ G1 by A2, A3, Th8;
hence G is_sum_of G2,G1 by A2, A4, Def6; ::_thesis: verum
end;
theorem :: GRAPH_1:11
for G being strict Graph holds G is_sum_of G,G
proof
let G be strict Graph; ::_thesis: G is_sum_of G,G
G = G \/ G by Th7;
hence G is_sum_of G,G by Def6; ::_thesis: verum
end;
theorem Th12: :: GRAPH_1:12
for G1, G2 being Graph st ex G being Graph st
( G1 c= G & G2 c= G ) holds
G1 \/ G2 = G2 \/ G1
proof
let G1, G2 be Graph; ::_thesis: ( ex G being Graph st
( G1 c= G & G2 c= G ) implies G1 \/ G2 = G2 \/ G1 )
given G being Graph such that A1: ( G1 c= G & G2 c= G ) ; ::_thesis: G1 \/ G2 = G2 \/ G1
A2: ( the Source of G1 c= the Source of G & the Source of G2 c= the Source of G ) by A1, Th5;
A3: ( the Target of G1 c= the Target of G & the Target of G2 c= the Target of G ) by A1, Th5;
A4: the Source of G1 tolerates the Source of G2 by A2, PARTFUN1:52;
the Target of G1 tolerates the Target of G2 by A3, PARTFUN1:52;
hence G1 \/ G2 = G2 \/ G1 by A4, Th8; ::_thesis: verum
end;
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)
proof
let G1, G2, G3 be Graph; ::_thesis: ( ex G being Graph st
( G1 c= G & G2 c= G & G3 c= G ) implies (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) )
given G being Graph such that A1: G1 c= G and
A2: G2 c= G and
A3: G3 c= G ; ::_thesis: (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3)
A4: the Source of G1 c= the Source of G by A1, Th5;
A5: the Source of G2 c= the Source of G by A2, Th5;
A6: the Source of G3 c= the Source of G by A3, Th5;
A7: the Target of G1 c= the Target of G by A1, Th5;
A8: the Target of G2 c= the Target of G by A2, Th5;
A9: the Target of G3 c= the Target of G by A3, Th5;
A10: the Source of G1 tolerates the Source of G2 by A4, A5, PARTFUN1:57;
A11: the Source of G1 tolerates the Source of G3 by A4, A6, PARTFUN1:57;
A12: the Source of G2 tolerates the Source of G3 by A5, A6, PARTFUN1:57;
A13: the Target of G1 tolerates the Target of G2 by A7, A8, PARTFUN1:57;
A14: the Target of G1 tolerates the Target of G3 by A7, A9, PARTFUN1:57;
the Target of G2 tolerates the Target of G3 by A8, A9, PARTFUN1:57;
hence (G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3) by A10, A11, A12, A13, A14, Th9; ::_thesis: verum
end;
theorem :: GRAPH_1:14
for G being Graph holds {} is Chain of G by Lm1;
theorem :: GRAPH_1:15
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 by Lm3;
theorem Th16: :: GRAPH_1:16
for G1, G2 being strict Graph st G1 c= G2 & G2 c= G1 holds
G1 = G2
proof
let G1, G2 be strict Graph; ::_thesis: ( G1 c= G2 & G2 c= G1 implies G1 = G2 )
assume that
A1: G1 c= G2 and
A2: G2 c= G1 ; ::_thesis: G1 = G2
A3: G1 is Subgraph of G2 by A1, Def24;
A4: G2 is Subgraph of G1 by A2, Def24;
A5: the carrier of G1 c= the carrier of G2 by A3, Def18;
the carrier of G2 c= the carrier of G1 by A4, Def18;
then A6: the carrier of G1 = the carrier of G2 by A5, XBOOLE_0:def_10;
A7: the carrier' of G1 c= the carrier' of G2 by A3, Def18;
the carrier' of G2 c= the carrier' of G1 by A4, Def18;
then A8: the carrier' of G1 = the carrier' of G2 by A7, XBOOLE_0:def_10;
then A9: dom the Source of G1 = the carrier' of G2 by FUNCT_2:def_1
.= dom the Source of G2 by FUNCT_2:def_1 ;
for v being set st v in dom the Source of G1 holds
the Source of G1 . v = the Source of G2 . v by A3, Def18;
then A10: the Source of G1 = the Source of G2 by A9, FUNCT_1:2;
A11: dom the Target of G1 = the carrier' of G2 by A8, FUNCT_2:def_1
.= dom the Target of G2 by FUNCT_2:def_1 ;
for v being set st v in dom the Target of G1 holds
the Target of G1 . v = the Target of G2 . v by A3, Def18;
hence G1 = G2 by A6, A8, A10, A11, FUNCT_1:2; ::_thesis: verum
end;
theorem Th17: :: GRAPH_1:17
for G1, G2, G3 being Graph st G1 c= G2 & G2 c= G3 holds
G1 c= G3
proof
let G1, G2, G3 be Graph; ::_thesis: ( G1 c= G2 & G2 c= G3 implies G1 c= G3 )
assume that
A1: G1 c= G2 and
A2: G2 c= G3 ; ::_thesis: G1 c= G3
A3: G1 is Subgraph of G2 by A1, Def24;
A4: G2 is Subgraph of G3 by A2, Def24;
A5: the carrier of G1 c= the carrier of G2 by A3, Def18;
the carrier of G2 c= the carrier of G3 by A4, Def18;
then A6: the carrier of G1 c= the carrier of G3 by A5, XBOOLE_1:1;
A7: the carrier' of G1 c= the carrier' of G2 by A3, Def18;
the carrier' of G2 c= the carrier' of G3 by A4, Def18;
then A8: the carrier' of G1 c= the carrier' of G3 by A7, XBOOLE_1:1;
for v being set st v in the carrier' of G1 holds
( the Source of G1 . v = the Source of G3 . v & the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 )
proof
let v be set ; ::_thesis: ( v in the carrier' of G1 implies ( the Source of G1 . v = the Source of G3 . v & the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 ) )
assume A9: v in the carrier' of G1 ; ::_thesis: ( the Source of G1 . v = the Source of G3 . v & the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 )
hence A10: the Source of G1 . v = the Source of G2 . v by A3, Def18
.= the Source of G3 . v by A4, A7, A9, Def18 ;
::_thesis: ( the Target of G1 . v = the Target of G3 . v & the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 )
thus A11: the Target of G1 . v = the Target of G2 . v by A3, A9, Def18
.= the Target of G3 . v by A4, A7, A9, Def18 ; ::_thesis: ( the Source of G3 . v in the carrier of G1 & the Target of G3 . v in the carrier of G1 )
v in dom the Source of G1 by A9, FUNCT_2:def_1;
then the Source of G1 . v in rng the Source of G1 by FUNCT_1:def_3;
hence the Source of G3 . v in the carrier of G1 by A10; ::_thesis: the Target of G3 . v in the carrier of G1
v in dom the Target of G1 by A9, FUNCT_2:def_1;
then the Target of G1 . v in rng the Target of G1 by FUNCT_1:def_3;
hence the Target of G3 . v in the carrier of G1 by A11; ::_thesis: verum
end;
then G1 is Subgraph of G3 by A6, A8, Def18;
hence G1 c= G3 by Def24; ::_thesis: verum
end;
theorem Th18: :: GRAPH_1:18
for G, G1, G2 being Graph st G is_sum_of G1,G2 holds
( G1 c= G & G2 c= G )
proof
let G, G1, G2 be Graph; ::_thesis: ( G is_sum_of G1,G2 implies ( G1 c= G & G2 c= G ) )
assume A1: G is_sum_of G1,G2 ; ::_thesis: ( G1 c= G & G2 c= G )
A2: for G, G1, G2 being Graph st G is_sum_of G1,G2 holds
G1 c= G
proof
let G, G1, G2 be Graph; ::_thesis: ( G is_sum_of G1,G2 implies G1 c= G )
assume A3: G is_sum_of G1,G2 ; ::_thesis: G1 c= G
then A4: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) by Def6;
A5: MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 by A3, Def6;
then the carrier of G = the carrier of G1 \/ the carrier of G2 by A4, Def5;
then A6: the carrier of G1 c= the carrier of G by XBOOLE_1:7;
the carrier' of G = the carrier' of G1 \/ the carrier' of G2 by A4, A5, Def5;
then A7: the carrier' of G1 c= the carrier' of G by XBOOLE_1:7;
for v being set st v in the carrier' of G1 holds
( the Source of G1 . v = the Source of G . v & the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 )
proof
let v be set ; ::_thesis: ( v in the carrier' of G1 implies ( the Source of G1 . v = the Source of G . v & the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 ) )
assume A8: v in the carrier' of G1 ; ::_thesis: ( the Source of G1 . v = the Source of G . v & the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 )
hence A9: the Source of G1 . v = the Source of G . v by A4, A5, Def5; ::_thesis: ( the Target of G1 . v = the Target of G . v & the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 )
thus A10: the Target of G1 . v = the Target of G . v by A4, A5, A8, Def5; ::_thesis: ( the Source of G . v in the carrier of G1 & the Target of G . v in the carrier of G1 )
thus the Source of G . v in the carrier of G1 by A8, A9, FUNCT_2:5; ::_thesis: the Target of G . v in the carrier of G1
thus the Target of G . v in the carrier of G1 by A8, A10, FUNCT_2:5; ::_thesis: verum
end;
then G1 is Subgraph of G by A6, A7, Def18;
hence G1 c= G by Def24; ::_thesis: verum
end;
hence G1 c= G by A1; ::_thesis: G2 c= G
thus G2 c= G by A1, A2, Th10; ::_thesis: verum
end;
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 )
proof
let G1, G2 be Graph; ::_thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) )
assume ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )
then G1 \/ G2 is_sum_of G1,G2 by Def6;
hence ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) by Th18; ::_thesis: verum
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 )
proof
let G1, G2 be Graph; ::_thesis: ( ex G being Graph st
( G1 c= G & G2 c= G ) implies ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) )
given G being Graph such that A1: ( G1 c= G & G2 c= G ) ; ::_thesis: ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 )
A2: ( the Source of G1 c= the Source of G & the Source of G2 c= the Source of G ) by A1, Th5;
A3: ( the Target of G1 c= the Target of G & the Target of G2 c= the Target of G ) by A1, Th5;
A4: the Source of G1 tolerates the Source of G2 by A2, PARTFUN1:57;
the Target of G1 tolerates the Target of G2 by A3, PARTFUN1:57;
hence ( G1 c= G1 \/ G2 & G2 c= G1 \/ G2 ) by A4, Th19; ::_thesis: verum
end;
theorem Th21: :: GRAPH_1:21
for G1, G3, G2, G being Graph st G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 holds
G c= G3
proof
let G1, G3, G2, G be Graph; ::_thesis: ( G1 c= G3 & G2 c= G3 & G is_sum_of G1,G2 implies G c= G3 )
assume that
A1: G1 c= G3 and
A2: G2 c= G3 and
A3: G is_sum_of G1,G2 ; ::_thesis: G c= G3
A4: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) by A3, Def6;
A5: MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 by A3, Def6;
A6: G1 is Subgraph of G3 by A1, Def24;
A7: G2 is Subgraph of G3 by A2, Def24;
A8: the carrier of G1 c= the carrier of G3 by A6, Def18;
the carrier of G2 c= the carrier of G3 by A7, Def18;
then A9: the carrier of G1 \/ the carrier of G2 c= the carrier of G3 by A8, XBOOLE_1:8;
A10: the carrier' of G1 c= the carrier' of G3 by A6, Def18;
the carrier' of G2 c= the carrier' of G3 by A7, Def18;
then A11: the carrier' of G1 \/ the carrier' of G2 c= the carrier' of G3 by A10, XBOOLE_1:8;
for v being set st v in the carrier' of (G1 \/ G2) holds
( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) )
proof
let v be set ; ::_thesis: ( v in the carrier' of (G1 \/ G2) implies ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) ) )
assume A12: v in the carrier' of (G1 \/ G2) ; ::_thesis: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v & the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) )
thus A13: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) ::_thesis: ( the Source of G3 . v in the carrier of (G1 \/ G2) & the Target of G3 . v in the carrier of (G1 \/ G2) )
proof
A14: v in the carrier' of G1 \/ the carrier' of G2 by A4, A12, Def5;
A15: now__::_thesis:_(_v_in_the_carrier'_of_G1_implies_(_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_G3_._v_&_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_G3_._v_)_)
assume A16: v in the carrier' of G1 ; ::_thesis: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v )
then A17: the Source of G3 . v = the Source of G1 . v by A6, Def18
.= the Source of (G1 \/ G2) . v by A4, A16, Def5 ;
the Target of G3 . v = the Target of G1 . v by A6, A16, Def18
.= the Target of (G1 \/ G2) . v by A4, A16, Def5 ;
hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A17; ::_thesis: verum
end;
now__::_thesis:_(_v_in_the_carrier'_of_G2_implies_(_the_Source_of_(G1_\/_G2)_._v_=_the_Source_of_G3_._v_&_the_Target_of_(G1_\/_G2)_._v_=_the_Target_of_G3_._v_)_)
assume A18: v in the carrier' of G2 ; ::_thesis: ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v )
then A19: the Source of G3 . v = the Source of G2 . v by A7, Def18
.= the Source of (G1 \/ G2) . v by A4, A18, Def5 ;
the Target of G3 . v = the Target of G2 . v by A7, A18, Def18
.= the Target of (G1 \/ G2) . v by A4, A18, Def5 ;
hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A19; ::_thesis: verum
end;
hence ( the Source of (G1 \/ G2) . v = the Source of G3 . v & the Target of (G1 \/ G2) . v = the Target of G3 . v ) by A14, A15, XBOOLE_0:def_3; ::_thesis: verum
end;
hence the Source of G3 . v in the carrier of (G1 \/ G2) by A12, FUNCT_2:5; ::_thesis: the Target of G3 . v in the carrier of (G1 \/ G2)
thus the Target of G3 . v in the carrier of (G1 \/ G2) by A12, A13, FUNCT_2:5; ::_thesis: verum
end;
hence ( the carrier of G c= the carrier of G3 & the carrier' of G c= the carrier' of G3 & ( for v being set st v in the carrier' of G holds
( the Source of G . v = the Source of G3 . v & the Target of G . v = the Target of G3 . v & the Source of G3 . v in the carrier of G & the Target of G3 . v in the carrier of G ) ) ) by A4, A5, A9, A11, Def5; :: according to GRAPH_1:def_18,GRAPH_1:def_24 ::_thesis: verum
end;
theorem Th22: :: GRAPH_1:22
for G1, G, G2 being Graph st G1 c= G & G2 c= G holds
G1 \/ G2 c= G
proof
let G1, G, G2 be Graph; ::_thesis: ( G1 c= G & G2 c= G implies G1 \/ G2 c= G )
assume A1: ( G1 c= G & G2 c= G ) ; ::_thesis: G1 \/ G2 c= G
then A2: ( the Source of G1 c= the Source of G & the Source of G2 c= the Source of G ) by Th5;
A3: ( the Target of G1 c= the Target of G & the Target of G2 c= the Target of G ) by A1, Th5;
A4: the Source of G1 tolerates the Source of G2 by A2, PARTFUN1:57;
the Target of G1 tolerates the Target of G2 by A3, PARTFUN1:57;
then G1 \/ G2 is_sum_of G1,G2 by A4, Def6;
hence G1 \/ G2 c= G by A1, Th21; ::_thesis: verum
end;
theorem :: GRAPH_1:23
for G1, G2 being strict Graph st G1 c= G2 holds
( G1 \/ G2 = G2 & G2 \/ G1 = G2 )
proof
let G1, G2 be strict Graph; ::_thesis: ( G1 c= G2 implies ( G1 \/ G2 = G2 & G2 \/ G1 = G2 ) )
assume A1: G1 c= G2 ; ::_thesis: ( G1 \/ G2 = G2 & G2 \/ G1 = G2 )
then ( G1 \/ G2 c= G2 & G2 c= G1 \/ G2 ) by Th20, Th22;
hence G1 \/ G2 = G2 by Th16; ::_thesis: G2 \/ G1 = G2
hence G2 \/ G1 = G2 by A1, Th12; ::_thesis: verum
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
proof
let G1, G2 be Graph; ::_thesis: ( 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 ) implies G1 c= G2 )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: ( ( not G1 \/ G2 = G2 & not G2 \/ G1 = G2 ) or G1 c= G2 )
assume A2: ( G1 \/ G2 = G2 or G2 \/ G1 = G2 ) ; ::_thesis: G1 c= G2
then the carrier of G2 = the carrier of G1 \/ the carrier of G2 by A1, Def5;
then A3: the carrier of G1 c= the carrier of G2 by XBOOLE_1:7;
the carrier' of G2 = the carrier' of G1 \/ the carrier' of G2 by A1, A2, Def5;
then A4: the carrier' of G1 c= the carrier' of G2 by XBOOLE_1:7;
for v being set st v in the carrier' of G1 holds
( the Source of G1 . v = the Source of G2 . v & the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 )
proof
let v be set ; ::_thesis: ( v in the carrier' of G1 implies ( the Source of G1 . v = the Source of G2 . v & the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 ) )
assume A5: v in the carrier' of G1 ; ::_thesis: ( the Source of G1 . v = the Source of G2 . v & the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 )
hence A6: the Source of G1 . v = the Source of G2 . v by A1, A2, Def5; ::_thesis: ( the Target of G1 . v = the Target of G2 . v & the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 )
thus A7: the Target of G1 . v = the Target of G2 . v by A1, A2, A5, Def5; ::_thesis: ( the Source of G2 . v in the carrier of G1 & the Target of G2 . v in the carrier of G1 )
thus the Source of G2 . v in the carrier of G1 by A5, A6, FUNCT_2:5; ::_thesis: the Target of G2 . v in the carrier of G1
thus the Target of G2 . v in the carrier of G1 by A5, A7, FUNCT_2:5; ::_thesis: verum
end;
then G1 is Subgraph of G2 by A3, A4, Def18;
hence G1 c= G2 by Def24; ::_thesis: verum
end;
theorem :: GRAPH_1:25
for G1 being Graph
for G being oriented Graph st G1 c= G holds
G1 is oriented
proof
let G1 be Graph; ::_thesis: for G being oriented Graph st G1 c= G holds
G1 is oriented
let G be oriented Graph; ::_thesis: ( G1 c= G implies G1 is oriented )
assume G1 c= G ; ::_thesis: G1 is oriented
then A1: G1 is Subgraph of G by Def24;
for x, y being set st x in the carrier' of G1 & y in the carrier' of G1 & the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y holds
x = y
proof
let x, y be set ; ::_thesis: ( x in the carrier' of G1 & y in the carrier' of G1 & the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y implies x = y )
assume that
A2: x in the carrier' of G1 and
A3: y in the carrier' of G1 and
A4: the Source of G1 . x = the Source of G1 . y and
A5: the Target of G1 . x = the Target of G1 . y ; ::_thesis: x = y
A6: the carrier' of G1 c= the carrier' of G by A1, Def18;
A7: the Source of G . x = the Source of G1 . y by A1, A2, A4, Def18
.= the Source of G . y by A1, A3, Def18 ;
the Target of G . x = the Target of G1 . y by A1, A2, A5, Def18
.= the Target of G . y by A1, A3, Def18 ;
hence x = y by A2, A3, A6, A7, Def7; ::_thesis: verum
end;
hence G1 is oriented by Def7; ::_thesis: verum
end;
theorem :: GRAPH_1:26
for G1 being Graph
for G being non-multi Graph st G1 c= G holds
G1 is non-multi
proof
let G1 be Graph; ::_thesis: for G being non-multi Graph st G1 c= G holds
G1 is non-multi
let G be non-multi Graph; ::_thesis: ( G1 c= G implies G1 is non-multi )
assume G1 c= G ; ::_thesis: G1 is non-multi
then A1: G1 is Subgraph of G by Def24;
for x, y being set st x in the carrier' of G1 & y in the carrier' of G1 & ( ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) or ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) holds
x = y
proof
let x, y be set ; ::_thesis: ( x in the carrier' of G1 & y in the carrier' of G1 & ( ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) or ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) implies x = y )
assume A2: ( x in the carrier' of G1 & y in the carrier' of G1 ) ; ::_thesis: ( ( not ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) & not ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) or x = y )
assume A3: ( ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) or ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) ; ::_thesis: x = y
A4: the carrier' of G1 c= the carrier' of G by A1, Def18;
A5: ( the Source of G1 . x = the Source of G . x & the Source of G1 . y = the Source of G . y ) by A1, A2, Def18;
( the Target of G1 . x = the Target of G . x & the Target of G1 . y = the Target of G . y ) by A1, A2, Def18;
hence x = y by A2, A3, A4, A5, Def8; ::_thesis: verum
end;
hence G1 is non-multi by Def8; ::_thesis: verum
end;
theorem :: GRAPH_1:27
for G1 being Graph
for G being simple Graph st G1 c= G holds
G1 is simple
proof
let G1 be Graph; ::_thesis: for G being simple Graph st G1 c= G holds
G1 is simple
let G be simple Graph; ::_thesis: ( G1 c= G implies G1 is simple )
assume G1 c= G ; ::_thesis: G1 is simple
then A1: G1 is Subgraph of G by Def24;
for x being set holds
( not x in the carrier' of G1 or not the Source of G1 . x = the Target of G1 . x )
proof
given x being set such that A2: x in the carrier' of G1 and
A3: the Source of G1 . x = the Target of G1 . x ; ::_thesis: contradiction
A4: the carrier' of G1 c= the carrier' of G by A1, Def18;
the Source of G . x = the Target of G1 . x by A1, A2, A3, Def18
.= the Target of G . x by A1, A2, Def18 ;
hence contradiction by A2, A4, Def9; ::_thesis: verum
end;
hence G1 is simple by Def9; ::_thesis: verum
end;
theorem :: GRAPH_1:28
for G being Graph
for G1 being strict Graph holds
( G1 in bool G iff G1 c= G )
proof
let G be Graph; ::_thesis: for G1 being strict Graph holds
( G1 in bool G iff G1 c= G )
let G1 be strict Graph; ::_thesis: ( G1 in bool G iff G1 c= G )
thus ( G1 in bool G implies G1 c= G ) ::_thesis: ( G1 c= G implies G1 in bool G )
proof
assume G1 in bool G ; ::_thesis: G1 c= G
then G1 is Subgraph of G by Def25;
hence G1 c= G by Def24; ::_thesis: verum
end;
assume G1 c= G ; ::_thesis: G1 in bool G
then G1 is Subgraph of G by Def24;
hence G1 in bool G by Def25; ::_thesis: verum
end;
theorem Th29: :: GRAPH_1:29
for G being strict Graph holds G in bool G
proof
let G be strict Graph; ::_thesis: G in bool G
G is Subgraph of G by Def24;
hence G in bool G by Def25; ::_thesis: verum
end;
theorem :: GRAPH_1:30
for G2 being Graph
for G1 being strict Graph holds
( G1 c= G2 iff bool G1 c= bool G2 )
proof
let G2 be Graph; ::_thesis: for G1 being strict Graph holds
( G1 c= G2 iff bool G1 c= bool G2 )
let G1 be strict Graph; ::_thesis: ( G1 c= G2 iff bool G1 c= bool G2 )
thus ( G1 c= G2 implies bool G1 c= bool G2 ) ::_thesis: ( bool G1 c= bool G2 implies G1 c= G2 )
proof
assume A1: G1 c= G2 ; ::_thesis: bool G1 c= bool G2
for x being set st x in bool G1 holds
x in bool G2
proof
let x be set ; ::_thesis: ( x in bool G1 implies x in bool G2 )
assume x in bool G1 ; ::_thesis: x in bool G2
then reconsider G = x as strict Subgraph of G1 by Def25;
G c= G1 by Def24;
then G c= G2 by A1, Th17;
then G is strict Subgraph of G2 by Def24;
hence x in bool G2 by Def25; ::_thesis: verum
end;
hence bool G1 c= bool G2 by TARSKI:def_3; ::_thesis: verum
end;
assume A2: bool G1 c= bool G2 ; ::_thesis: G1 c= G2
G1 in bool G1 by Th29;
then G1 is Subgraph of G2 by A2, Def25;
hence G1 c= G2 by Def24; ::_thesis: verum
end;
theorem :: GRAPH_1:31
for G being strict Graph holds {G} c= bool G
proof
let G be strict Graph; ::_thesis: {G} c= bool G
G in bool G by Th29;
hence {G} c= bool G by ZFMISC_1:31; ::_thesis: verum
end;
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
proof
let G1, G2 be strict Graph; ::_thesis: ( 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 implies G2 c= G1 )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: ( not bool (G1 \/ G2) c= (bool G1) \/ (bool G2) or G1 c= G2 or G2 c= G1 )
assume A2: bool (G1 \/ G2) c= (bool G1) \/ (bool G2) ; ::_thesis: ( G1 c= G2 or G2 c= G1 )
A3: G1 \/ G2 in bool (G1 \/ G2) by Th29;
A4: now__::_thesis:_(_G1_\/_G2_in_bool_G1_implies_G2_c=_G1_)
assume G1 \/ G2 in bool G1 ; ::_thesis: G2 c= G1
then G1 \/ G2 is Subgraph of G1 by Def25;
then A5: G1 \/ G2 c= G1 by Def24;
G1 c= G1 \/ G2 by A1, Th19;
then G1 \/ G2 = G1 by A5, Th16;
hence G2 c= G1 by A1, Th24; ::_thesis: verum
end;
now__::_thesis:_(_G1_\/_G2_in_bool_G2_implies_G1_c=_G2_)
assume G1 \/ G2 in bool G2 ; ::_thesis: G1 c= G2
then G1 \/ G2 is Subgraph of G2 by Def25;
then A6: G1 \/ G2 c= G2 by Def24;
G2 c= G1 \/ G2 by A1, Th19;
then G1 \/ G2 = G2 by A6, Th16;
hence G1 c= G2 by A1, Th24; ::_thesis: verum
end;
hence ( G1 c= G2 or G2 c= G1 ) by A2, A3, A4, XBOOLE_0:def_3; ::_thesis: verum
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)
proof
let G1, G2 be Graph; ::_thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies (bool G1) \/ (bool G2) c= bool (G1 \/ G2) )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; ::_thesis: (bool G1) \/ (bool G2) c= bool (G1 \/ G2)
A2: for v being set st v in bool G1 holds
v in bool (G1 \/ G2)
proof
let v be set ; ::_thesis: ( v in bool G1 implies v in bool (G1 \/ G2) )
assume v in bool G1 ; ::_thesis: v in bool (G1 \/ G2)
then reconsider G = v as strict Subgraph of G1 by Def25;
( G c= G1 & G1 c= G1 \/ G2 ) by A1, Def24, Th19;
then G c= G1 \/ G2 by Th17;
then G is strict Subgraph of G1 \/ G2 by Def24;
hence v in bool (G1 \/ G2) by Def25; ::_thesis: verum
end;
A3: for v being set st v in bool G2 holds
v in bool (G1 \/ G2)
proof
let v be set ; ::_thesis: ( v in bool G2 implies v in bool (G1 \/ G2) )
assume v in bool G2 ; ::_thesis: v in bool (G1 \/ G2)
then reconsider G = v as strict Subgraph of G2 by Def25;
( G c= G2 & G2 c= G1 \/ G2 ) by A1, Def24, Th19;
then G c= G1 \/ G2 by Th17;
then G is strict Subgraph of G1 \/ G2 by Def24;
hence v in bool (G1 \/ G2) by Def25; ::_thesis: verum
end;
for v being set st v in (bool G1) \/ (bool G2) holds
v in bool (G1 \/ G2)
proof
let v be set ; ::_thesis: ( v in (bool G1) \/ (bool G2) implies v in bool (G1 \/ G2) )
assume v in (bool G1) \/ (bool G2) ; ::_thesis: v in bool (G1 \/ G2)
then ( v in bool G1 or v in bool G2 ) by XBOOLE_0:def_3;
hence v in bool (G1 \/ G2) by A2, A3; ::_thesis: verum
end;
hence (bool G1) \/ (bool G2) c= bool (G1 \/ G2) by TARSKI:def_3; ::_thesis: verum
end;
theorem :: GRAPH_1:34
for G1, G, G2 being Graph st G1 in bool G & G2 in bool G holds
G1 \/ G2 in bool G
proof
let G1, G, G2 be Graph; ::_thesis: ( G1 in bool G & G2 in bool G implies G1 \/ G2 in bool G )
assume that
A1: G1 in bool G and
A2: G2 in bool G ; ::_thesis: G1 \/ G2 in bool G
A3: G1 is Subgraph of G by A1, Def25;
A4: G2 is Subgraph of G by A2, Def25;
A5: G1 c= G by A3, Def24;
G2 c= G by A4, Def24;
then G1 \/ G2 c= G by A5, Th22;
then G1 \/ G2 is Subgraph of G by Def24;
hence G1 \/ G2 in bool G by Def25; ::_thesis: verum
end;