:: Graphs
:: by Krzysztof Hryniewiecki
::
:: Received December 5, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, STRUCT_0, FUNCT_1, GLIB_000, XBOOLE_0,
FUNCT_5, RELAT_1, PARTFUN1, RELAT_2, FINSET_1, TREES_2, FINSEQ_1,
XXREAL_0, ARYTM_3, TARSKI, CARD_1, FUNCT_2, ZFMISC_1, GRAPH_1, RECDEF_2,
NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
FUNCT_2, FUNCT_5, FINSEQ_1, FINSET_1, PARTFUN1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, NAT_1, XTUPLE_0, MCART_1, XXREAL_0, STRUCT_0;
constructors PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0,
FUNCT_5, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1,
XREAL_0, FINSEQ_1, ORDINAL1, STRUCT_0, CARD_1, FUNCT_2, RELSET_1, NAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions FUNCT_1, TARSKI;
expansions FUNCT_1, TARSKI;
theorems FUNCT_2, FUNCT_1, PARTFUN1, FINSEQ_1, NAT_1, ZFMISC_1, MCART_1,
TARSKI, RELAT_1, FINSEQ_3, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, ORDINAL1;
schemes FUNCT_2, TARSKI, XBOOLE_0;
begin
reserve x, y, z, v for set,
n, m, k for Nat;
definition
struct(2-sorted) MultiGraphStruct (# carrier, carrier' -> set,
Source, Target -> Function of the carrier', the carrier #);
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;
:: from CAT_1, 2008.07.02, A.T.
definition
let C be MultiGraphStruct, f be Edge of C;
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;
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;
redefine func dom f -> Vertex of C equals (the Source of C).f; :: redefines dom (GRAPH_1, definition)
compatibility by Def1;
coherence;
redefine func cod f -> Vertex of C equals (the Target of C).f; :: redefines cod (GRAPH_1, definition)
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);
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 being 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 being object st x in E ex y being 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 being Function of E, V such that
A10: for x being 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 being 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 being 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 being object st x in E ex y being 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 being Function of E, V such that
A22: for x being 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 being 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 being 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 being 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;
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;
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;
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;
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;
attr IT is connected means
not ex G1, G2 being Graph st
the carrier of G1 misses the carrier of G2 & IT is_sum_of G1, G2;
end;
definition
let IT be MultiGraphStruct;
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 being Graph st
(the carrier of G1) misses (the carrier of G2) & 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;
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;
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);
pred x,y are_incident means
ex v being set st v in the carrier' of G & v joins x, y;
end;
definition
let G be Graph;
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 being 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
ex x9, y9 being 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;
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;
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;
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;
end;
let n;
thus thesis;
end;
definition
let G be Graph;
redefine mode Chain of G -> FinSequence of the carrier' of G; :: redefines Chain (GRAPH_1, definition)
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 being 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;
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;
redefine attr IT is one-to-one means :: redefines one-to-one (FUNCT_1, definition)
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;
attr IT is cyclic means
ex p being 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
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;
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;
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;
end;
thus for n st 1 <= n & n <= len p ex x9, y9 being 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;
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;
func VerticesCount G -> Element of NAT means
ex B being 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;
func EdgesCount G -> Element of NAT means
ex B being 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;
func EdgesIn x -> Element of NAT means
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
proof
defpred P[object] means (the Target of G).$1 = x;
consider X being set such that
A1: for z being object holds z in X iff
z in the carrier' of G & P[z] from XBOOLE_0:sch 1;
for z being 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 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);
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 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;
func EdgesOut x -> Element of NAT means
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
proof
defpred P[object] means (the Source of G).$1 = x;
consider X being set such that
A8: for z being object holds z in X iff
z in the carrier' of G & P[z] from XBOOLE_0:sch 1;
for z being 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 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);
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 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;
func Degree x -> Element of NAT equals
EdgesIn(x) + EdgesOut(x);
correctness;
end;
Lm2: for p being 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 being 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 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 st 1 <= n & n <= len q1 holds q1.n in the carrier of G and
A7: for n st 1 <= n & n <= len p 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;
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 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, 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 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 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 being 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 being 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;
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 being Graph, 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, 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;
func bool G -> set means
:Def25:
for x being 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 being Element of Prod, M being Graph,
v being non empty set, e being set, s being (Function of e, v),
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 object holds x in X iff x in Prod & P[x] from XBOOLE_0:sch 1;
defpred P[object, object] means ex y being Element of Prod,
M being strict Graph, v being non empty set, e being set,
s being Function of e, v, 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 object st P[a,b] & P[a, c] holds b = c;
consider Y being set such that
A3: for z being object holds z in Y iff
ex x being 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 being 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 being 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,def 9;
A6: s = y9`3_4 & t = y9`4_4 by MCART_1:def 10,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 being object holds x in X1 iff P[x] and
A8: for x being object holds x in X2 iff P[x];
thus X1 = X2 from XBOOLE_0:sch 2(A7,A8);
end;
end;
scheme GraphSeparation{G() -> Graph, P[object]}:
ex X being set st
for x being set holds x in X iff x is strict Subgraph of G() & P[x]
proof
consider X being set such that
A1: for
x being 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;
:: Properties of graphs ::
theorem
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
for x being Vertex of G holds x in the carrier of G;
theorem
for v being 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;
:: Chain ::
theorem
for p being Chain of G holds p|Seg(n) is Chain of G by Lm2;
:: Sum of two graphs ::
theorem 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 being 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 being 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 being 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
(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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 Th7:
for G being 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 being 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 being 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 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 being 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 being 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 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 Th10:
G is_sum_of G1, G2 implies G is_sum_of G2, G1
by Th8;
theorem
for G being strict Graph holds G is_sum_of G, G
by Th7;
:: Graphs' inclusion ::
theorem 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
(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
{} is Chain of G by Lm1;
theorem
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:
for G1,G2 being 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 being 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 being 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 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;
thus
then 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 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 being 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;
thus
then 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 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 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 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 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
for G1,G2 being 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;
thus
then G1 \/ G2 = G2 by Th16;
hence thesis by A1,Th12;
end;
theorem 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;
thus
then 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
for G being 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 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;
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
for G being 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 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 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
for G being 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 being set st x in the carrier' of G1 &
(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;
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;
:: Set of all subgraphs ::
theorem
for G1 being strict Graph holds G1 in bool G iff G1 c= G
by Def25;
theorem Th29:
for G being 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
for G1 being 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
for G being strict Graph holds { G } c= bool G by Th29,ZFMISC_1:31;
theorem
for G1,G2 being 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
(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
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;