graph_1.miz
begin
reserve x,y,z,v for
set,
n,m,k for
Nat;
definition
struct (
2-sorted)
MultiGraphStruct
(# the
carrier,
carrier' ->
set,
the
Source,
Target ->
Function of the carrier', the carrier #)
attr strict
strict;
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
strict non
empty non
void for
MultiGraphStruct;
existence
proof
MultiGraphStruct (#
{
0 },
{
0 },
op1 ,
op1 #) is non
empty non
void;
hence thesis;
end;
end
definition
mode
Graph is non
empty
MultiGraphStruct;
end
reserve G,G1,G2,G3 for
Graph;
definition
let C be
MultiGraphStruct, f be
Edge of C;
::
GRAPH_1:def1
func
dom f ->
Vertex of C equals
:
Def1: (the
Source of C
. f) if C is non
void non
empty
otherwise the
Vertex of C;
coherence
proof
thus C is non
void non
empty implies (the
Source of C
. f) is
Vertex of C
proof
assume C is non
void non
empty;
then
reconsider C as non
void non
empty
MultiGraphStruct;
reconsider f as
Edge of C;
(the
Source of C
. f) is
Vertex of C;
hence thesis;
end;
thus thesis;
end;
consistency ;
::
GRAPH_1:def2
func
cod f ->
Vertex of C equals
:
Def2: (the
Target of C
. f) if C is non
void non
empty
otherwise the
Vertex of C;
correctness
proof
thus C is non
void non
empty implies (the
Target of C
. f) is
Vertex of C
proof
assume C is non
void non
empty;
then
reconsider C as non
void non
empty
MultiGraphStruct;
reconsider f as
Edge of C;
(the
Target of C
. f) is
Vertex of C;
hence thesis;
end;
thus thesis;
end;
end
definition
let C be non
void non
empty
MultiGraphStruct, f be
Edge of C;
:: original:
dom
redefine
::
GRAPH_1:def3
func
dom f ->
Vertex of C equals (the
Source of C
. f);
compatibility by
Def1;
coherence ;
:: original:
cod
redefine
::
GRAPH_1:def4
func
cod f ->
Vertex of C equals (the
Target of C
. f);
compatibility by
Def2;
coherence ;
end
definition
let G1, G2;
assume that
A1: the
Source of G1
tolerates the
Source of G2 and
A2: the
Target of G1
tolerates the
Target of G2;
::
GRAPH_1:def5
func G1
\/ G2 ->
strict
Graph means
:
Def5: 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 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 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
proof
set V = (the
carrier of G1
\/ the
carrier of G2);
set E = (the
carrier' of G1
\/ the
carrier' of G2);
ex S be
Function of E, V st (for v st v
in the
carrier' of G1 holds (S
. v)
= (the
Source of G1
. v)) & for v st v
in the
carrier' of G2 holds (S
. v)
= (the
Source of G2
. v)
proof
defpred
P[
object,
object] 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 be
object st x
in E holds ex y be
object st y
in V &
P[x, y]
proof
let x be
object;
assume
A4: x
in E;
A5: x
in the
carrier' of G1 implies thesis
proof
assume
A6: x
in the
carrier' of G1;
take y = (the
Source of G1
. x) qua
set;
y
in the
carrier of G1 by
A6,
FUNCT_2: 5;
hence y
in V by
XBOOLE_0:def 3;
thus x
in the
carrier' of G1 implies y
= (the
Source of G1
. x);
assume x
in the
carrier' of G2;
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;
end;
not x
in the
carrier' of G1 implies thesis
proof
assume
A8: not x
in the
carrier' of G1;
then
A9: x
in the
carrier' of G2 by
A4,
XBOOLE_0:def 3;
take y = (the
Source of G2
. x) qua
set;
y
in the
carrier of G2 by
A9,
FUNCT_2: 5;
hence y
in V by
XBOOLE_0:def 3;
thus thesis by
A8;
end;
hence thesis by
A5;
end;
consider S be
Function of E, V such that
A10: for x be
object st x
in E holds
P[x, (S
. x)] from
FUNCT_2:sch 1(
A3);
take S;
thus for v st v
in the
carrier' of G1 holds (S
. v)
= (the
Source of G1
. v)
proof
let v;
assume
A11: v
in the
carrier' of G1;
then v
in E by
XBOOLE_0:def 3;
hence thesis by
A10,
A11;
end;
let v;
assume
A12: v
in the
carrier' of G2;
then v
in E by
XBOOLE_0:def 3;
hence thesis by
A10,
A12;
end;
then
consider S be
Function of E, V such that
A13: for v st v
in the
carrier' of G1 holds (S
. v)
= (the
Source of G1
. v) and
A14: for v st v
in the
carrier' of G2 holds (S
. v)
= (the
Source of G2
. v);
ex T be
Function of E, V st (for v st v
in the
carrier' of G1 holds (T
. v)
= (the
Target of G1
. v)) & for v st v
in the
carrier' of G2 holds (T
. v)
= (the
Target of G2
. v)
proof
defpred
P[
object,
object] 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 be
object st x
in E holds ex y be
object st y
in V &
P[x, y]
proof
let x be
object;
assume
A16: x
in E;
A17: x
in the
carrier' of G1 implies thesis
proof
assume
A18: x
in the
carrier' of G1;
take y = (the
Target of G1
. x) qua
set;
y
in the
carrier of G1 by
A18,
FUNCT_2: 5;
hence y
in V by
XBOOLE_0:def 3;
thus x
in the
carrier' of G1 implies y
= (the
Target of G1
. x);
assume x
in the
carrier' of G2;
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;
end;
not x
in the
carrier' of G1 implies thesis
proof
assume
A20: not x
in the
carrier' of G1;
then
A21: x
in the
carrier' of G2 by
A16,
XBOOLE_0:def 3;
take y = (the
Target of G2
. x) qua
set;
y
in the
carrier of G2 by
A21,
FUNCT_2: 5;
hence y
in V by
XBOOLE_0:def 3;
thus thesis by
A20;
end;
hence thesis by
A17;
end;
consider S be
Function of E, V such that
A22: for x be
object st x
in E holds
P[x, (S
. x)] from
FUNCT_2:sch 1(
A15);
take S;
thus for v st v
in the
carrier' of G1 holds (S
. v)
= (the
Target of G1
. v)
proof
let v;
assume
A23: v
in the
carrier' of G1;
then v
in E by
XBOOLE_0:def 3;
hence thesis by
A22,
A23;
end;
let v;
assume
A24: v
in the
carrier' of G2;
then v
in E by
XBOOLE_0:def 3;
hence thesis by
A22,
A24;
end;
then
consider T be
Function of E, V such that
A25: for v st v
in the
carrier' of G1 holds (T
. v)
= (the
Target of G1
. v) and
A26: for v st v
in the
carrier' of G2 holds (T
. v)
= (the
Target of G2
. v);
reconsider G =
MultiGraphStruct (# V, E, S, T #) as
strict
Graph;
take G;
thus the
carrier of G
= V;
thus the
carrier' of G
= E;
thus for v 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;
let v;
assume
A27: v
in the
carrier' of G2;
hence (the
Source of G
. v)
= (the
Source of G2
. v) by
A14;
thus thesis by
A26,
A27;
end;
uniqueness
proof
let G,G9 be
strict
Graph such 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 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 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 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 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);
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 be
object st x
in the
carrier' of G holds (the
Source of G
. x)
= (the
Source of G9
. x)
proof
let x be
object such that
A38: x
in the
carrier' of G;
A39:
now
assume
A40: x
in the
carrier' of G1;
hence (the
Source of G
. x)
= (the
Source of G1
. x) by
A30
.= (the
Source of G9
. x) by
A34,
A40;
end;
now
assume
A41: x
in the
carrier' of G2;
hence (the
Source of G
. x)
= (the
Source of G2
. x) by
A31
.= (the
Source of G9
. x) by
A35,
A41;
end;
hence thesis by
A29,
A38,
A39,
XBOOLE_0:def 3;
end;
then
A42: the
Source of G
= the
Source of G9 by
A36;
for x be
object st x
in the
carrier' of G holds (the
Target of G
. x)
= (the
Target of G9
. x)
proof
let x be
object such that
A43: x
in the
carrier' of G;
A44:
now
assume
A45: x
in the
carrier' of G1;
hence (the
Target of G
. x)
= (the
Target of G1
. x) by
A30
.= (the
Target of G9
. x) by
A34,
A45;
end;
now
assume
A46: x
in the
carrier' of G2;
hence (the
Target of G
. x)
= (the
Target of G2
. x) by
A31
.= (the
Target of G9
. x) by
A35,
A46;
end;
hence thesis by
A29,
A43,
A44,
XBOOLE_0:def 3;
end;
hence thesis by
A28,
A29,
A32,
A33,
A37,
A42,
FUNCT_1: 2;
end;
end
definition
let G,G1,G2 be
Graph;
::
GRAPH_1:def6
pred G
is_sum_of G1,G2 means the
Target of G1
tolerates the
Target of G2 & the
Source of G1
tolerates the
Source of G2 & the MultiGraphStruct of G
= (G1
\/ G2);
end
definition
let IT be
Graph;
::
GRAPH_1:def7
attr IT is
oriented means
:
Def7: for x, y 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;
::
GRAPH_1:def8
attr IT is
non-multi means
:
Def8: for x, y 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;
::
GRAPH_1:def9
attr IT is
simple means
:
Def9: not ex x st x
in the
carrier' of IT & (the
Source of IT
. x)
= (the
Target of IT
. x);
::
GRAPH_1:def10
attr IT is
connected means not ex G1,G2 be
Graph st the
carrier of G1
misses the
carrier of G2 & IT
is_sum_of (G1,G2);
end
definition
let IT be
MultiGraphStruct;
::
GRAPH_1:def11
attr IT is
finite means
:
Def11: the
carrier of IT is
finite & the
carrier' of IT is
finite;
end
registration
cluster
finite for
MultiGraphStruct;
existence
proof
take G =
MultiGraphStruct (#
{
0 },
{
0 },
op1 ,
op1 #);
thus the
carrier of G is
finite;
thus thesis;
end;
cluster
finite
non-multi
oriented
simple
connected for
Graph;
existence
proof
set V =
{1};
reconsider empty1 =
{} as
Function of
{} , V by
RELSET_1: 12;
reconsider G =
MultiGraphStruct (# V,
{} , empty1, empty1 #) as
Graph;
take G;
thus G is
finite;
thus G is
non-multi;
thus G is
oriented;
thus G is
simple;
not ex G1,G2 be
Graph st the
carrier of G1
misses the
carrier of G2 & G
is_sum_of (G1,G2)
proof
given G1,G2 be
Graph such that
A1: the
carrier of G1
misses the
carrier of G2 and
A2: G
is_sum_of (G1,G2);
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;
G
= (G1
\/ G2) by
A2;
then
A5: (the
carrier of G1
\/ the
carrier of G2)
= V by
A4,
Def5;
set x = the
Vertex of G1;
x
in the
carrier of G1 & x
in V by
A5,
XBOOLE_0:def 3;
then
A6: 1
in the
carrier of G1 by
TARSKI:def 1;
set y = the
Vertex of G2;
y
in the
carrier of G2 & y
in V 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;
end;
hence thesis;
end;
end
registration
let G be
finite
MultiGraphStruct;
cluster the
carrier of G ->
finite;
coherence by
Def11;
cluster the
carrier' of G ->
finite;
coherence by
Def11;
end
reserve x,y for
Element of the
carrier of G;
definition
let G;
let x, y;
let v;
::
GRAPH_1:def12
pred v
joins x,y means (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
definition
let G;
let x,y be
Element of the
carrier of G;
::
GRAPH_1:def13
pred x,y
are_incident means ex v be
set st v
in the
carrier' of G & v
joins (x,y);
end
definition
let G be
Graph;
::
GRAPH_1:def14
mode
Chain of G ->
FinSequence means
:
Def14: (for n st 1
<= n & n
<= (
len it ) holds (it
. n)
in the
carrier' of G) & ex p be
FinSequence st (
len p)
= ((
len it )
+ 1) & (for n st 1
<= n & n
<= (
len p) holds (p
. n)
in the
carrier of G) & for n st 1
<= n & n
<= (
len it ) holds ex x9,y9 be
Vertex of G st x9
= (p
. n) & y9
= (p
. (n
+ 1)) & (it
. n)
joins (x9,y9);
existence
proof
take
{} ;
thus for n st 1
<= n & n
<= (
len
{} ) holds (
{}
. n)
in the
carrier' of G;
set x = the
Vertex of G;
A1: x
in the
carrier of G;
take
<*x*>;
thus (
len
<*x*>)
= ((
len
{} )
+ 1) by
FINSEQ_1: 39;
thus for n st 1
<= n & n
<= (
len
<*x*>) holds (
<*x*>
. n)
in the
carrier of G
proof
let n;
assume that
A2: 1
<= n and
A3: n
<= (
len
<*x*>);
n
<= 1 by
A3,
FINSEQ_1: 39;
then n
= 1 by
A2,
XXREAL_0: 1;
hence thesis by
A1,
FINSEQ_1: 40;
end;
let n;
thus thesis;
end;
end
Lm1: for G holds
{} is
Chain of G
proof
let G;
thus for n st 1
<= n & n
<= (
len
{} ) holds (
{}
. n)
in the
carrier' of G;
set x = the
Vertex of G;
A1: x
in the
carrier of G;
take
<*x*>;
thus (
len
<*x*>)
= ((
len
{} )
+ 1) by
FINSEQ_1: 39;
thus for n st 1
<= n & n
<= (
len
<*x*>) holds (
<*x*>
. n)
in the
carrier of G
proof
let n;
assume that
A2: 1
<= n and
A3: n
<= (
len
<*x*>);
n
<= 1 by
A3,
FINSEQ_1: 39;
then n
= 1 by
A2,
XXREAL_0: 1;
hence thesis by
A1,
FINSEQ_1: 40;
end;
let n;
thus thesis;
end;
definition
let G be
Graph;
:: original:
Chain
redefine
mode
Chain of G ->
FinSequence of the
carrier' of G ;
coherence
proof
let c be
Chain of G;
(
rng c)
c= the
carrier' of G
proof
let y be
object;
assume y
in (
rng c);
then
consider x be
object such that
A1: x
in (
dom c) and
A2: y
= (c
. x) by
FUNCT_1:def 3;
reconsider x as
Element of
NAT by
A1;
1
<= x & x
<= (
len c) by
A1,
FINSEQ_3: 25;
hence thesis by
A2,
Def14;
end;
hence thesis by
FINSEQ_1:def 4;
end;
end
definition
let G be
Graph;
let IT be
Chain of G;
::
GRAPH_1:def15
attr IT is
oriented means for n st 1
<= n & n
< (
len IT) holds (the
Source of G
. (IT
. (n
+ 1)))
= (the
Target of G
. (IT
. n));
end
registration
let G be
Graph;
cluster
empty for
Chain of G;
existence
proof
{} is
Chain of G by
Lm1;
hence thesis;
end;
end
registration
let G be
Graph;
cluster
empty ->
oriented for
Chain of G;
coherence ;
end
definition
let G be
Graph;
let IT be
Chain of G;
:: original:
one-to-one
redefine
::
GRAPH_1:def16
attr IT is
one-to-one means for n, m st 1
<= n & n
< m & m
<= (
len IT) holds (IT
. n)
<> (IT
. m);
compatibility
proof
thus IT is
one-to-one implies for n, m st 1
<= n & n
< m & m
<= (
len IT) holds (IT
. n)
<> (IT
. m)
proof
assume
A1: IT is
one-to-one;
let n, m;
assume that
A2: 1
<= n and
A3: n
< m and
A4: m
<= (
len IT);
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 thesis by
A1,
A3,
A7;
end;
assume
A8: for n, m st 1
<= n & n
< m & m
<= (
len IT) holds (IT
. n)
<> (IT
. m);
let x1,x2 be
object;
assume that
A9: x1
in (
dom IT) & x2
in (
dom IT) and
A10: (IT
. x1)
= (IT
. 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;
per cases ;
suppose
A13: x9
<> y9;
now
per cases by
A13,
XXREAL_0: 1;
suppose x9
< y9;
hence thesis by
A8,
A10,
A12;
end;
suppose y9
< x9;
hence thesis by
A8,
A10,
A11;
end;
end;
hence thesis;
end;
suppose x9
= y9;
hence thesis;
end;
end;
end
definition
let G be
Graph;
mode
Path of G is
one-to-one
Chain of G;
end
definition
let G be
Graph;
mode
OrientedPath of G is
one-to-one
oriented
Chain of G;
end
definition
let G be
Graph;
let IT be
Path of G;
::
GRAPH_1:def17
attr IT is
cyclic means ex p be
FinSequence st (
len p)
= ((
len IT)
+ 1) & (for n st 1
<= n & n
<= (
len p) holds (p
. n)
in the
carrier of G) & (for n st 1
<= n & n
<= (
len IT) holds ex x9,y9 be
Vertex of G st x9
= (p
. n) & y9
= (p
. (n
+ 1)) & (IT
. n)
joins (x9,y9)) & (p
. 1)
= (p
. (
len p));
end
registration
let G be
Graph;
cluster
empty ->
cyclic for
Path of G;
coherence
proof
let p be
Path of G;
assume
A1: p is
empty;
set x = the
Vertex of G;
A2: x
in the
carrier of G;
take
<*x*>;
thus (
len
<*x*>)
= ((
len p)
+ 1) by
A1,
FINSEQ_1: 39;
thus for n st 1
<= n & n
<= (
len
<*x*>) holds (
<*x*>
. n)
in the
carrier of G
proof
let n;
assume that
A3: 1
<= n and
A4: n
<= (
len
<*x*>);
n
<= 1 by
A4,
FINSEQ_1: 39;
then n
= 1 by
A3,
XXREAL_0: 1;
hence thesis by
A2,
FINSEQ_1: 40;
end;
thus for n st 1
<= n & n
<= (
len p) holds ex x9,y9 be
Vertex of G st x9
= (
<*x*>
. n) & y9
= (
<*x*>
. (n
+ 1)) & (p
. n)
joins (x9,y9) by
A1;
thus thesis by
FINSEQ_1: 39;
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;
::
GRAPH_1:def18
mode
Subgraph of G ->
Graph means
:
Def18: the
carrier of it
c= the
carrier of G & the
carrier' of it
c= the
carrier' of G & for v 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
proof
take G;
thus the
carrier of G
c= the
carrier of G;
thus the
carrier' of G
c= the
carrier' of G;
let v;
assume v
in the
carrier' of G;
hence thesis by
FUNCT_2: 5;
end;
end
registration
let G be
Graph;
cluster
strict for
Subgraph of G;
existence
proof
reconsider S =
MultiGraphStruct (# the
carrier of G, the
carrier' of G, the
Source of G, the
Target of G #) as
Graph;
for v 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 thesis;
end;
end
definition
let G be
finite
Graph;
::
GRAPH_1:def19
func
VerticesCount G ->
Element of
NAT means ex B be
finite
set st B
= the
carrier of G & it
= (
card B);
existence
proof
set B = the
carrier of G;
take (
card B), B;
thus thesis;
end;
uniqueness ;
::
GRAPH_1:def20
func
EdgesCount G ->
Element of
NAT means ex B be
finite
set st B
= the
carrier' of G & it
= (
card B);
existence
proof
set B = the
carrier' of G;
take (
card B), B;
thus thesis;
end;
uniqueness ;
end
definition
let G be
finite
Graph;
let x be
Vertex of G;
::
GRAPH_1:def21
func
EdgesIn x ->
Element of
NAT means ex X be
finite
set st (for z be
set holds z
in X iff z
in the
carrier' of G & (the
Target of G
. z)
= x) & it
= (
card X);
existence
proof
defpred
P[
object] means (the
Target of G
. $1)
= x;
consider X be
set such that
A1: for z be
object holds z
in X iff z
in the
carrier' of G &
P[z] from
XBOOLE_0:sch 1;
for z be
object st z
in X holds z
in the
carrier' of G by
A1;
then X
c= the
carrier' of G;
then
reconsider X as
finite
set;
take (
card X);
take X;
thus thesis by
A1;
end;
uniqueness
proof
let n1,n2 be
Element of
NAT such that
A2: ex X be
finite
set st (for z be
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 be
finite
set st (for z be
set holds z
in X iff z
in the
carrier' of G & (the
Target of G
. z)
= x) & n2
= (
card X);
consider X1 be
finite
set such that
A4: for z be
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 be
finite
set such that
A6: for z be
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 be
object holds z
in X1 iff z
in X2
proof
let z be
object;
z
in X1 iff z
in the
carrier' of G & (the
Target of G
. z)
= x by
A4;
hence thesis by
A6;
end;
hence thesis by
A5,
A7,
TARSKI: 2;
end;
::
GRAPH_1:def22
func
EdgesOut x ->
Element of
NAT means ex X be
finite
set st (for z be
set holds z
in X iff z
in the
carrier' of G & (the
Source of G
. z)
= x) & it
= (
card X);
existence
proof
defpred
P[
object] means (the
Source of G
. $1)
= x;
consider X be
set such that
A8: for z be
object holds z
in X iff z
in the
carrier' of G &
P[z] from
XBOOLE_0:sch 1;
for z be
object st z
in X holds z
in the
carrier' of G by
A8;
then X
c= the
carrier' of G;
then
reconsider X as
finite
set;
take (
card X);
take X;
thus thesis by
A8;
end;
uniqueness
proof
let n1,n2 be
Element of
NAT such that
A9: ex X be
finite
set st (for z be
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 be
finite
set st (for z be
set holds z
in X iff z
in the
carrier' of G & (the
Source of G
. z)
= x) & n2
= (
card X);
consider X1 be
finite
set such that
A11: for z be
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 be
finite
set such that
A13: for z be
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 be
object holds z
in X1 iff z
in X2
proof
let z be
object;
z
in X1 iff z
in the
carrier' of G & (the
Source of G
. z)
= x by
A11;
hence thesis by
A13;
end;
hence thesis by
A12,
A14,
TARSKI: 2;
end;
end
definition
let G be
finite
Graph;
let x be
Vertex of G;
::
GRAPH_1:def23
func
Degree x ->
Element of
NAT equals ((
EdgesIn x)
+ (
EdgesOut x));
correctness ;
end
Lm2: for p be
Chain of G holds (p
| (
Seg n)) is
Chain of G
proof
let p be
Chain of G;
reconsider q = (p
| (
Seg n)) as
FinSequence by
FINSEQ_1: 15;
A1: for n st 1
<= n & n
<= (
len q) holds (q
. n)
in the
carrier' of G
proof
let k be
Nat;
assume that
A2: 1
<= k and
A3: k
<= (
len q);
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 thesis by
A4,
FUNCT_1: 47;
end;
ex q1 be
FinSequence st (
len q1)
= ((
len q)
+ 1) & (for n st 1
<= n & n
<= (
len q1) holds (q1
. n)
in the
carrier of G) & for n st 1
<= n & n
<= (
len q) holds ex x9,y9 be
Vertex of G st x9
= (q1
. n) & y9
= (q1
. (n
+ 1)) & (q
. n)
joins (x9,y9)
proof
consider q1 be
FinSequence such that
A5: (
len q1)
= ((
len p)
+ 1) and
A6: for n st 1
<= n & n
<= (
len q1) holds (q1
. n)
in the
carrier of G and
A7: for n st 1
<= n & n
<= (
len p) holds ex x9,y9 be
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;
thus
A8: (
len q2)
= ((
len q)
+ 1)
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;
per cases ;
suppose
A11: ((
len p)
+ 1)
<= (n
+ 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
A12: (
len q2)
= ((
len p)
+ 1) by
FINSEQ_1:def 3;
(
len p)
<= n by
A11,
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 thesis by
A12,
FINSEQ_1:def 3;
end;
suppose
A13: (n
+ 1)
<= ((
len p)
+ 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
A14: (
len q2)
= (n
+ 1) by
FINSEQ_1:def 3;
A15: n
in
NAT by
ORDINAL1:def 12;
n
<= (
len p) by
A13,
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 thesis by
A14,
FINSEQ_1:def 3,
A15;
end;
end;
thus for n st 1
<= n & n
<= (
len q2) holds (q2
. n)
in the
carrier of G
proof
let n be
Nat;
assume that
A16: 1
<= n and
A17: n
<= (
len q2);
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 thesis by
A18,
FUNCT_1: 47;
end;
let k;
assume that
A19: 1
<= k and
A20: k
<= (
len q);
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 be
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, 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;
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;
thus thesis by
A21,
A24,
FUNCT_1: 47;
end;
hence thesis by
A1,
Def14;
end;
Lm3: for H1,H2 be
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 H1,H2 be
strict
Subgraph of G such that
A1: the
carrier of H1
= the
carrier of H2 and
A2: the
carrier' of H1
= the
carrier' of 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 be
object st x
in the
carrier' of H1 holds (the
Source of H1
. x)
= (the
Source of H2
. x)
proof
let x be
object;
assume
A5: x
in the
carrier' of H1;
hence (the
Source of H1
. x)
= (the
Source of G
. x) by
Def18
.= (the
Source of H2
. x) by
A2,
A5,
Def18;
end;
then
A6: the
Source of H1
= the
Source of H2 by
A2,
A3;
for x be
object st x
in the
carrier' of H1 holds (the
Target of H1
. x)
= (the
Target of H2
. x)
proof
let x be
object;
assume
A7: x
in the
carrier' of H1;
hence (the
Target of H1
. x)
= (the
Target of G
. x) by
Def18
.= (the
Target of H2
. x) by
A2,
A7,
Def18;
end;
hence thesis by
A1,
A2,
A4,
A6,
FUNCT_1: 2;
end;
definition
let G1,G2 be
Graph;
::
GRAPH_1:def24
pred G1
c= G2 means
:
Def24: G1 is
Subgraph of G2;
reflexivity
proof
let G;
for v 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 thesis by
Def18;
end;
end
Lm4: for G be
Graph, H be
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, H be
Subgraph 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;
EH
c= EG & VH
c= VG by
Def18;
then (
Funcs (EH,VH))
c= (
PFuncs (EH,VH)) & (
PFuncs (EH,VH))
c= (
PFuncs (EG,VG)) by
FUNCT_2: 72,
PARTFUN1: 50;
then
A1: (
Funcs (EH,VH))
c= (
PFuncs (EG,VG));
the
Source of H
in (
Funcs (EH,VH)) by
FUNCT_2: 8;
hence the
Source of H
in (
PFuncs (EG,VG)) by
A1;
the
Target of H
in (
Funcs (EH,VH)) by
FUNCT_2: 8;
hence thesis by
A1;
end;
definition
let G be
Graph;
::
GRAPH_1:def25
func
bool G ->
set means
:
Def25: for x be
object holds x
in it iff x is
strict
Subgraph of G;
existence
proof
reconsider V = the
carrier of G as non
empty
set;
set E = the
carrier' of G;
set Prod =
[:(
bool V), (
bool E), (
PFuncs (E,V)), (
PFuncs (E,V)):];
defpred
P[
object] means ex y be
Element of Prod, M be
Graph, v be non
empty
set, e be
set, s be
Function of e, v, t be
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 be
set such that
A1: for x be
object holds x
in X iff x
in Prod &
P[x] from
XBOOLE_0:sch 1;
defpred
P[
object,
object] means ex y be
Element of Prod, M be
strict
Graph, v be non
empty
set, e be
set, s be
Function of e, v, t be
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 be
object st
P[a, b] &
P[a, c] holds b
= c;
consider Y be
set such that
A3: for z be
object holds z
in Y iff ex x be
object st x
in X &
P[x, z] from
TARSKI:sch 1(
A2);
take Y;
let x be
object;
thus x
in Y implies x is
strict
Subgraph of G
proof
assume x
in Y;
then ex z be
object st z
in X &
P[z, x] by
A3;
hence thesis;
end;
assume x is
strict
Subgraph of G;
then
reconsider H = x as
strict
Subgraph of G;
ex y be
object st y
in X &
P[y, x]
proof
take y =
[the
carrier of H, the
carrier' of H, the
Source of H, the
Target of H];
A4: the
carrier of H
c= V & the
carrier' of H
c= E by
Def18;
the
Source of H
in (
PFuncs (E,V)) & the
Target of H
in (
PFuncs (E,V)) by
Lm4;
then
reconsider y9 = y as
Element of Prod 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 e, v;
reconsider t = the
Target of H as
Function of e, v;
A5: v
= (y9
`1_4 ) & e
= (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;
thus thesis by
A5,
A6;
end;
hence thesis by
A3;
end;
uniqueness
proof
defpred
P[
object] means $1 is
strict
Subgraph of G;
let X1,X2 be
set such that
A7: for x be
object holds x
in X1 iff
P[x] and
A8: for x be
object holds x
in X2 iff
P[x];
thus X1
= X2 from
XBOOLE_0:sch 2(
A7,
A8);
end;
end
scheme ::
GRAPH_1:sch1
GraphSeparation { G() ->
Graph , P[
object] } :
ex X be
set st for x be
set holds x
in X iff x is
strict
Subgraph of G() & P[x];
consider X be
set such that
A1: for x be
object holds x
in X iff x
in (
bool G()) & P[x] from
XBOOLE_0:sch 1;
take X;
let x be
set;
thus x
in X implies x is
strict
Subgraph of G() & P[x]
proof
assume
A2: x
in X;
then x
in (
bool G()) by
A1;
hence x is
strict
Subgraph of G() by
Def25;
thus thesis by
A1,
A2;
end;
assume that
A3: x is
strict
Subgraph of G() and
A4: P[x];
x
in (
bool G()) by
A3,
Def25;
hence thesis by
A1,
A4;
end;
theorem ::
GRAPH_1:1
for G be
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 x be
Vertex of G holds x
in the
carrier of G;
theorem ::
GRAPH_1:3
for v be
set holds v
in the
carrier' of G implies (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 p be
Chain of G holds (p
| (
Seg n)) is
Chain of G by
Lm2;
theorem ::
GRAPH_1:5
Th5: G1
c= G implies the
Source of G1
c= the
Source of G & the
Target of G1
c= the
Target of G
proof
assume G1
c= G;
then
A1: G1 is
Subgraph of G;
for v be
object st v
in the
Source of G1 holds v
in the
Source of G
proof
let v be
object;
assume
A2: v
in the
Source of G1;
then
consider x,y be
object 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 thesis by
A3,
A7,
FUNCT_1:def 2;
end;
hence the
Source of G1
c= the
Source of G;
let v be
object;
assume
A8: v
in the
Target of G1;
then
consider x,y be
object 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 thesis by
A9,
A13,
FUNCT_1:def 2;
end;
theorem ::
GRAPH_1:6
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)
proof
assume
A1: the
Source of G1
tolerates the
Source of G2 & the
Target of G1
tolerates 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 be
object holds v
in S12 iff v
in (S1
\/ S2)
proof
let v be
object;
thus v
in S12 implies v
in (S1
\/ S2)
proof
assume
A2: v
in S12;
then
consider x,y be
object such that
A3:
[x, y]
= v by
RELAT_1:def 1;
x
in (
dom S12) 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
assume
A6: x
in the
carrier' of G1;
then
A7: x
in (
dom S1) by
FUNCT_2:def 1;
(S1
. x)
= (S12
. x) by
A1,
A6,
Def5
.= y by
A2,
A3,
FUNCT_1: 1;
then
[x, y]
in S1 or
[x, y]
in S2 by
A7,
FUNCT_1:def 2;
hence
[x, y]
in (S1
\/ S2) by
XBOOLE_0:def 3;
end;
now
assume
A8: x
in the
carrier' of G2;
then
A9: x
in (
dom S2) by
FUNCT_2:def 1;
(S2
. x)
= (S12
. x) by
A1,
A8,
Def5
.= y by
A2,
A3,
FUNCT_1: 1;
then
[x, y]
in S1 or
[x, y]
in S2 by
A9,
FUNCT_1:def 2;
hence
[x, y]
in (S1
\/ S2) by
XBOOLE_0:def 3;
end;
hence thesis by
A3,
A4,
A5,
XBOOLE_0:def 3;
end;
assume
A10: v
in (S1
\/ S2);
A11:
now
assume
A12: v
in S1;
then
consider x,y be
object such that
A13:
[x, y]
= v by
RELAT_1:def 1;
A14: x
in (
dom S1) by
A12,
A13,
FUNCT_1: 1;
A15: y
= (S1
. 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 S12) by
FUNCT_2:def 1;
(S12
. x)
= y by
A1,
A14,
A15,
Def5;
hence thesis by
A13,
A16,
FUNCT_1:def 2;
end;
now
assume
A17: v
in S2;
then
consider x,y be
object such that
A18:
[x, y]
= v by
RELAT_1:def 1;
A19: x
in (
dom S2) by
A17,
A18,
FUNCT_1: 1;
A20: y
= (S2
. 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 S12) by
FUNCT_2:def 1;
(S12
. x)
= y by
A1,
A19,
A20,
Def5;
hence thesis by
A18,
A21,
FUNCT_1:def 2;
end;
hence thesis by
A10,
A11,
XBOOLE_0:def 3;
end;
hence S12
= (S1
\/ S2) by
TARSKI: 2;
for v be
object holds v
in T12 iff v
in (T1
\/ T2)
proof
let v be
object;
thus v
in T12 implies v
in (T1
\/ T2)
proof
assume
A22: v
in T12;
then
consider x,y be
object such that
A23:
[x, y]
= v by
RELAT_1:def 1;
x
in (
dom T12) 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
assume
A26: x
in the
carrier' of G1;
then
A27: x
in (
dom T1) by
FUNCT_2:def 1;
(T1
. x)
= (T12
. x) by
A1,
A26,
Def5
.= y by
A22,
A23,
FUNCT_1: 1;
then
[x, y]
in T1 or
[x, y]
in T2 by
A27,
FUNCT_1:def 2;
hence
[x, y]
in (T1
\/ T2) by
XBOOLE_0:def 3;
end;
now
assume
A28: x
in the
carrier' of G2;
then
A29: x
in (
dom T2) by
FUNCT_2:def 1;
(T2
. x)
= (T12
. x) by
A1,
A28,
Def5
.= y by
A22,
A23,
FUNCT_1: 1;
then
[x, y]
in T1 or
[x, y]
in T2 by
A29,
FUNCT_1:def 2;
hence
[x, y]
in (T1
\/ T2) by
XBOOLE_0:def 3;
end;
hence thesis by
A23,
A24,
A25,
XBOOLE_0:def 3;
end;
assume
A30: v
in (T1
\/ T2);
A31:
now
assume
A32: v
in T1;
then
consider x,y be
object such that
A33:
[x, y]
= v by
RELAT_1:def 1;
A34: x
in (
dom T1) by
A32,
A33,
FUNCT_1: 1;
A35: y
= (T1
. 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 T12) by
FUNCT_2:def 1;
(T12
. x)
= y by
A1,
A34,
A35,
Def5;
hence thesis by
A33,
A36,
FUNCT_1:def 2;
end;
now
assume
A37: v
in T2;
then
consider x,y be
object such that
A38:
[x, y]
= v by
RELAT_1:def 1;
A39: x
in (
dom T2) by
A37,
A38,
FUNCT_1: 1;
A40: y
= (T2
. 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 T12) by
FUNCT_2:def 1;
(T12
. x)
= y by
A1,
A39,
A40,
Def5;
hence thesis by
A38,
A41,
FUNCT_1:def 2;
end;
hence thesis by
A30,
A31,
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
GRAPH_1:7
Th7: for G be
strict
Graph holds G
= (G
\/ G)
proof
let G be
strict
Graph;
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 be
object 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;
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 be
object st v
in (
dom the
Target of G) holds (the
Target of G
. v)
= (the
Target of (G
\/ G)
. v) by
Def5;
hence thesis by
A1,
A2,
A4,
A5,
FUNCT_1: 2;
end;
theorem ::
GRAPH_1:8
Th8: the
Source of G1
tolerates the
Source of G2 & the
Target of G1
tolerates the
Target of G2 implies (G1
\/ G2)
= (G2
\/ G1)
proof
assume
A1: the
Source of G1
tolerates the
Source of G2 & the
Target of G1
tolerates the
Target of G2;
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 be
object 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
object;
assume v
in (
dom the
Source of (G1
\/ G2));
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
assume
A7: v
in the
carrier' of G1;
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;
end;
now
assume
A8: v
in the
carrier' of G2;
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;
end;
hence thesis by
A5,
A6,
XBOOLE_0:def 3;
end;
then
A9: the
Source of (G1
\/ G2)
= the
Source of (G2
\/ G1) by
A4;
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 be
object 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
object;
assume v
in (
dom the
Target of (G1
\/ G2));
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
assume
A13: v
in the
carrier' of G1;
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;
end;
now
assume
A14: v
in the
carrier' of G2;
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;
end;
hence thesis by
A11,
A12,
XBOOLE_0:def 3;
end;
hence thesis by
A2,
A3,
A9,
A10,
FUNCT_1: 2;
end;
theorem ::
GRAPH_1:9
Th9: 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))
proof
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;
A7: for v be
object 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
object;
assume
A8: v
in ((
dom the
Source of (G1
\/ G2))
/\ (
dom the
Source of G3));
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
assume
A12: v
in the
carrier' of G1;
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;
end;
now
assume
A14: v
in the
carrier' of G2;
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;
end;
hence thesis by
A10,
A11,
XBOOLE_0:def 3;
end;
A16: for v be
object 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
object;
assume
A17: v
in ((
dom the
Target of (G1
\/ G2))
/\ (
dom the
Target of G3));
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
assume
A21: v
in the
carrier' of G1;
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;
end;
now
assume
A23: v
in the
carrier' of G2;
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;
end;
hence thesis by
A19,
A20,
XBOOLE_0:def 3;
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 be
object 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
object;
assume
A28: v
in ((
dom the
Source of G1)
/\ (
dom the
Source of (G2
\/ G3)));
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
assume
A32: v
in (
dom the
Source of G2);
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;
end;
now
assume
A34: v
in (
dom the
Source of G3);
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;
end;
hence thesis by
A30,
A31,
XBOOLE_0:def 3;
end;
A36: for v be
object 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
object;
assume
A37: v
in ((
dom the
Target of G1)
/\ (
dom the
Target of (G2
\/ G3)));
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
assume
A41: v
in (
dom the
Target of G2);
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;
end;
now
assume
A43: v
in (
dom the
Target of G3);
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;
end;
hence thesis by
A39,
A40,
XBOOLE_0:def 3;
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 be
object 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
object such that
A50: v
in (
dom the
Source of ((G1
\/ G2)
\/ G3));
(
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
assume
A53: v
in the
carrier' of G1;
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;
end;
A54:
now
assume
A55: v
in the
carrier' of G2;
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;
end;
now
assume
A58: v
in the
carrier' of G3;
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;
end;
hence thesis by
A51,
A52,
A54,
XBOOLE_0:def 3;
end;
then
A60: the
Source of ((G1
\/ G2)
\/ G3)
= the
Source of (G1
\/ (G2
\/ G3)) by
A49;
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 be
object 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
object such that
A62: v
in (
dom the
Target of ((G1
\/ G2)
\/ G3));
(
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
assume
A65: v
in the
carrier' of G1;
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;
end;
A66:
now
assume
A67: v
in the
carrier' of G2;
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;
end;
now
assume
A70: v
in the
carrier' of G3;
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;
end;
hence thesis by
A63,
A64,
A66,
XBOOLE_0:def 3;
end;
hence thesis by
A47,
A48,
A60,
A61,
FUNCT_1: 2;
end;
theorem ::
GRAPH_1:10
Th10: G
is_sum_of (G1,G2) implies G
is_sum_of (G2,G1) by
Th8;
theorem ::
GRAPH_1:11
for G be
strict
Graph holds G
is_sum_of (G,G) by
Th7;
theorem ::
GRAPH_1:12
Th12: (ex G st G1
c= G & G2
c= G) implies (G1
\/ G2)
= (G2
\/ G1)
proof
given G such that
A1: G1
c= G & G2
c= G;
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 thesis by
A4,
Th8;
end;
theorem ::
GRAPH_1:13
(ex G st G1
c= G & G2
c= G & G3
c= G) implies ((G1
\/ G2)
\/ G3)
= (G1
\/ (G2
\/ G3))
proof
given G such that
A1: G1
c= G and
A2: G2
c= G and
A3: G3
c= G;
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 thesis by
A10,
A11,
A12,
A13,
A14,
Th9;
end;
theorem ::
GRAPH_1:14
{} is
Chain of G by
Lm1;
theorem ::
GRAPH_1:15
for H1,H2 be
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 ::
GRAPH_1:16
Th16: for G1,G2 be
strict
Graph holds G1
c= G2 & G2
c= G1 implies G1
= G2
proof
let G1,G2 be
strict
Graph;
assume that
A1: G1
c= G2 and
A2: G2
c= G1;
A3: G1 is
Subgraph of G2 by
A1;
A4: G2 is
Subgraph of G1 by
A2;
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 be
object 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;
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 be
object st v
in (
dom the
Target of G1) holds (the
Target of G1
. v)
= (the
Target of G2
. v) by
A3,
Def18;
hence thesis by
A6,
A8,
A10,
A11,
FUNCT_1: 2;
end;
theorem ::
GRAPH_1:17
Th17: G1
c= G2 & G2
c= G3 implies G1
c= G3
proof
assume that
A1: G1
c= G2 and
A2: G2
c= G3;
A3: G1 is
Subgraph of G2 by
A1;
A4: G2 is
Subgraph of G3 by
A2;
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;
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;
for v 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;
assume
A9: 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;
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;
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;
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 thesis by
A11;
end;
then G1 is
Subgraph of G3 by
A6,
A8,
Def18;
hence thesis;
end;
theorem ::
GRAPH_1:18
Th18: G
is_sum_of (G1,G2) implies G1
c= G & G2
c= G
proof
assume
A1: G
is_sum_of (G1,G2);
A2: for G,G1,G2 be
Graph st G
is_sum_of (G1,G2) holds G1
c= G
proof
let G,G1,G2 be
Graph;
assume
A3: G
is_sum_of (G1,G2);
then
A4: the
Source of G1
tolerates the
Source of G2 & the
Target of G1
tolerates the
Target of G2;
A5: the MultiGraphStruct of G
= (G1
\/ G2) by
A3;
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 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;
assume
A8: v
in the
carrier' of G1;
hence
A9: (the
Source of G1
. v)
= (the
Source of G
. v) by
A4,
A5,
Def5;
thus
A10: (the
Target of G1
. v)
= (the
Target of G
. v) by
A4,
A5,
A8,
Def5;
thus (the
Source of G
. v)
in the
carrier of G1 by
A8,
A9,
FUNCT_2: 5;
thus thesis by
A8,
A10,
FUNCT_2: 5;
end;
then G1 is
Subgraph of G by
A6,
A7,
Def18;
hence thesis;
end;
hence G1
c= G by
A1;
thus thesis by
A1,
A2,
Th10;
end;
theorem ::
GRAPH_1:19
Th19: 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)
proof
assume the
Source of G1
tolerates the
Source of G2 & the
Target of G1
tolerates the
Target of G2;
then (G1
\/ G2)
is_sum_of (G1,G2);
hence thesis by
Th18;
end;
theorem ::
GRAPH_1:20
Th20: (ex G st G1
c= G & G2
c= G) implies G1
c= (G1
\/ G2) & G2
c= (G1
\/ G2)
proof
given G such that
A1: G1
c= G & G2
c= G;
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 thesis by
A4,
Th19;
end;
theorem ::
GRAPH_1:21
Th21: G1
c= G3 & G2
c= G3 & G
is_sum_of (G1,G2) implies G
c= G3
proof
assume that
A1: G1
c= G3 and
A2: G2
c= G3 and
A3: G
is_sum_of (G1,G2);
A4: the
Source of G1
tolerates the
Source of G2 & the
Target of G1
tolerates the
Target of G2 by
A3;
A5: the MultiGraphStruct of G
= (G1
\/ G2) by
A3;
A6: G1 is
Subgraph of G3 by
A1;
A7: G2 is
Subgraph of G3 by
A2;
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 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 such that
A12: 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)
proof
A14: v
in (the
carrier' of G1
\/ the
carrier' of G2) by
A4,
A12,
Def5;
A15:
now
assume
A16: v
in the
carrier' of G1;
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 thesis by
A17;
end;
now
assume
A18: v
in the
carrier' of G2;
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 thesis by
A19;
end;
hence thesis by
A14,
A15,
XBOOLE_0:def 3;
end;
hence (the
Source of G3
. v)
in the
carrier of (G1
\/ G2) by
A12,
FUNCT_2: 5;
thus thesis by
A12,
A13,
FUNCT_2: 5;
end;
hence the
carrier of G
c= the
carrier of G3 & the
carrier' of G
c= the
carrier' of G3 & for v 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;
end;
theorem ::
GRAPH_1:22
Th22: G1
c= G & G2
c= G implies (G1
\/ G2)
c= G
proof
assume
A1: G1
c= G & 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;
hence thesis by
A1,
Th21;
end;
theorem ::
GRAPH_1:23
for G1,G2 be
strict
Graph holds G1
c= G2 implies (G1
\/ G2)
= G2 & (G2
\/ G1)
= G2
proof
let G1,G2 be
strict
Graph;
assume
A1: G1
c= G2;
then (G1
\/ G2)
c= G2 & G2
c= (G1
\/ G2) by
Th20,
Th22;
hence (G1
\/ G2)
= G2 by
Th16;
hence thesis by
A1,
Th12;
end;
theorem ::
GRAPH_1:24
Th24: 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
proof
assume
A1: the
Source of G1
tolerates the
Source of G2 & the
Target of G1
tolerates the
Target of G2;
assume
A2: (G1
\/ G2)
= G2 or (G2
\/ G1)
= 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 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;
assume
A5: v
in the
carrier' of G1;
hence
A6: (the
Source of G1
. v)
= (the
Source of G2
. v) by
A1,
A2,
Def5;
thus
A7: (the
Target of G1
. v)
= (the
Target of G2
. v) by
A1,
A2,
A5,
Def5;
thus (the
Source of G2
. v)
in the
carrier of G1 by
A5,
A6,
FUNCT_2: 5;
thus thesis by
A5,
A7,
FUNCT_2: 5;
end;
then G1 is
Subgraph of G2 by
A3,
A4,
Def18;
hence thesis;
end;
theorem ::
GRAPH_1:25
for G be
oriented
Graph st G1
c= G holds G1 is
oriented
proof
let G be
oriented
Graph;
assume G1
c= G;
then
A1: G1 is
Subgraph of G;
for x,y be
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;
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);
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 thesis by
A2,
A3,
A6,
A7,
Def7;
end;
hence thesis;
end;
theorem ::
GRAPH_1:26
for G be
non-multi
Graph st G1
c= G holds G1 is
non-multi
proof
let G be
non-multi
Graph;
assume G1
c= G;
then
A1: G1 is
Subgraph of G;
for x,y be
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 such that
A2: x
in the
carrier' of G1 & y
in the
carrier' of G1;
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);
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 thesis by
A2,
A3,
A4,
A5,
Def8;
end;
hence thesis;
end;
theorem ::
GRAPH_1:27
for G be
simple
Graph st G1
c= G holds G1 is
simple
proof
let G be
simple
Graph;
assume G1
c= G;
then
A1: G1 is
Subgraph of G;
not ex x be
set st x
in the
carrier' of G1 & (the
Source of G1
. x)
= (the
Target of G1
. x)
proof
given x be
set such that
A2: x
in the
carrier' of G1 and
A3: (the
Source of G1
. x)
= (the
Target of G1
. x);
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;
end;
hence thesis;
end;
theorem ::
GRAPH_1:28
for G1 be
strict
Graph holds G1
in (
bool G) iff G1
c= G by
Def25;
theorem ::
GRAPH_1:29
Th29: for G be
strict
Graph holds G
in (
bool G)
proof
let G be
strict
Graph;
G is
Subgraph of G by
Def24;
hence thesis by
Def25;
end;
theorem ::
GRAPH_1:30
for G1 be
strict
Graph holds G1
c= G2 iff (
bool G1)
c= (
bool G2)
proof
let G1 be
strict
Graph;
thus G1
c= G2 implies (
bool G1)
c= (
bool G2)
proof
assume
A1: G1
c= G2;
let x be
object;
assume x
in (
bool G1);
then
reconsider G = x as
strict
Subgraph of G1 by
Def25;
G
c= G1;
then G
c= G2 by
A1,
Th17;
then G is
strict
Subgraph of G2;
hence thesis by
Def25;
end;
assume
A2: (
bool G1)
c= (
bool G2);
G1
in (
bool G1) by
Th29;
then G1 is
Subgraph of G2 by
A2,
Def25;
hence thesis;
end;
theorem ::
GRAPH_1:31
for G be
strict
Graph holds
{G}
c= (
bool G) by
Th29,
ZFMISC_1: 31;
theorem ::
GRAPH_1:32
for G1,G2 be
strict
Graph holds 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)) implies G1
c= G2 or G2
c= G1
proof
let G1,G2 be
strict
Graph;
assume
A1: the
Source of G1
tolerates the
Source of G2 & the
Target of G1
tolerates the
Target of G2;
assume
A2: (
bool (G1
\/ G2))
c= ((
bool G1)
\/ (
bool G2));
A3: (G1
\/ G2)
in (
bool (G1
\/ G2)) by
Th29;
A4:
now
assume (G1
\/ G2)
in (
bool G1);
then (G1
\/ G2) is
Subgraph of G1 by
Def25;
then
A5: (G1
\/ G2)
c= G1;
G1
c= (G1
\/ G2) by
A1,
Th19;
then (G1
\/ G2)
= G1 by
A5,
Th16;
hence G2
c= G1 by
A1,
Th24;
end;
now
assume (G1
\/ G2)
in (
bool G2);
then (G1
\/ G2) is
Subgraph of G2 by
Def25;
then
A6: (G1
\/ G2)
c= G2;
G2
c= (G1
\/ G2) by
A1,
Th19;
then (G1
\/ G2)
= G2 by
A6,
Th16;
hence G1
c= G2 by
A1,
Th24;
end;
hence thesis by
A2,
A3,
A4,
XBOOLE_0:def 3;
end;
theorem ::
GRAPH_1:33
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))
proof
assume
A1: the
Source of G1
tolerates the
Source of G2 & the
Target of G1
tolerates the
Target of G2;
A2: for v st v
in (
bool G1) holds v
in (
bool (G1
\/ G2))
proof
let v;
assume v
in (
bool G1);
then
reconsider G = v as
strict
Subgraph of G1 by
Def25;
G
c= G1 & G1
c= (G1
\/ G2) by
A1,
Th19;
then G
c= (G1
\/ G2) by
Th17;
then G is
strict
Subgraph of (G1
\/ G2);
hence thesis by
Def25;
end;
A3: for v st v
in (
bool G2) holds v
in (
bool (G1
\/ G2))
proof
let v;
assume v
in (
bool G2);
then
reconsider G = v as
strict
Subgraph of G2 by
Def25;
G
c= G2 & G2
c= (G1
\/ G2) by
A1,
Th19;
then G
c= (G1
\/ G2) by
Th17;
then G is
strict
Subgraph of (G1
\/ G2);
hence thesis by
Def25;
end;
let v be
object;
assume v
in ((
bool G1)
\/ (
bool G2));
then v
in (
bool G1) or v
in (
bool G2) by
XBOOLE_0:def 3;
hence thesis by
A2,
A3;
end;
theorem ::
GRAPH_1:34
G1
in (
bool G) & G2
in (
bool G) implies (G1
\/ G2)
in (
bool G)
proof
assume that
A1: G1
in (
bool G) and
A2: 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;
G2
c= G by
A4;
then (G1
\/ G2)
c= G by
A5,
Th22;
then (G1
\/ G2) is
Subgraph of G;
hence thesis by
Def25;
end;