:: Alternative Graph Structures
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received February 22, 2005
:: Copyright (c) 2005-2021 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, FINSET_1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1,
FINSEQ_1, NAT_1, FUNCT_4, FUNCOP_1, ZFMISC_1, CARD_1, ARYTM_3, CARD_2,
ORDINAL2, XXREAL_0, PBOOLE, GLIB_000, XCMPLX_0;
notations TARSKI, XBOOLE_0, DOMAIN_1, SUBSET_1, PBOOLE, RELAT_1, CARD_1,
CARD_2, FUNCT_1, RELSET_1, FINSEQ_1, FINSET_1, ORDINAL1, XCMPLX_0, NAT_1,
FUNCT_2, FUNCOP_1, FUNCT_4, ORDINAL2, FINSEQ_4, NUMBERS, XXREAL_0;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, FINSEQ_4, FUNCT_2, PARTFUN1,
RELSET_1;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions TARSKI, RELAT_1;
equalities FUNCOP_1;
expansions TARSKI;
theorems CARD_1, CARD_2, FUNCOP_1, ENUMSET1, FINSEQ_1, FUNCT_1, FUNCT_2,
FUNCT_4, NAT_1, RELAT_1, FINSEQ_4, TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1,
XREAL_1, XXREAL_0, ORDINAL1, RELSET_1, PARTFUN1;
schemes NAT_1, SUBSET_1;
begin :: Definitions
registration
cluster finite NAT-defined for Function;
existence
proof
take {};
thus {} is finite;
thus dom {} c= NAT;
end;
end;
definition
mode GraphStruct is finite NAT-defined Function;
end;
definition
func VertexSelector -> Element of NAT equals
1;
coherence;
func EdgeSelector -> Element of NAT equals
2;
coherence;
func SourceSelector -> Element of NAT equals
3;
coherence;
func TargetSelector -> Element of NAT equals
4;
coherence;
end;
definition
func _GraphSelectors -> non empty Subset of NAT equals
{VertexSelector,
EdgeSelector, SourceSelector, TargetSelector};
coherence;
end;
definition
let G be GraphStruct;
func the_Vertices_of G -> set equals
G.VertexSelector;
coherence;
func the_Edges_of G -> set equals
G.EdgeSelector;
coherence;
func the_Source_of G -> set equals
G.SourceSelector;
coherence;
func the_Target_of G -> set equals
G.TargetSelector;
coherence;
end;
definition
let G be GraphStruct;
attr G is [Graph-like] means
:Def10:
VertexSelector in dom G & EdgeSelector in dom G &
SourceSelector in dom G & TargetSelector in dom G &
the_Vertices_of G is non empty set &
the_Source_of G is Function of the_Edges_of G, the_Vertices_of G &
the_Target_of G is Function of the_Edges_of G, the_Vertices_of G;
end;
registration
cluster [Graph-like] for GraphStruct;
existence
proof
set V = {1}, E = {};
reconsider S = {} as Function of E,V by RELSET_1:12;
set G = <*V,E,S,S*>;
len G=4 by FINSEQ_4:76;
then
A1: dom G = Seg 4 by FINSEQ_1:def 3;
reconsider G as GraphStruct;
A2: SourceSelector in dom G & TargetSelector in dom G by A1,FINSEQ_1:1;
A3: the_Vertices_of G = V & the_Edges_of G = E by FINSEQ_4:76;
A4: the_Source_of G = S & the_Target_of G = S by FINSEQ_4:76;
VertexSelector in dom G & EdgeSelector in dom G by A1,FINSEQ_1:1;
then G is [Graph-like] by A3,A4,A2;
hence thesis;
end;
end;
definition
mode _Graph is [Graph-like] GraphStruct;
end;
registration
let G be _Graph;
cluster the_Vertices_of G -> non empty;
coherence by Def10;
end;
definition
let G be _Graph;
redefine func the_Source_of G -> Function of the_Edges_of G,the_Vertices_of
G;
coherence by Def10;
redefine func the_Target_of G -> Function of the_Edges_of G,the_Vertices_of
G;
coherence by Def10;
end;
definition
let V be non empty set,E be set, S,T be Function of E,V;
func createGraph(V,E,S,T) -> _Graph equals
<* V, E, S, T *>;
coherence
proof
set G = <*V,E,S,T*>;
len G = 4 by FINSEQ_4:76;
then
A1: dom G = Seg 4 by FINSEQ_1:def 3;
reconsider G as GraphStruct;
A2: SourceSelector in dom G & TargetSelector in dom G by A1,FINSEQ_1:1;
A3: the_Vertices_of G = V & the_Edges_of G = E by FINSEQ_4:76;
A4: the_Source_of G = S & the_Target_of G = T by FINSEQ_4:76;
VertexSelector in dom G & EdgeSelector in dom G by A1,FINSEQ_1:1;
hence thesis by A3,A4,A2,Def10;
end;
end;
definition
let G be GraphStruct, n be Nat, x be set;
func G.set(n,x) -> GraphStruct equals
G +* (n .--> x);
coherence
proof
set IT = G +* (n .--> x);
n in NAT by ORDINAL1:def 12;
then
A2: {n} c= NAT by ZFMISC_1:31;
dom IT = dom G \/ dom (n .--> x) & dom G c= NAT by FUNCT_4:def 1;
then dom IT c= NAT by A2,XBOOLE_1:8;
hence thesis by RELAT_1:def 18;
end;
end;
Lm1: for GS being GraphStruct holds GS is [Graph-like] iff _GraphSelectors c=
dom GS & the_Vertices_of GS is non empty & the_Source_of GS is Function of
the_Edges_of GS,the_Vertices_of GS & the_Target_of GS is Function of
the_Edges_of GS,the_Vertices_of GS
proof
let GS be GraphStruct;
now
thus VertexSelector in dom GS & EdgeSelector in dom GS &
SourceSelector in dom GS & TargetSelector in dom GS
implies _GraphSelectors c= dom GS by ENUMSET1:def 2;
A1: VertexSelector in _GraphSelectors & EdgeSelector in _GraphSelectors
by ENUMSET1:def 2;
A2: SourceSelector in _GraphSelectors & TargetSelector in _GraphSelectors
by ENUMSET1:def 2;
assume _GraphSelectors c= dom GS;
hence VertexSelector in dom GS & EdgeSelector in dom GS &
SourceSelector in dom GS & TargetSelector in dom GS by A1,A2;
end;
hence thesis;
end;
registration
let G be _Graph;
cluster G|(_GraphSelectors) -> [Graph-like];
coherence
proof
now
let x be object;
assume x in _GraphSelectors;
then
x = VertexSelector or x = EdgeSelector or x = SourceSelector or x =
TargetSelector by ENUMSET1:def 2;
hence x in dom G by Def10;
end;
then
A1: _GraphSelectors c= dom G;
set G2 = G|(_GraphSelectors);
VertexSelector in _GraphSelectors by ENUMSET1:def 2;
then
A2: the_Vertices_of G2 = the_Vertices_of G by FUNCT_1:49;
EdgeSelector in _GraphSelectors by ENUMSET1:def 2;
then
A3: the_Edges_of G2 = the_Edges_of G by FUNCT_1:49;
TargetSelector in _GraphSelectors by ENUMSET1:def 2;
then
A4: the_Target_of G2 = the_Target_of G by FUNCT_1:49;
SourceSelector in _GraphSelectors by ENUMSET1:def 2;
then
A5: the_Source_of G2 = the_Source_of G by FUNCT_1:49;
dom G2 = dom G /\ _GraphSelectors by RELAT_1:61
.= _GraphSelectors by A1,XBOOLE_1:28;
hence thesis by A2,A3,A5,A4,Lm1;
end;
end;
definition
let G be _Graph, x,y,e be object;
pred e Joins x,y,G means
e in the_Edges_of G & ( (the_Source_of G).e
= x & (the_Target_of G).e = y or (the_Source_of G).e = y & (the_Target_of G).e
= x );
end;
definition
let G be _Graph, x, y, e be object;
pred e DJoins x,y,G means
e in the_Edges_of G & (the_Source_of G).e = x & (the_Target_of G).e = y;
end;
definition
let G be _Graph, X,Y be set,e be object;
pred e SJoins X,Y,G means
e in the_Edges_of G & ( (the_Source_of G).e in X & (the_Target_of G).e in Y
or (the_Source_of G).e in Y & (the_Target_of G).e in X);
pred e DSJoins X,Y,G means
e in the_Edges_of G & (the_Source_of G).e in X & (the_Target_of G).e in Y;
end;
definition
let G be _Graph;
attr G is _finite means
:Def17:
the_Vertices_of G is finite & the_Edges_of G is finite;
attr G is loopless means
:Def18:
not ex e being object st e in the_Edges_of G &
(the_Source_of G).e = (the_Target_of G).e;
attr G is _trivial means
:Def19:
card the_Vertices_of G = 1;
attr G is non-multi means
:Def20:
for e1,e2,v1,v2 being object holds e1 Joins
v1,v2,G & e2 Joins v1,v2,G implies e1 = e2;
attr G is non-Dmulti means
for e1,e2,v1,v2 being object holds e1 DJoins
v1,v2,G & e2 DJoins v1,v2,G implies e1 = e2;
end;
definition
let G be _Graph;
attr G is simple means
G is loopless & G is non-multi;
attr G is Dsimple means
G is loopless & G is non-Dmulti;
end;
Lm2: for G being _Graph holds the_Edges_of G = {} implies G is simple
proof
let G be _Graph;
assume
A1: the_Edges_of G = {};
then
A2: G is loopless;
for e1,e2,v1,v2 being object holds e1 Joins v1,v2,G & e2 Joins v1,v2,G
implies e1 = e2 by A1;
then G is non-multi;
hence thesis by A2;
end;
registration
cluster non-multi -> non-Dmulti for _Graph;
coherence
proof
let G be _Graph;
assume
A1: G is non-multi;
now
let e1,e2,v1,v2 be object;
assume e1 DJoins v1,v2,G & e2 DJoins v1,v2,G;
then e1 Joins v1,v2,G & e2 Joins v1,v2,G;
hence e1 = e2 by A1;
end;
hence thesis;
end;
cluster simple -> loopless non-multi for _Graph;
coherence;
cluster loopless non-multi -> simple for _Graph;
coherence;
cluster loopless non-Dmulti -> Dsimple for _Graph;
coherence;
cluster Dsimple -> loopless non-Dmulti for _Graph;
coherence;
cluster _trivial loopless -> _finite for _Graph;
coherence
proof
let G be _Graph;
assume that
A2: G is _trivial and
A3: G is loopless;
card the_Vertices_of G = 1 by A2;
then consider v being object such that
A4: the_Vertices_of G = {v} by CARD_2:42;
now
per cases;
suppose
the_Edges_of G is empty;
hence the_Edges_of G is finite;
end;
suppose
the_Edges_of G is non empty;
then consider e being object such that
A5: e in the_Edges_of G by XBOOLE_0:def 1;
(the_Target_of G).e in the_Vertices_of G by A5,FUNCT_2:5;
then
A6: (the_Target_of G).e = v by A4,TARSKI:def 1;
(the_Source_of G).e in the_Vertices_of G by A5,FUNCT_2:5;
then (the_Source_of G).e = v by A4,TARSKI:def 1;
hence the_Edges_of G is finite by A3,A5,A6;
end;
end;
hence thesis by A4;
end;
cluster _trivial non-Dmulti -> _finite for _Graph;
coherence
proof
let G be _Graph;
assume that
A7: G is _trivial and
A8: G is non-Dmulti;
card the_Vertices_of G = 1 by A7;
then consider v being object such that
A9: the_Vertices_of G = {v} by CARD_2:42;
now
set e1 = the Element of the_Edges_of G;
set v1 = (the_Source_of G).e1, v2 = (the_Target_of G).e1;
assume
A10: not the_Edges_of G is finite;
then
A11: the_Edges_of G <> {};
v2 in the_Vertices_of G by A10,FUNCT_2:5;
then
A12: v2 = v by A9,TARSKI:def 1;
v1 in the_Vertices_of G by A10,FUNCT_2:5;
then v1 = v by A9,TARSKI:def 1;
then
A13: e1 DJoins v,v,G by A11,A12;
now
let x be object;
set v1 = (the_Source_of G).x, v2 = (the_Target_of G).x;
hereby
assume x in {e1};
then x = e1 by TARSKI:def 1;
hence x in the_Edges_of G by A11;
end;
assume
A14: x in the_Edges_of G;
then v2 in the_Vertices_of G by FUNCT_2:5;
then
A15: v2 = v by A9,TARSKI:def 1;
v1 in the_Vertices_of G by A14,FUNCT_2:5;
then v1 = v by A9,TARSKI:def 1;
then x DJoins v,v,G by A14,A15;
then x = e1 by A8,A13;
hence x in {e1} by TARSKI:def 1;
end;
hence contradiction by A10,TARSKI:2;
end;
hence thesis by A9;
end;
end;
registration
cluster _trivial simple for _Graph;
existence
proof
set V = {1}, E = {};
reconsider S = {} as Function of E,V by RELSET_1:12;
set G = createGraph(V,E,S,S);
take G;
the_Vertices_of G = {1} by FINSEQ_4:76;
then card the_Vertices_of G = 1 by CARD_1:30;
hence G is _trivial;
the_Edges_of G = {} by FINSEQ_4:76;
then
for e1,e2,v1,v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2;
then
A1: G is non-multi;
not ex e being object st e in the_Edges_of G & (the_Source_of G).e = (
the_Target_of G).e by FINSEQ_4:76;
then G is loopless;
hence thesis by A1;
end;
cluster _finite non _trivial simple for _Graph;
existence
proof
set V = {1,2}, E = {};
reconsider S = {} as Function of E,V by RELSET_1:12;
set G = createGraph(V,E,S,S);
take G;
A2: the_Edges_of G = {} by FINSEQ_4:76;
A3: the_Vertices_of G = {1,2} by FINSEQ_4:76;
hence G is _finite by A2;
card the_Vertices_of G <> 1 by A3,CARD_2:57;
hence G is non _trivial;
not ex e being object st e in the_Edges_of G & (the_Source_of G).e = (
the_Target_of G).e by FINSEQ_4:76;
then
A4: G is loopless;
for e1,e2,v1,v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G
holds e1 = e2 by A2;
then G is non-multi;
hence thesis by A4;
end;
end;
registration
let G be _finite _Graph;
cluster the_Vertices_of G -> finite;
coherence by Def17;
cluster the_Edges_of G -> finite;
coherence by Def17;
end;
registration
let G be _trivial _Graph;
cluster the_Vertices_of G -> finite;
coherence
proof
card the_Vertices_of G = 1 by Def19;
hence thesis;
end;
end;
registration
let V be non empty finite set, E be finite set, S,T be Function of E,V;
cluster createGraph(V,E,S,T) -> _finite;
coherence by FINSEQ_4:76;
end;
registration
let V be non empty set, E be empty set,S,T be Function of E,V;
cluster createGraph(V,E,S,T) -> simple;
coherence
proof
set G = createGraph(V,E,S,T);
the_Edges_of G = E by FINSEQ_4:76;
then
for e1,e2,v1,v2 be object st e1 Joins v1,v2,G & e2 Joins v1,v2,G
holds e1 = e2;
then
A1: G is non-multi;
not ex e being object st e in the_Edges_of G & (the_Source_of G).e = (
the_Target_of G).e by FINSEQ_4:76;
then G is loopless;
hence thesis by A1;
end;
end;
registration
let v be set, E be set, S,T be Function of E,{v};
cluster createGraph({v},E,S,T) -> _trivial;
coherence
proof
set G = createGraph({v},E,S,T);
the_Vertices_of G = {v} by FINSEQ_4:76;
then card the_Vertices_of G = 1 by CARD_1:30;
hence thesis;
end;
end;
definition
let G be _Graph;
func G.order() -> Cardinal equals
card the_Vertices_of G;
coherence;
end;
definition
let G be _finite _Graph;
redefine func G.order() -> non zero Element of NAT;
coherence
proof
G.order() = card the_Vertices_of G;
hence thesis;
end;
end;
definition
let G be _Graph;
func G.size() -> Cardinal equals
card the_Edges_of G;
coherence;
end;
definition
let G be _finite _Graph;
redefine func G.size() -> Element of NAT;
coherence
proof
G.size() = card the_Edges_of G;
hence thesis;
end;
end;
definition
let G be _Graph, X be set;
func G.edgesInto(X) -> Subset of the_Edges_of G means
:Def26:
for e being
set holds e in it iff e in the_Edges_of G & (the_Target_of G).e in X;
existence
proof
defpred P[set] means (the_Target_of G).$1 in X;
consider IT being Subset of the_Edges_of G such that
A1: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
thus thesis by A1;
end;
uniqueness
proof
let IT1, IT2 be Subset of the_Edges_of G such that
A2: for e being set holds e in IT1 iff e in the_Edges_of G & (
the_Target_of G).e in X and
A3: for e being set holds e in IT2 iff e in the_Edges_of G & (
the_Target_of G).e in X;
now
let e be object;
hereby
assume
A4: e in IT1;
then (the_Target_of G).e in X by A2;
hence e in IT2 by A3,A4;
end;
assume
A5: e in IT2;
then (the_Target_of G).e in X by A3;
hence e in IT1 by A2,A5;
end;
hence thesis by TARSKI:2;
end;
func G.edgesOutOf(X) -> Subset of the_Edges_of G means
:Def27:
for e being
set holds e in it iff e in the_Edges_of G & (the_Source_of G).e in X;
existence
proof
defpred P[set] means (the_Source_of G).$1 in X;
consider IT being Subset of the_Edges_of G such that
A6: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
thus thesis by A6;
end;
uniqueness
proof
let IT1, IT2 be Subset of the_Edges_of G such that
A7: for e being set holds e in IT1 iff e in the_Edges_of G & (
the_Source_of G).e in X and
A8: for e being set holds e in IT2 iff e in the_Edges_of G & (
the_Source_of G).e in X;
now
let e be object;
hereby
assume
A9: e in IT1;
then (the_Source_of G).e in X by A7;
hence e in IT2 by A8,A9;
end;
assume
A10: e in IT2;
then (the_Source_of G).e in X by A8;
hence e in IT1 by A7,A10;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let G be _Graph, X be set;
func G.edgesInOut(X) -> Subset of the_Edges_of G equals
G.edgesInto(X) \/ G.edgesOutOf(X);
coherence;
func G.edgesBetween(X) -> Subset of the_Edges_of G equals
G.edgesInto(X) /\ G.edgesOutOf(X);
coherence;
end;
definition
let G be _Graph, X,Y be set;
func G.edgesBetween(X,Y) -> Subset of the_Edges_of G means
:Def30:
for e being object holds e in it iff e SJoins X,Y,G;
existence
proof
defpred P[object] means $1 SJoins X,Y,G;
consider IT being Subset of the_Edges_of G such that
A1: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
let e be object;
thus e in IT implies P[e] by A1;
assume
A2: e SJoins X,Y,G;
thus thesis by A1,A2;
end;
uniqueness
proof
let IT1,IT2 being Subset of the_Edges_of G such that
A3: for e being object holds e in IT1 iff e SJoins X,Y,G and
A4: for e being object holds e in IT2 iff e SJoins X,Y,G;
for e being object holds e in IT2 iff e in IT1 by A3,A4;
hence thesis by TARSKI:2;
end;
func G.edgesDBetween(X,Y) -> Subset of the_Edges_of G means
:Def31:
for e being object holds e in it iff e DSJoins X,Y,G;
existence
proof
defpred P[object] means $1 DSJoins X,Y,G;
consider IT being Subset of the_Edges_of G such that
A5: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
let e be object;
thus e in IT implies P[e] by A5;
assume
A6: e DSJoins X,Y,G;
thus thesis by A5,A6;
end;
uniqueness
proof
let IT1,IT2 being Subset of the_Edges_of G such that
A7: for e being object holds e in IT1 iff e DSJoins X,Y,G and
A8: for e being object holds e in IT2 iff e DSJoins X,Y,G;
for e being object holds e in IT2 iff e in IT1 by A7,A8;
hence thesis by TARSKI:2;
end;
end;
scheme
FinGraphOrderInd{P[_Graph]}: for G being _finite _Graph holds P[G]
provided
A1: for G being _finite _Graph st G.order() = 1 holds P[G] and
A2: for k being non zero Nat st (for Gk being _finite _Graph st Gk
.order() = k holds P[Gk]) holds
for Gk1 being _finite _Graph st Gk1.order() = k+1 holds P[Gk1]
proof
defpred P2[Nat] means for G being _finite _Graph st G.order()=$1 holds P[G];
A3: for k being non zero Nat st P2[k] holds P2[k+1] by A2;
let G be _finite _Graph;
A4: G.order() = G.order();
A5: P2[1] by A1;
for k being non zero Nat holds P2[k] from NAT_1:sch 10(A5,A3);
hence thesis by A4;
end;
scheme
FinGraphSizeInd{P[_Graph]}: for G being _finite _Graph holds P[G]
provided
A1: for G being _finite _Graph st G.size() = 0 holds P[G] and
A2: for k being Nat st
(for Gk being _finite _Graph st Gk.size() = k holds P[Gk]) holds
for Gk1 being _finite _Graph st Gk1.size() = k+1
holds P[Gk1]
proof
defpred P2[Nat] means for G being _finite _Graph st G.size()=$1
holds P[G];
A3: for k being Nat st P2[k] holds P2[k+1] by A2;
let G be _finite _Graph;
A4: G.size() = G.size();
A5: P2[ 0 ] by A1;
for k being Nat holds P2[k] from NAT_1:sch 2(A5,A3);
hence thesis by A4;
end;
definition
let G be _Graph;
mode Subgraph of G -> _Graph means
:Def32:
the_Vertices_of it c= the_Vertices_of G &
the_Edges_of it c= the_Edges_of G & for e being set st e in
the_Edges_of it holds (the_Source_of it).e = (the_Source_of G).e & (
the_Target_of it).e = (the_Target_of G).e;
existence
proof
take G;
thus thesis;
end;
end;
definition
let G1 be _Graph, G2 be Subgraph of G1;
redefine func the_Vertices_of G2 -> non empty Subset of the_Vertices_of G1;
coherence by Def32;
redefine func the_Edges_of G2 -> Subset of the_Edges_of G1;
coherence by Def32;
end;
registration
let G be _Graph;
cluster _trivial simple for Subgraph of G;
existence
proof
set v = the Element of the_Vertices_of G;
set V = {v}, E = {};
reconsider S = {} as Function of E,V by RELSET_1:12;
set IT = createGraph(V,E,S,S);
A1: the_Vertices_of IT = {v} & for e being set st e in the_Edges_of IT
holds ( the_Source_of IT).e = (the_Source_of G).e & (the_Target_of IT).e = (
the_Target_of G).e by FINSEQ_4:76;
the_Edges_of IT = {} by FINSEQ_4:76;
then the_Edges_of IT c= the_Edges_of G;
then reconsider IT as Subgraph of G by A1,Def32;
take IT;
thus thesis;
end;
end;
Lm3: for G being _Graph holds G is Subgraph of G
proof
let G be _Graph;
for e being set st e in the_Edges_of G holds (the_Source_of G).e = (
the_Source_of G).e & (the_Target_of G).e = (the_Target_of G).e;
hence thesis by Def32;
end;
Lm4: for G1 being _Graph, G2 being Subgraph of G1,
x,y,e being object holds e
Joins x,y,G2 implies e Joins x,y,G1
proof
let G1 be _Graph, G2 be Subgraph of G1, x,y,e be object;
assume
A1: e Joins x,y,G2;
then
A2: e in the_Edges_of G2;
(the_Source_of G2).e = x & (the_Target_of G2).e = y or ( the_Source_of
G2).e = y & (the_Target_of G2).e = x by A1;
then (the_Source_of G1).e = x & (the_Target_of G1).e = y or ( the_Source_of
G1).e = y & (the_Target_of G1).e = x by A2,Def32;
hence thesis by A2;
end;
registration
let G be _finite _Graph;
cluster -> _finite for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
the_Vertices_of G2 is finite & the_Edges_of G2 is finite;
hence thesis;
end;
end;
registration
let G be loopless _Graph;
cluster -> loopless for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
now
given e being object such that
A1: e in the_Edges_of G2 and
A2: (the_Source_of G2).e = (the_Target_of G2).e;
(the_Source_of G2).e = (the_Source_of G).e & (the_Target_of G2).e =
( the_Target_of G).e by A1,Def32;
hence contradiction by A1,A2,Def18;
end;
hence thesis;
end;
end;
registration
let G be _trivial _Graph;
cluster -> _trivial for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
card the_Vertices_of G = 1 by Def19;
then consider v being object such that
A1: the_Vertices_of G = {v} by CARD_2:42;
the_Vertices_of G2 = {v} by A1,ZFMISC_1:33;
then card the_Vertices_of G2 = 1 by CARD_1:30;
hence thesis;
end;
end;
registration
let G be non-multi _Graph;
cluster -> non-multi for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
now
let e1,e2,v1,v2 be object;
assume e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2;
then e1 Joins v1,v2,G & e2 Joins v1,v2,G by Lm4;
hence e1 = e2 by Def20;
end;
hence thesis;
end;
end;
definition
let G1 be _Graph, G2 be Subgraph of G1;
attr G2 is spanning means
:Def33:
the_Vertices_of G2 = the_Vertices_of G1;
end;
registration
let G be _Graph;
cluster spanning for Subgraph of G;
existence
proof
reconsider G9=G as Subgraph of G by Lm3;
take G9;
thus thesis;
end;
end;
definition
let G1, G2 be _Graph;
pred G1 == G2 means
the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 &
the_Target_of G1 = the_Target_of G2;
reflexivity;
symmetry;
end;
notation
let G1,G2 be _Graph;
antonym G1 != G2 for G1 == G2;
end;
definition
let G1,G2 be _Graph;
pred G1 c= G2 means
G1 is Subgraph of G2;
reflexivity by Lm3;
end;
definition
let G1,G2 be _Graph;
pred G1 c< G2 means
G1 c= G2 & G1 != G2;
irreflexivity;
end;
definition
let G be _Graph, V, E be set;
mode inducedSubgraph of G,V,E -> Subgraph of G means
:Def37:
the_Vertices_of
it = V & the_Edges_of it = E if V is non empty Subset of the_Vertices_of G & E
c= G.edgesBetween(V) otherwise it == G;
existence
proof
hereby
assume that
A1: V is non empty Subset of the_Vertices_of G and
A2: E c= G.edgesBetween(V);
reconsider E9 = E as Subset of the_Edges_of G by A2,XBOOLE_1:1;
set S = (the_Source_of G) | E9, T = (the_Target_of G) | E9;
reconsider V9 = V as non empty Subset of the_Vertices_of G by A1;
dom the_Target_of G = the_Edges_of G by FUNCT_2:def 1;
then
A3: dom T = E9 by RELAT_1:62;
now
let e be object;
assume
A4: e in E9;
then e in G.edgesInto(V) by A2,XBOOLE_0:def 4;
then (the_Target_of G).e in V by Def26;
hence T.e in V by A4,FUNCT_1:49;
end;
then reconsider T as Function of E9,V9 by A3,FUNCT_2:3;
dom the_Source_of G = the_Edges_of G by FUNCT_2:def 1;
then
A5: dom S = E9 by RELAT_1:62;
now
let e be object;
assume
A6: e in E9;
then e in G.edgesOutOf(V) by A2,XBOOLE_0:def 4;
then (the_Source_of G).e in V by Def27;
hence S.e in V by A6,FUNCT_1:49;
end;
then reconsider S as Function of E9,V9 by A5,FUNCT_2:3;
set IT = createGraph(V9,E9,S,T);
A7: the_Edges_of IT = E by FINSEQ_4:76;
the_Source_of IT = S & the_Target_of IT = T by FINSEQ_4:76;
then the_Vertices_of IT = V & for e being set st e in the_Edges_of IT
holds ( the_Source_of IT).e = (the_Source_of G).e & (the_Target_of IT).e = (
the_Target_of G).e by A7,FINSEQ_4:76,FUNCT_1:49;
then reconsider IT as Subgraph of G by A7,Def32;
take IT;
thus the_Vertices_of IT = V & the_Edges_of IT = E by FINSEQ_4:76;
end;
G is Subgraph of G by Lm3;
hence thesis;
end;
consistency;
end;
definition
let G be _Graph, V be set;
mode inducedSubgraph of G,V is inducedSubgraph of G,V,G.edgesBetween(V);
end;
registration
let G be _Graph, V be finite non empty Subset of the_Vertices_of G, E be
finite Subset of G.edgesBetween(V);
cluster -> _finite for inducedSubgraph of G,V,E;
coherence by Def37;
end;
registration
let G be _Graph, v be Element of the_Vertices_of G, E be Subset of G
.edgesBetween({v});
cluster -> _trivial for inducedSubgraph of G,{v},E;
coherence
proof
let IT be inducedSubgraph of G,{v},E;
the_Vertices_of IT = {v} by Def37;
then card the_Vertices_of IT = 1 by CARD_1:30;
hence thesis;
end;
end;
registration
let G be _Graph, v be Element of the_Vertices_of G;
cluster -> _finite _trivial for inducedSubgraph of G,{v},{};
coherence
proof
reconsider E = {} as finite Subset of G.edgesBetween({v}) by XBOOLE_1:2;
let IT be inducedSubgraph of G,{v},{};
IT is inducedSubgraph of G,{v},E;
hence thesis;
end;
end;
registration
let G be _Graph, V be non empty Subset of the_Vertices_of G;
cluster -> simple for inducedSubgraph of G,V,{};
coherence
proof
let IT be inducedSubgraph of G,V,{};
reconsider E = {} as Subset of G.edgesBetween(V) by XBOOLE_1:2;
IT is inducedSubgraph of G,V,E;
then the_Edges_of IT = {} by Def37;
hence thesis by Lm2;
end;
end;
Lm5: for G being _Graph, e,X being set holds e in the_Edges_of G & (
the_Source_of G).e in X & (the_Target_of G).e in X iff e in G.edgesBetween(X)
proof
let G be _Graph, e,X be set;
hereby
assume
e in the_Edges_of G & (the_Source_of G).e in X & (the_Target_of G) .e in X;
then e in G.edgesInto(X) & e in G.edgesOutOf(X) by Def26,Def27;
hence e in G.edgesBetween(X) by XBOOLE_0:def 4;
end;
assume e in G.edgesBetween(X);
then e in G.edgesInto(X) & e in G.edgesOutOf(X) by XBOOLE_0:def 4;
hence thesis by Def26,Def27;
end;
Lm6: for G being _Graph holds the_Edges_of G = G.edgesBetween(the_Vertices_of
G)
proof
let G be _Graph;
set EG = the_Edges_of G, SG = the_Source_of G, TG = the_Target_of G;
now
let x be object;
hereby
assume
A1: x in EG;
then SG.x in the_Vertices_of G & TG.x in the_Vertices_of G by FUNCT_2:5;
hence x in G.edgesBetween(the_Vertices_of G) by A1,Lm5;
end;
assume x in G.edgesBetween(the_Vertices_of G);
hence x in EG;
end;
hence thesis by TARSKI:2;
end;
registration
let G be _Graph, E be Subset of the_Edges_of G;
cluster -> spanning for inducedSubgraph of G,the_Vertices_of G, E;
coherence
proof
let G1 be inducedSubgraph of G,the_Vertices_of G, E;
G.edgesBetween(the_Vertices_of G) = the_Edges_of G & the_Vertices_of G
c= the_Vertices_of G by Lm6;
then the_Vertices_of G1 = the_Vertices_of G by Def37;
hence thesis;
end;
end;
registration
let G be _Graph;
cluster -> spanning for inducedSubgraph of G,the_Vertices_of G,{};
coherence
proof
let G1 be inducedSubgraph of G,the_Vertices_of G,{};
the_Vertices_of G c= the_Vertices_of G & {} c= G.edgesBetween(
the_Vertices_of G);
then the_Vertices_of G1 = the_Vertices_of G by Def37;
hence thesis;
end;
end;
definition
let G be _Graph, v be set;
mode removeVertex of G,v is inducedSubgraph of G, the_Vertices_of G \ {v};
end;
definition
let G be _Graph, V be set;
mode removeVertices of G,V is inducedSubgraph of G, the_Vertices_of G \ V;
end;
definition
let G be _Graph, e be set;
mode removeEdge of G,e is inducedSubgraph of G, the_Vertices_of G,
the_Edges_of G \ {e};
end;
definition
let G be _Graph, E be set;
mode removeEdges of G,E is inducedSubgraph of G, the_Vertices_of G,
the_Edges_of G \ E;
end;
registration
let G be _Graph, e be set;
cluster -> spanning for removeEdge of G,e;
coherence;
end;
registration
let G be _Graph, E be set;
cluster -> spanning for removeEdges of G,E;
coherence;
end;
definition
let G be _Graph;
mode Vertex of G is Element of the_Vertices_of G;
end;
definition
let G be _Graph, v be Vertex of G;
func v.edgesIn() -> Subset of the_Edges_of G equals
G.edgesInto( {v} );
coherence;
func v.edgesOut() -> Subset of the_Edges_of G equals
G.edgesOutOf( {v} );
coherence;
func v.edgesInOut() -> Subset of the_Edges_of G equals
G.edgesInOut( {v} );
coherence;
end;
Lm7: for G being _Graph, v being Vertex of G, e being set holds e in v
.edgesIn() iff e in the_Edges_of G & (the_Target_of G).e = v
proof
let G be _Graph, v be Vertex of G, e be set;
hereby
assume
A1: e in v.edgesIn();
then (the_Target_of G).e in {v} by Def26;
hence e in the_Edges_of G & (the_Target_of G).e = v by A1,TARSKI:def 1;
end;
assume that
A2: e in the_Edges_of G and
A3: (the_Target_of G).e = v;
(the_Target_of G).e in {v} by A3,TARSKI:def 1;
hence thesis by A2,Def26;
end;
Lm8: for G being _Graph, v being Vertex of G, e being set holds e in v
.edgesOut() iff e in the_Edges_of G & (the_Source_of G).e = v
proof
let G be _Graph, v be Vertex of G, e be set;
hereby
assume
A1: e in v.edgesOut();
then (the_Source_of G).e in {v} by Def27;
hence e in the_Edges_of G & (the_Source_of G).e = v by A1,TARSKI:def 1;
end;
assume that
A2: e in the_Edges_of G and
A3: (the_Source_of G).e = v;
(the_Source_of G).e in {v} by A3,TARSKI:def 1;
hence thesis by A2,Def27;
end;
definition
let G be _Graph, v be Vertex of G, e be object;
func v.adj(e) -> Vertex of G equals
:Def41:
(the_Source_of G).e if e in
the_Edges_of G & (the_Target_of G).e = v, (the_Target_of G).e if e in
the_Edges_of G & (the_Source_of G).e = v & not (the_Target_of G).e = v
otherwise v;
coherence by FUNCT_2:5;
consistency;
end;
definition
let G be _Graph, v be Vertex of G;
func v.inDegree() -> Cardinal equals
card v.edgesIn();
coherence;
func v.outDegree() -> Cardinal equals
card v.edgesOut();
coherence;
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine func v.inDegree() -> Element of NAT;
coherence
proof
v.inDegree() = card v.edgesIn();
hence thesis;
end;
redefine func v.outDegree() -> Element of NAT;
coherence
proof
v.outDegree() = card v.edgesOut();
hence thesis;
end;
end;
definition
let G be _Graph, v be Vertex of G;
func v.degree() -> Cardinal equals
v.inDegree() +` v.outDegree();
coherence;
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine func v.degree() -> Element of NAT equals
v.inDegree() + v
.outDegree();
correctness
proof
v.degree() = card (v.inDegree() +^ v.outDegree()) by CARD_2:def 1
.= card (v.inDegree() + v.outDegree()) by CARD_2:36
.= v.inDegree() + v.outDegree();
hence thesis;
end;
end;
definition
let G be _Graph, v be Vertex of G;
func v.inNeighbors() -> Subset of the_Vertices_of G equals
(the_Source_of G)
.:v.edgesIn();
coherence;
func v.outNeighbors() -> Subset of the_Vertices_of G equals
(the_Target_of G
).:v.edgesOut();
coherence;
end;
definition
let G be _Graph, v be Vertex of G;
func v.allNeighbors() -> Subset of the_Vertices_of G equals
v.inNeighbors()
\/ v.outNeighbors();
coherence;
end;
definition
let G be _Graph, v being Vertex of G;
attr v is isolated means
v.edgesInOut() = {};
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine attr v is isolated means
v.degree() = 0;
compatibility
proof
hereby
assume v is isolated;
then
A1: v.edgesInOut() = {};
then v.inDegree() = 0 by CARD_1:27,XBOOLE_1:15;
hence v.degree() = 0 by A1,CARD_1:27,XBOOLE_1:15;
end;
assume
A2: v.degree() = 0;
then v.edgesIn() = {};
hence thesis by A2;
end;
end;
definition
let G be _Graph, v be Vertex of G;
attr v is endvertex means
ex e being object st v.edgesInOut() = {e} & not e Joins v,v,G;
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine attr v is endvertex means
v.degree() = 1;
compatibility
proof
hereby
assume v is endvertex;
then consider e being object such that
A1: v.edgesInOut() = {e} and
A2: not e Joins v,v,G;
now
per cases by A1,ZFMISC_1:37;
suppose
A3: v.edgesIn() = {e} & v.edgesOut() = {e};
then e in v.edgesOut() by TARSKI:def 1;
then
A4: (the_Source_of G).e = v by Lm8;
A5: e in v.edgesIn() by A3,TARSKI:def 1;
then (the_Target_of G).e = v by Lm7;
hence v.degree() = 1 by A2,A5,A4;
end;
suppose
v.edgesIn() = {} & v.edgesOut() = {e};
hence v.degree() = 1 by CARD_1:30;
end;
suppose
v.edgesIn() = {e} & v.edgesOut() = {};
hence v.degree() = 1 by CARD_1:30;
end;
end;
hence v.degree() = 1;
end;
assume
A6: v.degree() = 1;
now
per cases;
suppose
A7: card v.edgesIn() = 0;
then consider e being object such that
A8: v.edgesOut() = {e} by A6,CARD_2:42;
A9: v.edgesIn() = {} by A7;
then
A10: not e Joins v,v,G by Lm7;
v.edgesInOut() = {e} by A9,A8;
hence thesis by A10;
end;
suppose
card v.edgesIn() <> 0;
then 0 < card v.edgesIn();
then
A11: 0+1 <= card v.edgesIn() by NAT_1:13;
card v.edgesIn() <= 1 by A6,NAT_1:11;
then
A12: card v.edgesIn() = 1 by A11,XXREAL_0:1;
then consider e being object such that
A13: v.edgesIn() = {e} by CARD_2:42;
A14: v.edgesOut() = {} by A6,A12;
then
A15: not e Joins v,v,G by Lm8;
v.edgesInOut() = {e} by A13,A14;
hence thesis by A15;
end;
end;
hence thesis;
end;
end;
LmNat:
for F being ManySortedSet of NAT, n being object
holds n is Nat iff n in dom F
proof
let F be ManySortedSet of NAT, n being object;
hereby
assume n is Nat;
then n in NAT by ORDINAL1:def 12;
hence n in dom F by PARTFUN1:def 2;
end;
assume n in dom F;
hence n is Nat;
end;
definition
let F be Function;
attr F is Graph-yielding means
:Def53a:
for x being object st x in dom F holds F.x is _Graph;
end;
definition
let F be ManySortedSet of NAT;
redefine attr F is Graph-yielding means :Def53:
for n being Nat holds F.n is _Graph;
compatibility
proof
thus F is Graph-yielding implies for n be Nat holds F.n is _Graph by LmNat;
assume A2: for n being Nat holds F.n is _Graph;
let x be object;
assume x in dom F;
hence thesis by A2;
end;
attr F is halting means
ex n being Nat st F.n = F.(n+1);
end;
definition
let F be ManySortedSet of NAT;
func F.Lifespan() -> Element of NAT means
F.it = F.(it+1) & for n being Nat
st F.n = F.(n+1) holds it <= n if F is halting otherwise it = 0;
existence
proof
defpred P[Nat] means F.$1 = F.($1+1);
hereby
assume F is halting;
then
A1: ex n being Nat st P[n];
ex IT being Nat st P[IT] & for n being Nat st P[n] holds IT <= n
from NAT_1:sch 5(A1);
then consider IT being Nat such that
A2: ( P[IT])& for n being Nat st P[n] holds IT <= n;
IT in NAT by ORDINAL1:def 12;
hence
ex IT being Element of NAT st P[IT] & for n being Nat st P[n] holds
IT <= n by A2;
end;
thus thesis;
end;
uniqueness
proof
let IT1, IT2 be Element of NAT;
hereby
assume F is halting;
assume
A3: F.IT1 = F.(IT1+1) & for n being Nat st F.n = F.(n+1) holds IT1 <= n;
assume
F.IT2 = F.(IT2+1) & for n being Nat st F.n = F.(n+1) holds IT2 <= n;
then IT1 <= IT2 & IT2 <= IT1 by A3;
hence IT1 = IT2 by XXREAL_0:1;
end;
thus thesis;
end;
consistency;
end;
definition
let F be ManySortedSet of NAT;
func F.Result() -> set equals
F.(F.Lifespan());
coherence;
end;
registration
cluster empty -> Graph-yielding for Function;
coherence;
end;
registration
let G be _Graph;
cluster NAT --> G -> Graph-yielding;
coherence
proof
set F = NAT --> G;
A1: dom F = NAT;
reconsider F as ManySortedSet of NAT;
let x be Nat;
x in NAT by ORDINAL1:def 12;
then F.x in rng F by A1,FUNCT_1:3;
then F.x in {G} by FUNCOP_1:8;
hence thesis by TARSKI:def 1;
end;
end;
registration
cluster Graph-yielding for ManySortedSet of NAT;
existence
proof
set G = the _Graph;
set F = NAT --> G;
reconsider F as ManySortedSet of NAT;
take F;
thus thesis;
end;
end;
definition
mode GraphSeq is Graph-yielding ManySortedSet of NAT;
end;
registration
cluster -> non empty for GraphSeq;
coherence
proof
let GSeq be GraphSeq;
dom GSeq = NAT by PARTFUN1:def 2;
hence thesis;
end;
end;
registration
cluster non empty Graph-yielding for Function;
existence
proof
take the GraphSeq;
thus thesis;
end;
end;
registration
let GF be non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> Function-like Relation-like;
coherence by Def53a;
end;
registration
let GSq be GraphSeq, x be Nat;
cluster GSq.x -> Function-like Relation-like;
coherence by Def53;
end;
registration
let GF be non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> NAT -defined finite;
coherence by Def53a;
end;
registration
let GSq be GraphSeq, x be Nat;
cluster GSq.x -> NAT -defined finite;
coherence by Def53;
end;
registration
let GF be non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> [Graph-like];
coherence by Def53a;
end;
registration
let GSq be GraphSeq, x be Nat;
cluster GSq.x -> [Graph-like];
coherence by Def53;
end;
definition
let GF be Graph-yielding Function;
attr GF is _finite means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is _finite;
attr GF is loopless means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is loopless;
attr GF is _trivial means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is _trivial;
attr GF is non-trivial means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is non _trivial;
attr GF is non-multi means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is non-multi;
attr GF is non-Dmulti means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is non-Dmulti;
attr GF is simple means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is simple;
attr GF is Dsimple means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is Dsimple;
end;
registration
cluster empty -> _finite loopless _trivial non-trivial non-multi
non-Dmulti simple Dsimple for Graph-yielding Function;
coherence;
end;
definition
let GF be non empty Graph-yielding Function;
redefine attr GF is _finite means
:Def57b:
for x being Element of dom GF holds GF.x is _finite;
compatibility
proof
hereby
assume A1: GF is _finite;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is _finite by A1;
thus GF.x is _finite by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is _finite;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
redefine attr GF is loopless means
:Def58b:
for x being Element of dom GF holds GF.x is loopless;
compatibility
proof
hereby
assume A1: GF is loopless;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is loopless by A1;
thus GF.x is loopless by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is loopless;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
redefine attr GF is _trivial means
:Def59b:
for x being Element of dom GF holds GF.x is _trivial;
compatibility
proof
hereby
assume A1: GF is _trivial;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is _trivial by A1;
thus GF.x is _trivial by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is _trivial;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
redefine attr GF is non-trivial means
:Def60b:
for x being Element of dom GF holds GF.x is non _trivial;
compatibility
proof
hereby
assume A1: GF is non-trivial;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is non _trivial by A1;
thus GF.x is non _trivial by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is non _trivial;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
redefine attr GF is non-multi means
:Def61b:
for x being Element of dom GF holds GF.x is non-multi;
compatibility
proof
hereby
assume A1: GF is non-multi;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is non-multi by A1;
thus GF.x is non-multi by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is non-multi;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
redefine attr GF is non-Dmulti means
:Def62b:
for x being Element of dom GF holds GF.x is non-Dmulti;
compatibility
proof
hereby
assume A1: GF is non-Dmulti;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is non-Dmulti by A1;
thus GF.x is non-Dmulti by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is non-Dmulti;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
redefine attr GF is simple means
:Def63b:
for x being Element of dom GF holds GF.x is simple;
compatibility
proof
hereby
assume A1: GF is simple;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is simple by A1;
thus GF.x is simple by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is simple;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
redefine attr GF is Dsimple means
:Def64b:
for x being Element of dom GF holds GF.x is Dsimple;
compatibility
proof
hereby
assume A1: GF is Dsimple;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is Dsimple by A1;
thus GF.x is Dsimple by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is Dsimple;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is _finite means
:Def57:
for x being Nat holds GSq.x is _finite;
compatibility
proof
hereby
assume A1: GSq is _finite;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is _finite by A1;
end;
assume A2: for x being Nat holds GSq.x is _finite;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is loopless means
:Def58:
for x being Nat holds GSq.x is loopless;
compatibility
proof
hereby
assume A1: GSq is loopless;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is loopless by A1;
end;
assume A2: for x being Nat holds GSq.x is loopless;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is _trivial means
:Def59:
for x being Nat holds GSq.x is _trivial;
compatibility
proof
hereby
assume A1: GSq is _trivial;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is _trivial by A1;
end;
assume A2: for x being Nat holds GSq.x is _trivial;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is non-trivial means
:Def60:
for x being Nat holds GSq.x is non _trivial;
compatibility
proof
hereby
assume A1: GSq is non-trivial;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is non _trivial by A1;
end;
assume A2: for x being Nat holds GSq.x is non _trivial;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is non-multi means
:Def61:
for x being Nat holds GSq.x is non-multi;
compatibility
proof
hereby
assume A1: GSq is non-multi;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is non-multi by A1;
end;
assume A2: for x being Nat holds GSq.x is non-multi;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is non-Dmulti means
:Def62:
for x being Nat holds GSq.x is non-Dmulti;
compatibility
proof
hereby
assume A1: GSq is non-Dmulti;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is non-Dmulti by A1;
end;
assume A2: for x being Nat holds GSq.x is non-Dmulti;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is simple means
:Def63:
for x being Nat holds GSq.x is simple;
compatibility
proof
hereby
assume A1: GSq is simple;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is simple by A1;
end;
assume A2: for x being Nat holds GSq.x is simple;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is Dsimple means
:Def64:
for x being Nat holds GSq.x is Dsimple;
compatibility
proof
hereby
assume A1: GSq is Dsimple;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is Dsimple by A1;
end;
assume A2: for x being Nat holds GSq.x is Dsimple;
let x be Element of dom GSq;
thus thesis by A2;
end;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is halting means
ex n being Nat st GSq.n = GSq.(n+1);
compatibility;
end;
registration
cluster halting _finite loopless _trivial non-multi non-Dmulti
simple Dsimple for GraphSeq;
existence
proof
set G = the _finite loopless _trivial non-multi
non-Dmulti simple Dsimple _Graph;
set F = NAT --> G;
reconsider F as ManySortedSet of NAT;
reconsider F as GraphSeq;
A2: F.(1+1) = G;
take F;
F.1 = G;
hence F is halting by A2;
thus thesis;
end;
cluster halting _finite loopless non-trivial non-multi non-Dmulti simple
Dsimple for GraphSeq;
existence
proof
set G = the _finite loopless non _trivial non-multi non-Dmulti
simple Dsimple _Graph;
set F = NAT --> G;
reconsider F as ManySortedSet of NAT;
reconsider F as GraphSeq;
A4: F.(1+1) = G;
take F;
F.1 = G;
hence F is halting by A4;
thus thesis;
end;
end;
registration
let GF be _finite non empty Graph-yielding Function,
x be Element of dom GF;
cluster GF.x -> _finite;
coherence by Def57b;
end;
registration
let GSq be _finite GraphSeq, x be Nat;
cluster GSq.x -> _finite;
coherence by Def57;
end;
registration
let GF be loopless non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> loopless;
coherence by Def58b;
end;
registration
let GSq be loopless GraphSeq, x be Nat;
cluster GSq.x -> loopless for _Graph;
coherence by Def58;
end;
registration
let GF be _trivial non empty Graph-yielding Function,
x be Element of dom GF;
cluster GF.x -> _trivial;
coherence by Def59b;
end;
registration
let GSq be _trivial GraphSeq, x be Nat;
cluster GSq.x -> _trivial for _Graph;
coherence by Def59;
end;
registration
let GF be non-trivial non empty Graph-yielding Function;
let x be Element of dom GF;
cluster GF.x -> non _trivial;
coherence by Def60b;
end;
registration
let GSq be non-trivial GraphSeq, x be Nat;
cluster GSq.x -> non _trivial for _Graph;
coherence by Def60;
end;
registration
let GF be non-multi non empty Graph-yielding Function;
let x be Element of dom GF;
cluster GF.x -> non-multi;
coherence by Def61b;
end;
registration
let GSq be non-multi GraphSeq, x be Nat;
cluster GSq.x -> non-multi for _Graph;
coherence by Def61;
end;
registration
let GF be non-Dmulti non empty Graph-yielding Function;
let x be Element of dom GF;
cluster GF.x -> non-Dmulti;
coherence by Def62b;
end;
registration
let GSq be non-Dmulti GraphSeq, x be Nat;
cluster GSq.x -> non-Dmulti for _Graph;
coherence by Def62;
end;
registration
let GF be simple non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> simple;
coherence by Def63b;
end;
registration
let GSq be simple GraphSeq, x be Nat;
cluster GSq.x -> simple for _Graph;
coherence by Def63;
end;
registration
let GF be Dsimple non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> Dsimple;
coherence by Def64b;
end;
registration
let GSq be Dsimple GraphSeq, x be Nat;
cluster GSq.x -> Dsimple for _Graph;
coherence by Def64;
end;
registration
cluster non-multi -> non-Dmulti for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster simple -> loopless non-multi for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster loopless non-multi -> simple for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster loopless non-Dmulti -> Dsimple for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster Dsimple -> loopless non-Dmulti for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster _trivial loopless -> _finite for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster _trivial non-Dmulti -> _finite for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
begin :: Theorems
reserve GS for GraphStruct;
reserve G,G1,G2,G3 for _Graph;
reserve e,x,x1,x2,y,y1,y2,E,V,X,Y for set;
reserve n,n1,n2 for Nat;
reserve v,v1,v2 for Vertex of G;
theorem
VertexSelector = 1 & EdgeSelector = 2 & SourceSelector = 3 &
TargetSelector = 4;
theorem
_GraphSelectors c= dom G
proof
let x be object;
assume x in _GraphSelectors;
then x = VertexSelector or x = EdgeSelector or x = SourceSelector or x =
TargetSelector by ENUMSET1:def 2;
hence x in dom G by Def10;
end;
theorem
the_Vertices_of GS = GS.VertexSelector & the_Edges_of GS = GS.
EdgeSelector & the_Source_of GS = GS.SourceSelector & the_Target_of GS = GS.
TargetSelector;
theorem
dom (the_Source_of G) = the_Edges_of G & dom (the_Target_of G) =
the_Edges_of G & rng (the_Source_of G) c= the_Vertices_of G & rng (
the_Target_of G) c= the_Vertices_of G by FUNCT_2:def 1;
theorem
GS is [Graph-like] iff _GraphSelectors c= dom GS & the_Vertices_of GS
is non empty & the_Source_of GS is Function of the_Edges_of GS,the_Vertices_of
GS & the_Target_of GS is Function of the_Edges_of GS,the_Vertices_of GS by Lm1;
theorem ::: obsolete as reductions are added
for V being non empty set, E being set, S,T being Function of E,V holds
the_Vertices_of createGraph(V,E,S,T) = V &
the_Edges_of createGraph(V,E,S,T) = E &
the_Source_of createGraph(V,E,S,T) = S &
the_Target_of createGraph(V,E,S,T) = T by FINSEQ_4:76;
registration
let V be non empty set, E be set, S,T be Function of E,V;
reduce the_Vertices_of createGraph(V,E,S,T) to V;
reducibility by FINSEQ_4:76;
reduce the_Edges_of createGraph(V,E,S,T) to E;
reducibility by FINSEQ_4:76;
reduce the_Source_of createGraph(V,E,S,T) to S;
reducibility by FINSEQ_4:76;
reduce the_Target_of createGraph(V,E,S,T) to T;
reducibility by FINSEQ_4:76;
end;
theorem Th7:
dom GS.set(n,x) = dom GS \/ {n}
proof
set G2 = GS.set(n,x);
thus dom G2 = dom GS \/ dom (n.-->x) by FUNCT_4:def 1
.= dom GS \/ {n};
end;
theorem Th8:
GS.set(n,x).n = x
proof
set G2 = GS.set(n,x);
n in dom (n.-->x) by TARSKI:def 1;
hence G2.n = (n.-->x).n by FUNCT_4:13
.= x by FUNCOP_1:72;
end;
theorem Th9:
n1 <> n2 implies GS.n2 = GS.set(n1,x).n2
proof
assume n1 <> n2;
then not n2 in dom (n1.-->x) by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
not n in _GraphSelectors implies the_Vertices_of G = the_Vertices_of G
.set(n,x) & the_Edges_of G = the_Edges_of G.set(n,x) & the_Source_of G =
the_Source_of G.set(n,x) & the_Target_of G = the_Target_of G.set(n,x) & G.set(n
,x) is _Graph
proof
set G2 = G.set(n,x);
A1: dom G c= dom G2 by FUNCT_4:10;
assume
A2: not n in _GraphSelectors;
then EdgeSelector <> n by ENUMSET1:def 2;
then
A3: not EdgeSelector in dom (n .--> x) by TARSKI:def 1;
TargetSelector <> n by A2,ENUMSET1:def 2;
then
A4: not TargetSelector in dom (n .--> x) by TARSKI:def 1;
SourceSelector <> n by A2,ENUMSET1:def 2;
then
A5: not SourceSelector in dom (n .--> x) by TARSKI:def 1;
VertexSelector <> n by A2,ENUMSET1:def 2;
then not VertexSelector in dom (n .--> x) by TARSKI:def 1;
hence
A6: the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 =
the_Edges_of G & the_Source_of G2 = the_Source_of G & the_Target_of G2 =
the_Target_of G by A3,A5,A4,FUNCT_4:11;
A7: SourceSelector in dom G & TargetSelector in dom G by Def10;
VertexSelector in dom G & EdgeSelector in dom G by Def10;
hence thesis by A7,A1,A6,Def10;
end;
theorem
the_Vertices_of GS.set(VertexSelector,x) = x & the_Edges_of GS.set(
EdgeSelector,x) = x & the_Source_of GS.set(SourceSelector,x) = x &
the_Target_of GS.set(TargetSelector,x) = x by Th8;
theorem
n1 <> n2 implies n1 in dom GS.set(n1,x).set(n2,y) & n2 in dom GS.set(
n1,x).set(n2,y) & GS.set(n1,x).set(n2,y).n1 = x & GS.set(n1,x).set(n2,y).n2 = y
proof
assume
A1: n1 <> n2;
set G2 = GS.set(n1,x), G3 = G2.set(n2,y);
A2: dom G3 = dom G2 \/ {n2} by Th7;
dom G2 = dom GS \/ {n1} & n1 in {n1} by Th7,TARSKI:def 1;
then n1 in dom G2 by XBOOLE_0:def 3;
hence n1 in dom GS.set(n1,x).set(n2,y) by A2,XBOOLE_0:def 3;
n2 in {n2} by TARSKI:def 1;
hence n2 in dom GS.set(n1,x).set(n2,y) by A2,XBOOLE_0:def 3;
thus GS.set(n1,x).set(n2,y).n1 = G2.n1 by A1,Th9
.= x by Th8;
thus thesis by Th8;
end;
theorem
for e,x,y being object holds
e Joins x,y,G implies x in the_Vertices_of G & y in the_Vertices_of G
by FUNCT_2:5;
theorem
for e,x,y being object holds
e Joins x,y,G implies e Joins y,x,G;
theorem
for e,x1,x2,y1,y2 being object holds
e Joins x1,y1,G & e Joins x2,y2,G implies x1 = x2 & y1 = y2 or x1 = y2
& y1 = x2;
theorem
for e,x,y being object holds
e Joins x,y,G iff (e DJoins x,y,G or e DJoins y,x,G);
theorem
for e,x,y being object st
e Joins x,y,G & ( x in X & y in Y or x in Y & y in X ) holds
e SJoins X,Y,G;
theorem
G is loopless iff for v being object holds
not ex e being object st e Joins v,v,G
proof
thus G is loopless implies for v being object
holds not ex e being object st e Joins v,v,G;
assume
A1: for v being object holds not ex e being object st e Joins v,v,G;
now
given e being object such that
A2: e in the_Edges_of G & (the_Source_of G).e = (the_Target_of G).e;
set v = (the_Source_of G).e;
e Joins v,v,G by A2;
hence contradiction by A1;
end;
hence thesis;
end;
theorem
for G being loopless _Graph, v being Vertex of G holds
v.degree() = card v.edgesInOut()
proof
let G be loopless _Graph, v be Vertex of G;
set In = v.edgesIn(), Out = v.edgesOut();
now
given e being object such that
A1: e in In /\ Out;
e in Out by A1,XBOOLE_0:def 4;
then
A2: (the_Source_of G).e = v by Lm8;
e in In by A1,XBOOLE_0:def 4;
then (the_Target_of G).e = v by Lm7;
hence contradiction by A1,A2,Def18;
end;
then In /\ Out = {} by XBOOLE_0:def 1;
then In misses Out by XBOOLE_0:def 7;
hence thesis by CARD_2:35;
end;
theorem
for G being non _trivial _Graph, v being Vertex of G holds
(the_Vertices_of G) \ {v} is non empty
proof
let G be non _trivial _Graph, v be Vertex of G;
set VG = the_Vertices_of G;
now
assume VG \ {v} = {};
then VG c= {v} by XBOOLE_1:37;
then VG = {v} by ZFMISC_1:33;
then card VG = 1 by CARD_1:30;
hence contradiction by Def19;
end;
hence thesis;
end;
theorem
for G being non _trivial _Graph holds ex v1, v2 being Vertex of G st v1 <> v2
proof
let G be non _trivial _Graph;
set VG = the_Vertices_of G;
take v1 = the Element of VG;
set VG2 = VG \ {v1};
now
assume
A1: VG2 = {};
card (VG2 \/ {v1}) = card VG2 +` card {v1} by CARD_2:35,XBOOLE_1:79
.= 0 +` 1 by A1,CARD_1:30
.= card (0 +^ 1) by CARD_2:def 1
.= card (0+1) by CARD_2:36
.= 1;
then card VG = 1 by XBOOLE_1:45;
hence contradiction by Def19;
end;
then reconsider VG2 as non empty set;
set v2 = the Element of VG2;
A2: not v2 in {v1} by XBOOLE_0:def 5;
reconsider v2 as Vertex of G by XBOOLE_0:def 5;
take v2;
thus thesis by A2,TARSKI:def 1;
end;
theorem Th22:
for G being _trivial _Graph holds ex v being Vertex of G st
the_Vertices_of G = {v}
proof
let G be _trivial _Graph;
card (the_Vertices_of G) = 1 by Def19;
then consider v being object such that
A1: the_Vertices_of G = {v} by CARD_2:42;
reconsider v as Vertex of G by A1,TARSKI:def 1;
take v;
thus thesis by A1;
end;
theorem
for G being _trivial loopless _Graph holds the_Edges_of G = {}
proof
let G be _trivial loopless _Graph;
consider v being Vertex of G such that
A1: the_Vertices_of G = {v} by Th22;
now
assume the_Edges_of G <> {};
then consider e being object such that
A2: e in the_Edges_of G by XBOOLE_0:def 1;
(the_Target_of G).e in {v} by A1,A2,FUNCT_2:5;
then
A3: (the_Target_of G).e = v by TARSKI:def 1;
(the_Source_of G).e in {v} by A1,A2,FUNCT_2:5;
then (the_Source_of G).e = v by TARSKI:def 1;
hence contradiction by A2,A3,Def18;
end;
hence thesis;
end;
theorem
the_Edges_of G = {} implies G is simple
proof
assume
A1: the_Edges_of G = {};
then
A2: G is loopless;
for e1,e2,v1,v2 being object holds e1 Joins v1,v2,G & e2 Joins v1,v2,G
implies e1 = e2 by A1;
then G is non-multi;
hence thesis by A2;
end;
theorem
for G being _finite _Graph holds G.order() >= 1
proof
let G be _finite _Graph;
0+1 < G.order()+1 by NAT_1:3,XREAL_1:8;
hence thesis by NAT_1:13;
end;
theorem
for G being _Graph holds G.order() = 1 iff G is _trivial;
theorem
for G being _Graph holds G.order() = 1 iff ex v being Vertex of
G st the_Vertices_of G = {v}
proof
let G be _Graph;
hereby
assume G.order() = 1;
then consider v being object such that
A1: the_Vertices_of G = {v} by CARD_2:42;
reconsider v as Vertex of G by A1,TARSKI:def 1;
take v;
thus the_Vertices_of G = {v} by A1;
end;
given v being Vertex of G such that
A2: the_Vertices_of G = {v};
thus thesis by A2,CARD_1:30;
end;
theorem Th28:
e in the_Edges_of G & ((the_Source_of G).e in X or
(the_Target_of G).e in X) iff e in G.edgesInOut(X)
proof
hereby
assume that
A1: e in the_Edges_of G and
A2: (the_Source_of G).e in X or (the_Target_of G).e in X;
now
per cases by A2;
suppose
(the_Source_of G).e in X;
then e in G.edgesOutOf(X) by A1,Def27;
hence e in G.edgesInOut(X) by XBOOLE_0:def 3;
end;
suppose
(the_Target_of G).e in X;
then e in G.edgesInto(X) by A1,Def26;
hence e in G.edgesInOut(X) by XBOOLE_0:def 3;
end;
end;
hence e in G.edgesInOut(X);
end;
assume e in G.edgesInOut(X);
then e in G.edgesInto(X) or e in G.edgesOutOf(X) by XBOOLE_0:def 3;
hence thesis by Def26,Def27;
end;
theorem
G.edgesInto(X) c= G.edgesInOut(X) & G.edgesOutOf(X) c= G.edgesInOut(X)
by XBOOLE_0:def 3;
theorem
the_Edges_of G = G.edgesInOut(the_Vertices_of G)
proof
set EG = the_Edges_of G, SG = the_Source_of G;
now
let x be object;
hereby
assume
A1: x in EG;
then SG.x in the_Vertices_of G by FUNCT_2:5;
hence x in G.edgesInOut(the_Vertices_of G) by A1,Th28;
end;
assume x in G.edgesInOut(the_Vertices_of G);
hence x in EG;
end;
hence thesis by TARSKI:2;
end;
theorem
e in the_Edges_of G & (the_Source_of G).e in X & (the_Target_of G).e
in X iff e in G.edgesBetween(X) by Lm5;
theorem
for e,x,y being object holds
x in X & y in X & e Joins x,y,G implies e in G.edgesBetween(X) by Lm5;
theorem
G.edgesBetween(X) c= G.edgesInOut(X)
proof
let z be object;
assume z in G.edgesBetween(X);
then z in G.edgesInto(X) by XBOOLE_0:def 4;
hence z in G.edgesInOut(X) by XBOOLE_0:def 3;
end;
theorem Th34:
the_Edges_of G = G.edgesBetween(the_Vertices_of G)
proof
set EG = the_Edges_of G, SG = the_Source_of G, TG = the_Target_of G;
now
let x be object;
hereby
assume
A1: x in EG;
then SG.x in the_Vertices_of G & TG.x in the_Vertices_of G by FUNCT_2:5;
hence x in G.edgesBetween(the_Vertices_of G) by A1,Lm5;
end;
assume x in G.edgesBetween(the_Vertices_of G);
hence x in EG;
end;
hence thesis by TARSKI:2;
end;
theorem Th35:
(the_Edges_of G) \ (G.edgesInOut(X)) = G.edgesBetween( (
the_Vertices_of G) \ X)
proof
set EG = the_Edges_of G, VG = the_Vertices_of G;
set EIO = G.edgesInOut(X), EB = G.edgesBetween(VG\X);
now
let x be object;
hereby
assume
A1: x in EG \ EIO;
then
A2: (the_Target_of G).x in VG by FUNCT_2:5;
A3: not x in EIO by A1,XBOOLE_0:def 5;
then not (the_Target_of G).x in X by A1,Th28;
then
A4: (the_Target_of G).x in VG \ X by A2,XBOOLE_0:def 5;
A5: (the_Source_of G).x in VG by A1,FUNCT_2:5;
not (the_Source_of G).x in X by A1,A3,Th28;
then (the_Source_of G).x in VG \ X by A5,XBOOLE_0:def 5;
hence x in EB by A1,A4,Lm5;
end;
assume
A6: x in EB;
then (the_Target_of G).x in VG \ X by Lm5;
then
A7: not (the_Target_of G).x in X by XBOOLE_0:def 5;
(the_Source_of G).x in VG \ X by A6,Lm5;
then not (the_Source_of G).x in X by XBOOLE_0:def 5;
then not x in EIO by A7,Th28;
hence x in EG\EIO by A6,XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem
X c= Y implies G.edgesBetween(X) c= G.edgesBetween(Y)
proof
assume
A1: X c= Y;
let x be object;
assume
A2: x in G.edgesBetween(X);
then (the_Source_of G).x in X & (the_Target_of G).x in X by Lm5;
hence x in G.edgesBetween(Y) by A1,A2,Lm5;
end;
theorem
for G being _Graph, X1,X2,Y1,Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G.edgesBetween(X1,Y1) c= G.edgesBetween(X2,Y2)
proof
let G be _Graph, X1,X2,Y1,Y2 be set;
assume
A1: X1 c= X2 & Y1 c= Y2;
let e be object;
assume e in G.edgesBetween(X1,Y1);
then e SJoins X1,Y1,G by Def30;
then e SJoins X2,Y2,G by A1;
hence e in G.edgesBetween(X2,Y2) by Def30;
end;
theorem
for G being _Graph, X1,X2,Y1,Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G.edgesDBetween(X1,Y1) c= G.edgesDBetween(X2,Y2)
proof
let G be _Graph, X1,X2,Y1,Y2 be set;
assume
A1: X1 c= X2 & Y1 c= Y2;
let e be object;
assume e in G.edgesDBetween(X1,Y1);
then e DSJoins X1,Y1,G by Def31;
then e DSJoins X2,Y2,G by A1;
hence e in G.edgesDBetween(X2,Y2) by Def31;
end;
theorem
for G being _Graph, v being Vertex of G holds v.edgesIn() = G
.edgesDBetween(the_Vertices_of G, {v}) & v.edgesOut() = G.edgesDBetween({v},
the_Vertices_of G)
proof
let G be _Graph, v be Vertex of G;
now
let e be object;
hereby
assume
A1: e in v.edgesIn();
then (the_Target_of G).e = v by Lm7;
then
A2: (the_Target_of G).e in {v} by TARSKI:def 1;
(the_Source_of G).e in the_Vertices_of G by A1,FUNCT_2:5;
then e DSJoins the_Vertices_of G,{v},G by A1,A2;
hence e in G.edgesDBetween(the_Vertices_of G, {v}) by Def31;
end;
assume
A3: e in G.edgesDBetween(the_Vertices_of G, {v});
then e DSJoins the_Vertices_of G, {v}, G by Def31;
then (the_Target_of G).e = v by TARSKI:def 1;
hence e in v.edgesIn() by A3,Lm7;
end;
hence v.edgesIn() = G.edgesDBetween(the_Vertices_of G, {v}) by TARSKI:2;
now
let e be object;
hereby
assume
A4: e in v.edgesOut();
then (the_Source_of G).e = v by Lm8;
then
A5: (the_Source_of G).e in {v} by TARSKI:def 1;
(the_Target_of G).e in the_Vertices_of G by A4,FUNCT_2:5;
then e DSJoins {v},the_Vertices_of G,G by A4,A5;
hence e in G.edgesDBetween({v},the_Vertices_of G) by Def31;
end;
assume
A6: e in G.edgesDBetween({v},the_Vertices_of G);
then e DSJoins {v},the_Vertices_of G, G by Def31;
then (the_Source_of G).e = v by TARSKI:def 1;
hence e in v.edgesOut() by A6,Lm8;
end;
hence thesis by TARSKI:2;
end;
theorem
G is Subgraph of G by Lm3;
theorem Th41:
G1 is Subgraph of G2 & G2 is Subgraph of G1 iff the_Vertices_of
G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1
= the_Source_of G2 & the_Target_of G1 = the_Target_of G2
proof
hereby
assume that
A1: G1 is Subgraph of G2 and
A2: G2 is Subgraph of G1;
A3: the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c=
the_Edges_of G1 by A2,Def32;
the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c=
the_Edges_of G2 by A1,Def32;
hence
A4: the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 =
the_Edges_of G2 by A3,XBOOLE_0:def 10;
then
A5: dom the_Source_of G1 = the_Edges_of G1 & dom the_Source_of G2 =
the_Edges_of G1 by FUNCT_2:def 1;
for e being object st e in dom the_Source_of G1 holds (the_Source_of G1)
.e = (the_Source_of G2).e by A1,Def32;
hence the_Source_of G1 = the_Source_of G2 by A5,FUNCT_1:2;
A6: dom the_Target_of G1 = the_Edges_of G1 & dom the_Target_of G2 =
the_Edges_of G1 by A4,FUNCT_2:def 1;
for e being object st e in dom the_Target_of G1 holds (the_Target_of G1)
.e = (the_Target_of G2).e by A1,Def32;
hence the_Target_of G1 = the_Target_of G2 by A6,FUNCT_1:2;
end;
assume that
A7: the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 =
the_Edges_of G2 and
A8: the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2;
for e being set st e in the_Edges_of G1 holds (the_Source_of G1).e = (
the_Source_of G2).e & (the_Target_of G1).e = (the_Target_of G2).e by A8;
hence thesis by A7,Def32;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, x being set holds (x in
the_Vertices_of G2 implies x in the_Vertices_of G1) & (x in the_Edges_of G2
implies x in the_Edges_of G1);
theorem Th43:
for G1 being _Graph, G2 being Subgraph of G1, G3 being Subgraph
of G2 holds G3 is Subgraph of G1
proof
let G1 be _Graph, G2 be Subgraph of G1, G3 be Subgraph of G2;
A1: the_Edges_of G2 c= the_Edges_of G1;
A2: the_Vertices_of G3 c= the_Vertices_of G2;
now
thus the_Vertices_of G3 c= the_Vertices_of G1 by A2,XBOOLE_1:1;
thus the_Edges_of G3 c= the_Edges_of G1 by A1;
let e be set;
assume
A3: e in the_Edges_of G3;
hence (the_Source_of G3).e = (the_Source_of G2).e by Def32
.= (the_Source_of G1).e by A3,Def32;
thus (the_Target_of G3).e = (the_Target_of G2).e by A3,Def32
.= (the_Target_of G1).e by A3,Def32;
end;
hence thesis by Def32;
end;
theorem Th44:
for G being _Graph, G1, G2 being Subgraph of G st
the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2
holds G1 is Subgraph of G2
proof
let G be _Graph, G1, G2 be Subgraph of G;
assume that
A1: the_Vertices_of G1 c= the_Vertices_of G2 and
A2: the_Edges_of G1 c= the_Edges_of G2;
now
let e be set;
assume
A3: e in the_Edges_of G1;
hence (the_Source_of G1).e = (the_Source_of G).e by Def32
.= (the_Source_of G2).e by A2,A3,Def32;
thus (the_Target_of G1).e = (the_Target_of G).e by A3,Def32
.= (the_Target_of G2).e by A2,A3,Def32;
end;
hence thesis by A1,A2,Def32;
end;
theorem Th45:
for G1 being _Graph, G2 being Subgraph of G1 holds the_Source_of
G2 = (the_Source_of G1) | the_Edges_of G2 & the_Target_of G2 = (the_Target_of
G1) | the_Edges_of G2
proof
let G1 be _Graph, G2 be Subgraph of G1;
set S2 = (the_Source_of G1) | the_Edges_of G2;
set T2 = (the_Target_of G1) | the_Edges_of G2;
A1: now
let x be object;
assume
A2: x in dom the_Source_of G2;
hence (the_Source_of G2).x = (the_Source_of G1).x by Def32
.= S2.x by A2,FUNCT_1:49;
end;
dom the_Source_of G1 = the_Edges_of G1 by FUNCT_2:def 1;
then dom the_Source_of G2 = the_Edges_of G2 & dom S2 = the_Edges_of G2 by
FUNCT_2:def 1,RELAT_1:62;
hence the_Source_of G2 = S2 by A1,FUNCT_1:2;
A3: now
let x be object;
assume
A4: x in dom the_Target_of G2;
hence (the_Target_of G2).x = (the_Target_of G1).x by Def32
.= T2.x by A4,FUNCT_1:49;
end;
dom the_Target_of G1 = the_Edges_of G1 by FUNCT_2:def 1;
then dom the_Target_of G2 = the_Edges_of G2 & dom T2 = the_Edges_of G2 by
FUNCT_2:def 1,RELAT_1:62;
hence thesis by A3,FUNCT_1:2;
end;
theorem
for G being _Graph, V1,V2,E1,E2 being set, G1 being inducedSubgraph of
G,V1,E1, G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non
empty Subset of the_Vertices_of G & E2 c= G.edgesBetween(V2) holds G2 is
Subgraph of G1
proof
let G be _Graph, V1,V2,E1,E2 be set, G1 be inducedSubgraph of G,V1,E1, G2 be
inducedSubgraph of G,V2,E2;
assume that
A1: V2 c= V1 & E2 c= E1 and
A2: V2 is non empty Subset of the_Vertices_of G & E2 c= G.edgesBetween( V2);
A3: the_Vertices_of G2 = V2 & the_Edges_of G2 = E2 by A2,Def37;
now
per cases;
suppose
V1 is non empty Subset of the_Vertices_of G & E1 c= G .edgesBetween(V1);
then the_Vertices_of G1 = V1 & the_Edges_of G1 = E1 by Def37;
hence thesis by A1,A3,Th44;
end;
suppose
not (V1 is non empty Subset of the_Vertices_of G & E1 c= G
.edgesBetween(V1));
then G1 == G by Def37;
hence thesis by A3,Th44;
end;
end;
hence thesis;
end;
theorem Th47:
for G1 being non _trivial _Graph, v being Vertex of G1, G2 being
removeVertex of G1,v holds the_Vertices_of G2 = the_Vertices_of G1 \ {v} &
the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ {v})
proof
let G1 be non _trivial _Graph,v be Vertex of G1,
G2 be removeVertex of G1,v;
set VG = the_Vertices_of G1, V = VG \ {v};
now
assume V is empty;
then VG c= {v} by XBOOLE_1:37;
then VG = {v} by ZFMISC_1:33;
then card VG = 1 by CARD_1:30;
hence contradiction by Def19;
end;
then reconsider V as non empty Subset of VG;
G2 is inducedSubgraph of G1,V;
hence thesis by Def37;
end;
theorem
for G1 being _finite non _trivial _Graph, v being Vertex of G1, G2 being
removeVertex of G1,v holds G2.order() + 1 = G1.order() & G2.size() + card v
.edgesInOut() = G1.size()
proof
let G1 be _finite non _trivial _Graph, v be Vertex of G1,
G2 be removeVertex of G1,v;
set VG1 = the_Vertices_of G1, VG2 = the_Vertices_of G2;
set EG1 = the_Edges_of G1, EG2 = the_Edges_of G2, EV = v.edgesInOut();
A1: VG2 = VG1 \ {v} by Th47;
v in {v} by TARSKI:def 1;
then not v in VG2 by A1,XBOOLE_0:def 5;
then card (( VG1 \ {v}) \/ {v}) = G2.order() + 1 by A1,CARD_2:41;
hence G2.order() + 1 = G1.order() by XBOOLE_1:45;
A2: EG2 = G1.edgesBetween(VG1 \ {v}) & G1.edgesBetween(VG1 \ {v}) = EG1 \ EV
by Th35,Th47;
then EG1 = EG2 \/ EV by XBOOLE_1:45;
hence thesis by A2,CARD_2:40,XBOOLE_1:79;
end;
theorem Th49:
for G1 being _Graph, V being set, G2 being removeVertices of G1,
V st V c< the_Vertices_of G1 holds the_Vertices_of G2 = the_Vertices_of G1 \ V
& the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ V)
proof
let G1 be _Graph, V be set, G2 be removeVertices of G1,V;
set VG2 = the_Vertices_of G1 \ V;
assume
A1: V c< the_Vertices_of G1;
now
assume VG2 is empty;
then the_Vertices_of G1 c= V by XBOOLE_1:37;
hence contradiction by A1,XBOOLE_0:def 8;
end;
then reconsider VG2 as non empty Subset of the_Vertices_of G1;
G2 is inducedSubgraph of G1,VG2;
hence thesis by Def37;
end;
theorem
for G1 being _finite _Graph, V being Subset of the_Vertices_of G1, G2
being removeVertices of G1,V st V <> the_Vertices_of G1 holds G2.order() + card
V = G1.order() & G2.size() + card G1.edgesInOut(V) = G1.size()
proof
let G1 be _finite _Graph, V be Subset of the_Vertices_of G1, G2 be
removeVertices of G1,V;
set VG1 = the_Vertices_of G1, VG2 = the_Vertices_of G2;
set EG1 = the_Edges_of G1, EG2 = the_Edges_of G2;
A1: G1.edgesBetween(VG1 \ V) = EG1 \ G1.edgesInOut(V) by Th35;
assume V <> VG1;
then
A2: V c< VG1 by XBOOLE_0:def 8;
then
A3: VG2 = VG1 \ V by Th49;
then card (VG2 \/ V) = card VG2 + card V by CARD_2:40,XBOOLE_1:79;
hence G2.order() + card V = G1.order() by A3,XBOOLE_1:45;
A4: EG2 = G1.edgesBetween(VG1 \ V) by A2,Th49;
then EG1 = EG2 \/ G1.edgesInOut(V) by A1,XBOOLE_1:45;
hence thesis by A4,A1,CARD_2:40,XBOOLE_1:79;
end;
theorem Th51:
for G1 being _Graph, e being set, G2 being removeEdge of G1,e
holds the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of
G1 \ {e}
proof
let G1 be _Graph, e be set, G2 be removeEdge of G1,e;
set V = the_Vertices_of G1;
V c= V;
then reconsider V as non empty Subset of the_Vertices_of G1;
set E = the_Edges_of G1 \ {e};
reconsider E as Subset of G1.edgesBetween(V) by Th34;
G2 is inducedSubgraph of G1,V,E;
hence thesis by Def37;
end;
theorem
for G1 being _finite _Graph, e being set, G2 being removeEdge of G1,e
holds G1.order() = G2.order() & (e in the_Edges_of G1 implies G2.size() + 1 =
G1.size())
proof
let G1 be _finite _Graph, e be set, G2 be removeEdge of G1,e;
A1: the_Edges_of G2 = the_Edges_of G1 \ {e} by Th51;
thus G1.order() = G2.order() by Th51;
assume e in the_Edges_of G1;
then for x being object st x in {e} holds x in the_Edges_of G1
by TARSKI:def 1;
then {e} c= the_Edges_of G1;
then
A2: the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1,XBOOLE_1:45;
e in {e} by TARSKI:def 1;
then not e in the_Edges_of G2 by A1,XBOOLE_0:def 5;
hence thesis by A2,CARD_2:41;
end;
theorem Th53:
for G1 being _Graph, E being set, G2 being removeEdges of G1,E
holds the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of
G1 \ E
proof
let G1 be _Graph, E be set, G2 be removeEdges of G1,E;
set V = the_Vertices_of G1;
V c= V;
then reconsider V as non empty Subset of the_Vertices_of G1;
set E2 = the_Edges_of G1 \ E;
reconsider E2 as Subset of G1.edgesBetween(V) by Th34;
G2 is inducedSubgraph of G1,V,E2;
hence thesis by Def37;
end;
theorem
for G1 being _Graph, E being set, G2 being removeEdges of G1,E
holds G1.order() = G2.order() by Th53;
theorem
for G1 being _finite _Graph, E being Subset of the_Edges_of G1, G2
being removeEdges of G1,E holds G2.size() + card E = G1.size()
proof
let G1 be _finite _Graph, E be Subset of the_Edges_of G1, G2 be removeEdges
of G1,E;
A1: the_Edges_of G2 = the_Edges_of G1 \ E by Th53;
then the_Edges_of G1 = the_Edges_of G2 \/ E by XBOOLE_1:45;
hence thesis by A1,CARD_2:40,XBOOLE_1:79;
end;
theorem
e in v.edgesIn() iff e in the_Edges_of G & (the_Target_of G).e = v by Lm7;
theorem
e in v.edgesIn() iff ex x being set st e DJoins x,v,G
proof
hereby
set x = (the_Source_of G).e;
assume
A1: e in v.edgesIn();
take x;
(the_Target_of G).e = v by A1,Lm7;
hence e DJoins x,v,G by A1;
end;
given x being set such that
A2: e DJoins x,v,G;
e in the_Edges_of G & (the_Target_of G).e = v by A2;
hence thesis by Lm7;
end;
theorem
e in v.edgesOut() iff e in the_Edges_of G & (the_Source_of G).e = v by Lm8;
theorem
e in v.edgesOut() iff ex x being set st e DJoins v,x,G
proof
hereby
set x = (the_Target_of G).e;
assume
A1: e in v.edgesOut();
take x;
(the_Source_of G).e = v by A1,Lm8;
hence e DJoins v,x,G by A1;
end;
given x being set such that
A2: e DJoins v,x,G;
e in the_Edges_of G & (the_Source_of G).e = v by A2;
hence thesis by Lm8;
end;
theorem
v.edgesInOut() = v.edgesIn() \/ v.edgesOut();
theorem Th61:
e in v.edgesInOut() iff e in the_Edges_of G & ((the_Source_of G)
.e = v or (the_Target_of G).e = v)
proof
hereby
assume
A1: e in v.edgesInOut();
hence e in the_Edges_of G;
e in v.edgesIn() or e in v.edgesOut() by A1,XBOOLE_0:def 3;
hence (the_Source_of G).e=v or (the_Target_of G).e=v by Lm7,Lm8;
end;
assume
e in the_Edges_of G &( (the_Source_of G).e=v or (the_Target_of G).e= v);
then e in v.edgesIn() or e in v.edgesOut() by Lm7,Lm8;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th62:
for e,x being object holds
e Joins v1,x,G implies e in v1.edgesInOut() by Th61;
theorem Th63:
e Joins v1,v2,G implies e in v1.edgesIn() & e in v2.edgesOut()
or e in v2.edgesIn() & e in v1.edgesOut()
proof
assume
A1: e Joins v1,v2,G;
then
A2: e in the_Edges_of G;
now
per cases by A1;
suppose
(the_Source_of G).e = v1 & (the_Target_of G).e = v2;
hence thesis by A2,Lm7,Lm8;
end;
suppose
(the_Source_of G).e = v2 & (the_Target_of G).e = v1;
hence thesis by A2,Lm7,Lm8;
end;
end;
hence thesis;
end;
theorem
e in v1.edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G
proof
hereby
assume
A1: e in v1.edgesInOut();
now
per cases by A1,Th61;
suppose
A2: (the_Source_of G).e = v1;
set v2 = (the_Target_of G).e;
reconsider v2 as Vertex of G by A1,FUNCT_2:5;
take v2;
thus e Joins v1, v2, G by A1,A2;
end;
suppose
A3: (the_Target_of G).e = v1;
set v2 = (the_Source_of G).e;
reconsider v2 as Vertex of G by A1,FUNCT_2:5;
take v2;
thus e Joins v1,v2,G by A1,A3;
end;
end;
hence ex v2 being Vertex of G st e Joins v1,v2,G;
end;
given v2 being Vertex of G such that
A4: e Joins v1,v2,G;
thus thesis by A4,Th62;
end;
theorem
for e,x,y being object holds
e in v.edgesInOut() & e Joins x,y,G implies v = x or v = y
proof let e,x,y be object;
assume that
A1: e in v.edgesInOut() and
A2: e Joins x,y,G;
now
assume
A3: v <> x;
now
per cases by A1,Th61;
suppose
(the_Source_of G).e = v;
hence v = y by A2,A3;
end;
suppose
(the_Target_of G).e = v;
hence v = y by A2,A3;
end;
end;
hence v = y;
end;
hence thesis;
end;
theorem
for e being object holds
e Joins v1,v2,G implies v1.adj(e) = v2 & v2.adj(e) = v1
proof let e be object;
assume
A1: e Joins v1, v2,G;
then
A2: e in v1.edgesInOut() by Th62;
now
per cases by A1;
suppose
A3: (the_Source_of G).e = v2 & (the_Target_of G).e = v1;
hence v1.adj(e) = v2 by A2,Def41;
now
per cases;
suppose
v1 = v2;
hence v2.adj(e) = v1 by A2,A3,Def41;
end;
suppose
v1 <> v2;
hence v2.adj(e) = v1 by A2,A3,Def41;
end;
end;
hence v2.adj(e) = v1;
end;
suppose
A4: (the_Source_of G).e = v1 & (the_Target_of G).e = v2;
now
per cases;
suppose
v1 = v2;
hence v1.adj(e) = v2 by A2,A4,Def41;
end;
suppose
v1 <> v2;
hence v1.adj(e) = v2 by A2,A4,Def41;
end;
end;
hence v1.adj(e) = v2;
thus v2.adj(e) = v1 by A2,A4,Def41;
end;
end;
hence thesis;
end;
theorem
e in v.edgesInOut() iff e Joins v,v.adj(e),G
proof
hereby
assume
A1: e in v.edgesInOut();
then
A2: (the_Source_of G).e = v or (the_Target_of G).e = v by Th61;
now
per cases;
suppose
A3: (the_Target_of G).e = v;
then v.adj(e) = (the_Source_of G).e by A1,Def41;
hence e Joins v,v.adj(e),G by A1,A3;
end;
suppose
A4: (the_Target_of G).e <> v;
then v.adj(e) = (the_Target_of G).e by A1,A2,Def41;
hence e Joins v,v.adj(e),G by A1,A2,A4;
end;
end;
hence e Joins v,v.adj(e),G;
end;
assume e Joins v,v.adj(e),G;
hence thesis by Th62;
end;
theorem
for G being _finite _Graph, e being set, v1,v2 being Vertex of G holds
e Joins v1,v2,G implies 1 <= v1.degree() & 1 <= v2.degree()
proof
let G be _finite _Graph, e be set, v1, v2 be Vertex of G;
assume
A1: e Joins v1, v2,G;
now
per cases by A1,Th63;
suppose
A2: e in v1.edgesIn() & e in v2.edgesOut();
then for x being object st x in {e}
holds x in v1.edgesIn() by TARSKI:def 1;
then {e} c= v1.edgesIn();
then card {e} <= card v1.edgesIn() by NAT_1:43;
then 1 <= v1.inDegree() by CARD_1:30;
hence 1 <= v1.degree() by NAT_1:12;
for x being object
st x in {e} holds x in v2.edgesOut() by A2,TARSKI:def 1;
then {e} c= v2.edgesOut();
then card {e} <= card v2.edgesOut() by NAT_1:43;
then 1 <= v2.outDegree() by CARD_1:30;
hence 1 <= v2.degree() by NAT_1:12;
end;
suppose
A3: e in v2.edgesIn() & e in v1.edgesOut();
then for x being object
st x in {e} holds x in v1.edgesOut() by TARSKI:def 1;
then {e} c= v1.edgesOut();
then card {e} <= card v1.edgesOut() by NAT_1:43;
then 1 <= v1.outDegree() by CARD_1:30;
hence 1 <= v1.degree() by NAT_1:12;
for x being object
st x in {e} holds x in v2.edgesIn() by A3,TARSKI:def 1;
then {e} c= v2.edgesIn();
then card {e} <= card v2.edgesIn() by NAT_1:43;
then 1 <= v2.inDegree() by CARD_1:30;
hence 1 <= v2.degree() by NAT_1:12;
end;
end;
hence thesis;
end;
theorem Th69:
x in v.inNeighbors() iff ex e being object st e DJoins x,v,G
proof
hereby
assume x in v.inNeighbors();
then consider e being object such that
A1: e in dom (the_Source_of G) and
A2: e in v.edgesIn() and
A3: x = (the_Source_of G).e by FUNCT_1:def 6;
take e;
(the_Target_of G).e = v by A2,Lm7;
hence e DJoins x,v,G by A1,A3;
end;
given e being object such that
A4: e DJoins x,v,G;
A5: e in the_Edges_of G by A4;
then
A6: e in dom (the_Source_of G) by FUNCT_2:def 1;
(the_Target_of G).e = v by A4;
then
A7: e in v.edgesIn() by A5,Lm7;
(the_Source_of G).e = x by A4;
hence thesis by A7,A6,FUNCT_1:def 6;
end;
theorem Th70:
x in v.outNeighbors() iff ex e being object st e DJoins v,x,G
proof
hereby
assume x in v.outNeighbors();
then consider e being object such that
A1: e in dom (the_Target_of G) and
A2: e in v.edgesOut() and
A3: x = (the_Target_of G).e by FUNCT_1:def 6;
take e;
(the_Source_of G).e = v by A2,Lm8;
hence e DJoins v,x,G by A1,A3;
end;
given e being object such that
A4: e DJoins v,x,G;
A5: e in the_Edges_of G by A4;
then
A6: e in dom (the_Target_of G) by FUNCT_2:def 1;
(the_Source_of G).e = v by A4;
then
A7: e in v.edgesOut() by A5,Lm8;
(the_Target_of G).e = x by A4;
hence thesis by A7,A6,FUNCT_1:def 6;
end;
theorem Th71:
x in v.allNeighbors() iff ex e being object st e Joins v,x,G
proof
hereby
assume
A1: x in v.allNeighbors();
now
per cases by A1,XBOOLE_0:def 3;
suppose
x in v.inNeighbors();
then consider e being object such that
A2: e DJoins x,v,G by Th69;
take e;
thus e Joins v,x,G by A2;
end;
suppose
x in v.outNeighbors();
then consider e being object such that
A3: e DJoins v,x,G by Th70;
take e;
thus e Joins v,x,G by A3;
end;
end;
hence ex e being object st e Joins v,x,G;
end;
given e being object such that
A4: e Joins v,x,G;
now
per cases by A4;
suppose
e DJoins x,v,G;
then x in v.inNeighbors() by Th69;
hence x in v.inNeighbors() \/ v.outNeighbors() by XBOOLE_0:def 3;
end;
suppose
e DJoins v,x,G;
then x in v.outNeighbors() by Th70;
hence x in v.inNeighbors() \/ v.outNeighbors() by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
theorem Th72:
for G1 being _Graph, G2 being Subgraph of G1,
x,y being set, e being object
holds (e Joins x,y,G2 implies e Joins x,y,G1) & (e DJoins x,y,G2 implies e
DJoins x,y,G1) & (e SJoins x,y,G2 implies e SJoins x,y,G1) & (e DSJoins x,y,G2
implies e DSJoins x,y,G1)
proof
let G1 be _Graph, G2 be Subgraph of G1, x,y be set, e be object;
thus e Joins x,y,G2 implies e Joins x,y,G1 by Lm4;
hereby
assume
A1: e DJoins x,y,G2;
then
A2: e in the_Edges_of G2;
(the_Target_of G2) .e=y by A1;
then
A3: (the_Target_of G1).e = y by A2,Def32;
(the_Source_of G2).e=x by A1;
then (the_Source_of G1).e = x by A2,Def32;
hence e DJoins x,y,G1 by A2,A3;
end;
hereby
assume
A4: e SJoins x,y,G2;
then
A5: (the_Source_of G2).e in x & (the_Target_of G2).e in y or (
the_Source_of G2).e in y & (the_Target_of G2).e in x;
A6: e in the_Edges_of G2 by A4;
then (the_Source_of G2).e = (the_Source_of G1).e & (the_Target_of G2).e =
( the_Target_of G1).e by Def32;
hence e SJoins x,y,G1 by A6,A5;
end;
assume
A7: e DSJoins x,y,G2;
then
A8: (the_Source_of G2).e in x & (the_Target_of G2).e in y;
A9: e in the_Edges_of G2 by A7;
then (the_Source_of G2).e = (the_Source_of G1).e & (the_Target_of G2).e = (
the_Target_of G1).e by Def32;
hence thesis by A9,A8;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, x,y,e being set st e in
the_Edges_of G2 holds (e Joins x,y,G1 implies e Joins x,y,G2) & (e DJoins x,y,
G1 implies e DJoins x,y,G2) & (e SJoins x,y,G1 implies e SJoins x,y,G2) & (e
DSJoins x,y,G1 implies e DSJoins x,y,G2)
by Def32;
theorem
for G1 being _Graph, G2 being spanning Subgraph of G1, G3 being
spanning Subgraph of G2 holds G3 is spanning Subgraph of G1
proof
let G1 be _Graph, G2 be spanning Subgraph of G1, G3 be spanning Subgraph of
G2;
the_Vertices_of G3 = the_Vertices_of G2 by Def33
.= the_Vertices_of G1 by Def33;
hence thesis by Def33,Th43;
end;
theorem
for G1 being _finite _Graph, G2 being Subgraph of G1 holds G2.order()
<= G1.order() & G2.size() <= G1.size()
proof
let G1 be _finite _Graph, G2 be Subgraph of G1;
card the_Vertices_of G2 <= card the_Vertices_of G1 by NAT_1:43;
hence G2.order() <= G1.order();
card the_Edges_of G2 <= card the_Edges_of G1 by NAT_1:43;
hence thesis;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, X being set holds G2
.edgesInto(X) c= G1.edgesInto(X) & G2.edgesOutOf(X) c= G1.edgesOutOf(X) & G2
.edgesInOut(X) c= G1.edgesInOut(X) & G2.edgesBetween(X) c= G1.edgesBetween(X)
proof
let G1 be _Graph, G2 be Subgraph of G1, X be set;
now
let e be object;
assume
A1: e in G2.edgesInto(X);
then
A2: (the_Target_of G2).e = (the_Target_of G1).e by Def32;
e in the_Edges_of G2 & (the_Target_of G2).e in X by A1,Def26;
hence e in G1.edgesInto(X) by A2,Def26;
end;
hence
A3: G2.edgesInto(X) c= G1.edgesInto(X);
then
A4: G2.edgesInto(X) c= G1.edgesInOut(X) by XBOOLE_1:10;
now
let e be object;
assume
A5: e in G2.edgesOutOf(X);
then
A6: (the_Source_of G2).e = (the_Source_of G1).e by Def32;
e in the_Edges_of G2 & (the_Source_of G2).e in X by A5,Def27;
hence e in G1.edgesOutOf(X) by A6,Def27;
end;
hence
A7: G2.edgesOutOf(X) c= G1.edgesOutOf(X);
then G2.edgesOutOf(X) c= G1.edgesInOut(X) by XBOOLE_1:10;
hence G2.edgesInOut(X) c= G1.edgesInOut(X) by A4,XBOOLE_1:8;
thus thesis by A3,A7,XBOOLE_1:27;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, X,Y being set holds G2
.edgesBetween(X,Y) c= G1.edgesBetween(X,Y) & G2.edgesDBetween(X,Y) c= G1
.edgesDBetween(X,Y)
proof
let G1 be _Graph, G2 be Subgraph of G1, X,Y be set;
now
let x be object;
assume x in G2.edgesBetween(X,Y);
then x SJoins X,Y,G2 by Def30;
then x SJoins X,Y,G1 by Th72;
hence x in G1.edgesBetween(X,Y) by Def30;
end;
hence G2.edgesBetween(X,Y) c= G1.edgesBetween(X,Y);
now
let x be object;
assume x in G2.edgesDBetween(X,Y);
then x DSJoins X,Y,G2 by Def31;
then x DSJoins X,Y,G1 by Th72;
hence x in G1.edgesDBetween(X,Y) by Def31;
end;
hence thesis;
end;
theorem Th78:
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of
G1, v2 being Vertex of G2 st v1 = v2 holds v2.edgesIn() c= v1.edgesIn() & v2
.edgesOut() c= v1.edgesOut() & v2.edgesInOut() c= v1.edgesInOut()
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2;
assume
A1: v1 = v2;
now
let x be object;
assume
A2: x in v2.edgesIn();
then (the_Target_of G2).x = v2 by Lm7;
then
A3: (the_Target_of G1).x = v1 by A1,A2,Def32;
x in the_Edges_of G2 by A2;
hence x in v1.edgesIn() by A3,Lm7;
end;
hence v2.edgesIn() c= v1.edgesIn();
now
let x be object;
assume
A4: x in v2.edgesOut();
then (the_Source_of G2).x = v2 by Lm8;
then
A5: (the_Source_of G1).x = v1 by A1,A4,Def32;
x in the_Edges_of G2 by A4;
hence x in v1.edgesOut() by A5,Lm8;
end;
hence v2.edgesOut() c= v1.edgesOut();
now
let x be object;
assume
A6: x in v2.edgesInOut();
then (the_Source_of G2).x = v2 or (the_Target_of G2).x = v2 by Th61;
then
A7: (the_Source_of G1).x = v1 or (the_Target_of G1).x=v1 by A1,A6,Def32;
x in the_Edges_of G2 by A6;
hence x in v1.edgesInOut() by A7,Th61;
end;
hence thesis;
end;
theorem Th79:
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of
G1, v2 being Vertex of G2 st v1 = v2 holds v2.edgesIn() = v1.edgesIn() /\ (
the_Edges_of G2) & v2.edgesOut() = v1.edgesOut() /\ (the_Edges_of G2) & v2
.edgesInOut() = v1.edgesInOut() /\ (the_Edges_of G2)
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2;
assume
A1: v1 = v2;
now
let x be object;
hereby
assume
A2: x in v2.edgesIn();
v2.edgesIn() c= v1.edgesIn() by A1,Th78;
hence x in v1.edgesIn()/\(the_Edges_of G2) by A2,XBOOLE_0:def 4;
end;
assume
A3: x in v1.edgesIn() /\ (the_Edges_of G2);
then
A4: x in the_Edges_of G2 by XBOOLE_0:def 4;
x in v1.edgesIn() by A3,XBOOLE_0:def 4;
then (the_Target_of G1).x = v1 by Lm7;
then (the_Target_of G2).x = v2 by A1,A4,Def32;
hence x in v2.edgesIn() by A4,Lm7;
end;
hence
A5: v2.edgesIn() = v1.edgesIn() /\ (the_Edges_of G2) by TARSKI:2;
now
let x be object;
hereby
assume
A6: x in v2.edgesOut();
v2.edgesOut() c= v1.edgesOut() by A1,Th78;
hence x in v1.edgesOut() /\ (the_Edges_of G2) by A6,XBOOLE_0:def 4;
end;
assume
A7: x in v1.edgesOut() /\ (the_Edges_of G2);
then
A8: x in the_Edges_of G2 by XBOOLE_0:def 4;
x in v1.edgesOut() by A7,XBOOLE_0:def 4;
then (the_Source_of G1).x = v1 by Lm8;
then (the_Source_of G2).x = v2 by A1,A8,Def32;
hence x in v2.edgesOut() by A8,Lm8;
end;
hence
A9: v2.edgesOut() = v1.edgesOut() /\ (the_Edges_of G2) by TARSKI:2;
now
let x be object;
hereby
assume
A10: x in v1.edgesInOut() /\ (the_Edges_of G2);
then
A11: x in the_Edges_of G2 by XBOOLE_0:def 4;
A12: x in v1.edgesInOut() by A10,XBOOLE_0:def 4;
now
per cases by A12,XBOOLE_0:def 3;
suppose
x in v1.edgesIn();
then x in v1.edgesIn()/\(the_Edges_of G2) by A11,XBOOLE_0:def 4;
hence x in v2.edgesInOut() by A5,XBOOLE_0:def 3;
end;
suppose
x in v1.edgesOut();
then x in v1.edgesOut()/\(the_Edges_of G2) by A11,XBOOLE_0:def 4;
hence x in v2.edgesInOut() by A9,XBOOLE_0:def 3;
end;
end;
hence x in v2.edgesInOut();
end;
assume
A13: x in v2.edgesInOut();
now
per cases by A5,A9,A13,XBOOLE_0:def 3;
suppose
A14: x in v1.edgesIn() /\ (the_Edges_of G2);
then x in v1.edgesIn() by XBOOLE_0:def 4;
then
A15: x in v1.edgesIn() \/ v1.edgesOut() by XBOOLE_0:def 3;
x in the_Edges_of G2 by A14,XBOOLE_0:def 4;
hence x in v1.edgesInOut() /\ (the_Edges_of G2) by A15,XBOOLE_0:def 4;
end;
suppose
A16: x in v1.edgesOut() /\ (the_Edges_of G2);
then x in v1.edgesOut() by XBOOLE_0:def 4;
then
A17: x in v1.edgesIn() \/ v1.edgesOut() by XBOOLE_0:def 3;
x in (the_Edges_of G2) by A16,XBOOLE_0:def 4;
hence x in v1.edgesInOut() /\ (the_Edges_of G2) by A17,XBOOLE_0:def 4;
end;
end;
hence x in v1.edgesInOut() /\ (the_Edges_of G2);
end;
hence thesis by TARSKI:2;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2, e being set st v1 = v2 & e in the_Edges_of G2 holds v1
.adj(e) = v2.adj(e)
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2, e be set;
assume that
A1: v1 = v2 and
A2: e in the_Edges_of G2;
A3: (the_Source_of G2).e = (the_Source_of G1).e & (the_Target_of G2).e = (
the_Target_of G1).e by A2,Def32;
now
per cases;
suppose
A4: (the_Target_of G1).e = v1;
hence v1.adj(e) = (the_Source_of G1).e by A2,Def41
.= v2.adj(e) by A1,A2,A3,A4,Def41;
end;
suppose
A5: (the_Source_of G1).e = v1 & (the_Target_of G1).e <> v1;
hence v1.adj(e) = (the_Target_of G1).e by A2,Def41
.= v2.adj(e) by A1,A2,A3,A5,Def41;
end;
suppose
A6: (the_Source_of G1).e <> v1 & (the_Target_of G1).e <> v1;
hence v1.adj(e) = v2 by A1,Def41
.= v2.adj(e) by A1,A3,A6,Def41;
end;
end;
hence thesis;
end;
theorem
for G1 being _finite _Graph, G2 being Subgraph of G1, v1 being Vertex
of G1, v2 being Vertex of G2 st v1 = v2 holds v2.inDegree() <= v1.inDegree() &
v2.outDegree() <= v1.outDegree() & v2.degree() <= v1.degree()
proof
let G1 be _finite _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1 = v2;
then v2.edgesIn() = v1.edgesIn() /\ (the_Edges_of G2) by Th79;
hence
A2: v2.inDegree() <= v1.inDegree() by NAT_1:43,XBOOLE_1:17;
A3: v2.edgesOut() = v1.edgesOut()/\(the_Edges_of G2) by A1,Th79;
hence v2.outDegree() <= v1.outDegree() by NAT_1:43,XBOOLE_1:17;
v2.outDegree() <= card v1.edgesOut() by A3,NAT_1:43,XBOOLE_1:17;
hence thesis by A2,XREAL_1:7;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 holds v2.inNeighbors() c= v1.inNeighbors() &
v2.outNeighbors() c= v1.outNeighbors() & v2.allNeighbors() c= v1.allNeighbors()
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2;
assume
A1: v1 = v2;
now
let v be object;
assume v in v2.inNeighbors();
then consider e being object such that
A2: e DJoins v,v2,G2 by Th69;
e DJoins v,v1,G1 by A1,A2,Th72;
hence v in v1.inNeighbors() by Th69;
end;
hence v2.inNeighbors() c= v1.inNeighbors();
now
let v be object;
assume v in v2.outNeighbors();
then consider e being object such that
A3: e DJoins v2,v,G2 by Th70;
e DJoins v1,v,G1 by A1,A3,Th72;
hence v in v1.outNeighbors() by Th70;
end;
hence v2.outNeighbors() c= v1.outNeighbors();
let v be object;
assume v in v2.allNeighbors();
then consider e being object such that
A4: e Joins v2,v,G2 by Th71;
e Joins v1,v,G1 by A1,A4,Lm4;
hence v in v1.allNeighbors() by Th71;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2 is isolated
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2;
assume v1 = v2 & v1 is isolated;
then v1.edgesInOut() = {} & v2.edgesInOut() c= v1.edgesInOut() by Th78;
hence thesis;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds v2 is endvertex or v2
is isolated
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2;
assume that
A1: v1 = v2 and
A2: v1 is endvertex;
consider e being object such that
A3: v1.edgesInOut() = {e} and
A4: not e Joins v1,v1,G1 by A2;
v2.edgesInOut() c= v1.edgesInOut() by A1,Th78;
then
A5: v2.edgesInOut() = {} or v2.edgesInOut() = {e} by A3,ZFMISC_1:33;
v2 is not isolated implies v2 is endvertex by A5,A1,A4,Lm4;
hence thesis;
end;
theorem
G1 == G2 & G2 == G3 implies G1 == G3;
theorem Th86:
for G being _Graph, G1,G2 being Subgraph of G st the_Vertices_of
G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 holds G1 == G2
proof
let G be _Graph, G1,G2 be Subgraph of G;
assume that
A1: the_Vertices_of G1 = the_Vertices_of G2 and
A2: the_Edges_of G1 = the_Edges_of G2;
A3: dom (the_Target_of G1) = the_Edges_of G1 & dom (the_Target_of G2) =
the_Edges_of G2 by FUNCT_2:def 1;
now
let e be object;
assume
A4: e in the_Edges_of G1;
then (the_Target_of G1).e = (the_Target_of G).e by Def32;
hence (the_Target_of G1).e = (the_Target_of G2).e by A2,A4,Def32;
end;
then
A5: the_Target_of G1 = the_Target_of G2 by A2,A3,FUNCT_1:2;
A6: now
let e be object;
assume
A7: e in the_Edges_of G1;
then (the_Source_of G1).e = (the_Source_of G).e by Def32;
hence (the_Source_of G1).e = (the_Source_of G2).e by A2,A7,Def32;
end;
dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Source_of G2) =
the_Edges_of G2 by FUNCT_2:def 1;
then the_Source_of G1 = the_Source_of G2 by A2,A6,FUNCT_1:2;
hence thesis by A1,A2,A5;
end;
theorem Th87:
G1 == G2 iff G1 is Subgraph of G2 & G2 is Subgraph of G1 by Th41;
theorem
for e,x,y being object holds
G1 == G2 implies (e Joins x,y,G1 implies e Joins x,y,G2) & (e
DJoins x,y,G1 implies e DJoins x,y,G2) & (e SJoins X,Y,G1 implies e SJoins X,Y,
G2) & (e DSJoins X,Y,G1 implies e DSJoins X,Y,G2);
theorem
G1 == G2 implies (G1 is _finite implies G2 is _finite) &
(G1 is loopless implies G2 is loopless) &
(G1 is _trivial implies G2 is _trivial) &
(G1 is non-multi implies G2 is non-multi) &
(G1 is non-Dmulti implies G2 is non-Dmulti) &
(G1 is simple implies G2 is simple) &
(G1 is Dsimple implies G2 is Dsimple)
proof
assume
A1: G1 == G2;
then
A2: the_Edges_of G1 = the_Edges_of G2;
the_Vertices_of G1 = the_Vertices_of G2 by A1;
hence G1 is _finite implies G2 is _finite by A2;
A3: the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of
G2 by A1;
A4: G1 is loopless implies G2 is loopless by A2,A3;
hence G1 is loopless implies G2 is loopless;
thus G1 is _trivial implies G2 is _trivial by A1;
A5: now
assume
A6: G1 is non-multi;
now
let e1,e2,v1,v2 be object;
assume e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2;
then e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 by A1;
hence e1 = e2 by A6;
end;
hence G2 is non-multi;
end;
hence G1 is non-multi implies G2 is non-multi;
A7: now
assume
A8: G1 is non-Dmulti;
now
let e1,e2,v1,v2 be object;
assume e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2;
then e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 by A1;
hence e1 = e2 by A8;
end;
hence G2 is non-Dmulti;
end;
hence G1 is non-Dmulti implies G2 is non-Dmulti;
thus G1 is simple implies G2 is simple by A4,A5;
thus thesis by A4,A7;
end;
theorem Th90:
G1 == G2 implies G1.order() = G2.order() & G1.size() = G2.size()
& G1.edgesInto(X) = G2.edgesInto(X) & G1.edgesOutOf(X) = G2.edgesOutOf(X) & G1
.edgesInOut(X) = G2.edgesInOut(X) & G1.edgesBetween(X) = G2.edgesBetween(X) &
G1.edgesDBetween(X,Y) = G2.edgesDBetween(X,Y)
proof
assume
A1: G1 == G2;
hence G1.order() = G2.order();
thus G1.size() = G2.size() by A1;
A2: the_Edges_of G1 = the_Edges_of G2 by A1;
A3: the_Target_of G1 = the_Target_of G2 by A1;
A4: now
let e be object;
e in G1.edgesInto(X) iff e in the_Edges_of G2 & (the_Target_of G2).e
in X by A2,A3,Def26;
hence e in G1.edgesInto(X) iff e in G2.edgesInto(X) by Def26;
end;
hence
A5: G1.edgesInto(X) = G2.edgesInto(X) by TARSKI:2;
A6: the_Source_of G1 = the_Source_of G2 by A1;
A7: now
let e be object;
e in G1.edgesOutOf(X) iff e in the_Edges_of G2 & (the_Source_of G2).e
in X by A2,A6,Def27;
hence e in G1.edgesOutOf(X) iff e in G2.edgesOutOf(X) by Def27;
end;
hence
A8: G1.edgesOutOf(X) = G2.edgesOutOf(X) by TARSKI:2;
thus G1.edgesInOut(X)= G2.edgesInOut(X) by A5,A7,TARSKI:2;
thus G1.edgesBetween(X)=G2.edgesBetween(X) by A4,A8,TARSKI:2;
now
let e be object;
e in G1.edgesDBetween(X,Y) iff e DSJoins X,Y,G1 by Def31;
then e in G1.edgesDBetween(X,Y) iff e DSJoins X,Y,G2 by A1;
hence e in G2.edgesDBetween(X,Y) iff e in G1.edgesDBetween(X,Y) by Def31;
end;
hence thesis by TARSKI:2;
end;
theorem Th91:
G1 == G2 & G3 is Subgraph of G1 implies G3 is Subgraph of G2
proof
assume that
A1: G1 == G2 and
A2: G3 is Subgraph of G1;
the_Vertices_of G3 c= the_Vertices_of G1 by A2,Def32;
hence the_Vertices_of G3 c= the_Vertices_of G2 by A1;
the_Edges_of G3 c= the_Edges_of G1 by A2,Def32;
hence the_Edges_of G3 c= the_Edges_of G2 by A1;
let e be set;
assume
A3: e in the_Edges_of G3;
hence (the_Source_of G3).e = (the_Source_of G1).e by A2,Def32
.= (the_Source_of G2).e by A1;
thus (the_Target_of G3).e = (the_Target_of G1).e by A2,A3,Def32
.= (the_Target_of G2).e by A1;
end;
theorem
G1 == G2 & G1 is Subgraph of G3 implies G2 is Subgraph of G3
proof
assume that
A1: G1 == G2 and
A2: G1 is Subgraph of G3;
A3: the_Edges_of G1 = the_Edges_of G2 by A1;
A4: the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of
G2 by A1;
the_Vertices_of G1 = the_Vertices_of G2 by A1;
hence the_Vertices_of G2 c= the_Vertices_of G3 & the_Edges_of G2 c=
the_Edges_of G3 by A2,A3,Def32;
let e be set;
assume e in the_Edges_of G2;
hence thesis by A2,A3,A4,Def32;
end;
theorem
for G1,G2 being inducedSubgraph of G,V,E holds G1 == G2
proof
let G1,G2 be inducedSubgraph of G,V,E;
now
per cases;
suppose
A1: V is non empty Subset of the_Vertices_of G & E c= G.edgesBetween (V);
then
A2: the_Edges_of G1 = E & the_Edges_of G2 = E by Def37;
the_Vertices_of G1 = V & the_Vertices_of G2 = V by A1,Def37;
hence thesis by A2,Th86;
end;
suppose
not (V is non empty Subset of the_Vertices_of G & E c= G
.edgesBetween(V));
then G1 == G & G2 == G by Def37;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for G1 being _Graph, G2 being inducedSubgraph of G1,the_Vertices_of G1
holds G1 == G2
proof
let G1 be _Graph, G2 be inducedSubgraph of G1, the_Vertices_of G1;
A1: the_Vertices_of G1 c= the_Vertices_of G1;
then the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1) by Def37;
then
A2: the_Edges_of G2 = the_Edges_of G1 by Th34;
then the_Source_of G2 = (the_Source_of G1)|the_Edges_of G1 by Th45;
then the_Source_of G2 = (the_Source_of G1)|(dom the_Source_of G1);
then
A3: the_Source_of G2 = the_Source_of G1;
the_Target_of G2 = (the_Target_of G1)|the_Edges_of G1 by A2,Th45;
then the_Target_of G2 = (the_Target_of G1)|(dom the_Target_of G1);
then
A4: the_Target_of G2 = the_Target_of G1;
the_Vertices_of G2 = the_Vertices_of G1 by A1,Def37;
hence thesis by A2,A3,A4;
end;
theorem
for G1,G2 being _Graph, V,E being set, G3 being inducedSubgraph of G1,
V,E st G1 == G2 holds G3 is inducedSubgraph of G2,V,E
proof
let G1,G2 be _Graph, V,E be set, G3 be inducedSubgraph of G1,V,E;
assume
A1: G1 == G2;
now
per cases;
suppose
A2: V is non empty Subset of the_Vertices_of G1 & E c= G1 .edgesBetween(V);
then
A3: the_Vertices_of G3 = V & the_Edges_of G3 = E by Def37;
A4: G3 is Subgraph of G2 by A1,Th91;
V is non empty Subset of the_Vertices_of G2 & E c= G2.edgesBetween(V
) by A1,A2,Th90;
hence thesis by A3,A4,Def37;
end;
suppose
A5: not (V is non empty Subset of the_Vertices_of G1 & E c= G1
.edgesBetween(V));
then
A6: not (V is non empty Subset of the_Vertices_of G2 & E c= G2
.edgesBetween(V)) by A1,Th90;
G3 == G1 by A5,Def37;
then
A7: G3 == G2 by A1;
then G3 is Subgraph of G2 by Th87;
hence thesis by A6,A7,Def37;
end;
end;
hence thesis;
end;
theorem Th96:
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & G1
== G2 holds v1.edgesIn() = v2.edgesIn() & v1.edgesOut() = v2.edgesOut() & v1
.edgesInOut() = v2.edgesInOut() & v1.adj(e) = v2.adj(e) & v1.inDegree() = v2
.inDegree() & v1.outDegree() = v2.outDegree() & v1.degree() = v2.degree() & v1
.inNeighbors() = v2.inNeighbors() & v1.outNeighbors() = v2.outNeighbors() & v1
.allNeighbors() = v2.allNeighbors()
proof
let v1 be Vertex of G1, v2 be Vertex of G2;
assume that
A1: v1 = v2 and
A2: G1 == G2;
thus
A3: v1.edgesIn() = v2.edgesIn() by A1,A2,Th90;
thus
A4: v1.edgesOut() = v2.edgesOut() by A1,A2,Th90;
thus v1.edgesInOut() = v2.edgesInOut() by A1,A2,Th90;
now
per cases;
suppose
A5: e in the_Edges_of G1 & (the_Target_of G1).e = v1;
then
A6: e in the_Edges_of G2 & (the_Target_of G2).e = v2 by A1,A2;
thus v1.adj(e) = (the_Source_of G1).e by A5,Def41
.= (the_Source_of G2).e by A2
.= v2.adj(e) by A6,Def41;
end;
suppose
A7: e in the_Edges_of G1 & (the_Source_of G1).e = v1 & not (
the_Target_of G1).e = v1;
then
A8: not (the_Target_of G2).e = v2 by A1,A2;
A9: e in the_Edges_of G2 & (the_Source_of G2).e = v2 by A1,A2,A7;
thus v1.adj(e) = (the_Target_of G1).e by A7,Def41
.= (the_Target_of G2).e by A2
.= v2.adj(e) by A9,A8,Def41;
end;
suppose
A10: not (e in the_Edges_of G1 & (the_Target_of G1).e = v1) & not (e
in the_Edges_of G1 & (the_Source_of G1).e = v1 & not (the_Target_of G1).e = v1)
;
then
A11: ( not (e in the_Edges_of G2 & (the_Target_of G2).e = v2))& not (e
in the_Edges_of G2 & (the_Source_of G2).e = v2 & not ( the_Target_of G2).e = v2
) by A1,A2;
thus v1.adj(e) = v2 by A1,A10,Def41
.= v2.adj(e) by A11,Def41;
end;
end;
hence v1.adj(e) = v2.adj(e);
thus v1.inDegree() = v2.inDegree() by A1,A2,Th90;
thus v1.outDegree() = v2.outDegree() by A1,A2,Th90;
hence v1.degree() = v2.degree() by A1,A2,Th90;
thus v1.inNeighbors() = v2.inNeighbors() by A2,A3;
thus v1.outNeighbors() = v2.outNeighbors() by A2,A4;
hence thesis by A2,A3;
end;
theorem
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & G1 == G2
holds (v1 is isolated implies v2 is isolated) & (v1 is endvertex implies v2 is
endvertex)
proof
let v1 be Vertex of G1, v2 be Vertex of G2;
assume
A1: v1 = v2 & G1 == G2;
hence v1 is isolated implies v2 is isolated by Th96;
assume v1 is endvertex;
then consider e being object such that
A2: v1.edgesInOut() = {e} & not e Joins v1,v1,G1;
v2.edgesInOut() = {e} & not e Joins v2,v2,G2 by A1,A2,Th96;
hence thesis;
end;
theorem Th98:
for G being _Graph, G1,G2 being Subgraph of G st G1 c< G2 holds
(the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2
)
proof
let G be _Graph, G1,G2 be Subgraph of G;
assume
A1: G1 c< G2;
then G1 c= G2;
then
A2: G1 is Subgraph of G2;
then
A3: the_Vertices_of G1 c= the_Vertices_of G2 by Def32;
A4: the_Edges_of G1 c= the_Edges_of G2 by A2,Def32;
A5: not G1 == G2 by A1;
now
per cases by A5,Th86;
suppose
the_Vertices_of G1 <> the_Vertices_of G2;
hence thesis by A3,XBOOLE_0:def 8;
end;
suppose
the_Edges_of G1 <> the_Edges_of G2;
hence thesis by A4,XBOOLE_0:def 8;
end;
end;
hence thesis;
end;
theorem
for G being _Graph, G1,G2 being Subgraph of G st G1 c< G2 holds (ex v
being object st v in the_Vertices_of G2 & not v in the_Vertices_of G1) or
ex e being object st e in the_Edges_of G2 & not e in the_Edges_of G1
proof
let G be _Graph, G1,G2 be Subgraph of G;
assume G1 c< G2;
then the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c<
the_Edges_of G2 by Th98;
hence thesis by XBOOLE_0:6;
end;