:: About Supergraphs, {P}art {III}
:: by Sebastian Koch
::
:: Received May 27, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI,
ORDINAL4, ARYTM_3, CARD_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PBOOLE,
FINSET_1, ZFMISC_1, RELAT_2, GLIB_002, FUNCOP_1, TREES_1, GLIB_001,
FUNCT_4, ABIAN, REWRITE1, CHORD, HELLY, FINSEQ_8, GRAPH_1, RFINSEQ,
XCMPLX_0, CARD_2, GRAPH_2, GLIB_006, GLIB_007, SCMYCIEL, GLIB_003,
EQREL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, EQREL_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3,
FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, VALUED_0, NAT_D, CARD_2, FINSEQ_1, RVSUM_1,
RFINSEQ, FUNCT_7, ABIAN, FINSEQ_6, GLIB_000, FINSEQ_8, GRAPH_2, GRAPH_5,
GLIB_001, GLIB_002, HELLY, GLIB_003, CHORD, GLIB_006, GLIB_007;
constructors DOMAIN_1, BINOP_1, BINOP_2, FINSOP_1, RVSUM_1, FINSEQ_5, GRAPH_5,
ABIAN, WELLORD2, FUNCT_2, FIB_NUM2, FINSEQ_8, GLIB_001, GLIB_002, HELLY,
RELSET_1, FUNCT_3, CHORD, NAT_D, GRAPH_2, RFINSEQ, FINSEQ_6, CARD_2,
FUNCT_7, FINSEQ_1, SUBSET_1, GLIB_006, GLIB_007, RELAT_1, GLIB_003,
EQREL_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, ABIAN,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, GLIB_000, GLIB_001, HELLY, GLIB_002,
CARD_1, RELSET_1, SUBSET_1, GLIB_006, GLIB_007, GLIB_003, MSAFREE5,
JORDAN1J, EQREL_1;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions GLIB_000, GLIB_002;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ORDINAL1, XXREAL_0, RELAT_1, CARD_1,
CARD_2, FUNCT_2, FUNCOP_1, FUNCT_4, ZFMISC_1, FUNCT_1, GLIB_000,
GLIB_001, GLIB_002, CHORD, POLYFORM, NAT_1, XREAL_1, ABIAN, FINSEQ_6,
FINSEQ_8, FINSEQ_1, FINSEQ_3, FINSEQ_5, RFINSEQ, INT_1, HELLY, PARTFUN1,
GLIB_006, GLIB_007, GLIB_003, FUNCT_7, EQREL_1, WELLORD2;
schemes NAT_1, FUNCT_1;
begin :: Preliminaries
Lm12:
for p being non empty FinSequence, x being object
for n being Element of dom(p^<*x*>) st n <= len(p^<*x*>) - 1
holds n = len(p^<*x*>) - 1 or n <= len p - 1
proof
let p be non empty FinSequence, x be object, n be Element of dom(p^<*x*>);
A1: len(p^<*x*>) = len p + len <*x*> by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:39;
assume A2: n <= len(p^<*x*>) - 1;
assume n <> len(p^<*x*>) - 1; then
A3: n < len p - 1 + 1 by A1, A2, XXREAL_0:1;
len p - 1 is Nat by INT_1:74;
hence n <= len p - 1 by A3, NAT_1:13;
end;
Lm13:
for p being non empty FinSequence, x being object
for n being Element of dom(<*x*>^p) st n <= len(<*x*>^p) - 1
holds n = 1 or (n-1 in dom p & n-1 <= len p - 1)
proof
let p be non empty FinSequence, x be object, n be Element of dom(<*x*>^p);
A1: len(<*x*>^p) = len <*x*> + len p by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:39;
assume n <= len(<*x*>^p) - 1; then
A2: n-1 <= len p - 1 by A1, XREAL_1:9; then
A3: n-1 + 0 <= len p - 1 + 1 by XREAL_1:7;
assume A4: n <> 1;
n is non zero by FINSEQ_3:25; then
A5: n-1 is Nat by INT_1:74;
1 <= n-1
proof
assume not 1 <= n-1;
then n-1 = 0 by A5, NAT_1:14;
hence contradiction by A4;
end;
hence n-1 in dom p by A3, A5, FINSEQ_3:25;
thus n-1 <= len p - 1 by A2;
end;
::$CT 18
:: START into GLIB_002 ?
Lm6: for G being _finite connected _Graph
ex H being Subgraph of G st H is spanning Tree-like connected acyclic
proof
defpred P[Nat] means for G being _finite connected _Graph
st G.order() + $1 = G.size() + 1
ex H being Subgraph of G st H is spanning Tree-like connected acyclic;
A1: P[0]
proof
let G be _finite connected _Graph;
assume A2: G.order() + 0 = G.size() + 1;
reconsider H = G as Subgraph of G by GLIB_000:40;
take H;
the_Vertices_of H = the_Vertices_of G;
hence H is spanning by GLIB_000:def 33;
thus H is Tree-like by A2, GLIB_002:47;
hence thesis;
end;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
let G be _finite connected _Graph;
assume A5: G.order() + (k+1) = G.size() + 1;
:: we want to remove an edge that is part of a cycle
:: so that the resulting subgraph is still connected
k+1 <> 0;
then G.order() <> G.size() + 1 by A5;
then G is non acyclic by GLIB_002:47;
then consider C being Walk of G such that
A6: C is Cycle-like by GLIB_002:def 2;
A7: C.edges() is non empty by A6, GLIB_001:136;
set e = the Element of C.edges();
set G2 = the removeEdge of G, e;
A8: G2 is connected by A6, A7, GLIB_002:5;
G.order() + k + 1 = G2.size() + 1 + 1
by A5, A7, TARSKI:def 3, GLIB_000:52;
then G2.order() + k = G2.size() + 1 by GLIB_000:52;
then consider H being Subgraph of G2 such that
A9: H is spanning Tree-like connected acyclic by A4, A8;
reconsider H as spanning Subgraph of G by A9, GLIB_000:74;
take H;
thus thesis by A9;
end;
A10: for k being Nat holds P[k] from NAT_1:sch 2(A1,A3);
let G be _finite connected _Graph;
ex k being Nat st
G.size() + 1 = G.order() + k by GLIB_002:40, NAT_1:10;
hence thesis by A10;
end;
registration
let G be _finite connected _Graph;
cluster spanning Tree-like connected acyclic for Subgraph of G;
existence by Lm6;
end;
theorem Th19:
for G1 being connected _Graph, G2 being Subgraph of G1
st the_Edges_of G1 c= the_Edges_of G2 holds G1 == G2
proof
let G1 be connected _Graph, G2 be Subgraph of G1;
assume A1: the_Edges_of G1 c= the_Edges_of G2;
A2: the_Edges_of G1 = the_Edges_of G2 by A1, XBOOLE_0:def 10;
A3: G1 is Subgraph of G1 by GLIB_000:40;
the_Vertices_of G1 = the_Vertices_of G2
proof
per cases;
suppose A4: G1 is non _trivial;
assume the_Vertices_of G1 <> the_Vertices_of G2;
then not the_Vertices_of G1 c= the_Vertices_of G2 by XBOOLE_0:def 10;
then A5: the_Vertices_of G1 \ the_Vertices_of G2 <> {} by XBOOLE_1:37;
set v = the Element of the_Vertices_of G1 \ the_Vertices_of G2;
reconsider v as Vertex of G1 by A5, TARSKI:def 3;
per cases;
suppose v.edgesInOut() = {};
hence contradiction by A4, GLIB_000:def 49;
end;
suppose A6: v.edgesInOut() <> {};
set e = the Element of v.edgesInOut();
per cases by A6, GLIB_000:61;
suppose A7: (the_Source_of G1).e = v;
A8: e in the_Edges_of G2 by A2, A6, GLIB_000:61;
then (the_Source_of G2).e = v by A7, GLIB_000:def 32;
then v in the_Vertices_of G2 by A8, FUNCT_2:5;
hence contradiction by A5, XBOOLE_0:def 5;
end;
suppose A9: (the_Target_of G1).e = v;
A10: e in the_Edges_of G2 by A2, A6, GLIB_000:61;
then (the_Target_of G2).e = v by A9, GLIB_000:def 32;
then v in the_Vertices_of G2 by A10, FUNCT_2:5;
hence contradiction by A5, XBOOLE_0:def 5;
end;
end;
end;
suppose A11: G1 is _trivial;
then consider v1 being Vertex of G1 such that
A12: the_Vertices_of G1 = {v1} by GLIB_000:22;
consider v2 being Vertex of G2 such that
A13: the_Vertices_of G2 = {v2} by A11, GLIB_000:22;
thus thesis by A12, A13, ZFMISC_1:3;
end;
end;
hence thesis by A2, A3, GLIB_000:86;
end;
theorem
for G1 being _finite connected _Graph, G2 being Subgraph of G1
st G1.size() = G2.size() holds G1 == G2
proof
let G1 be _finite connected _Graph, G2 be Subgraph of G1;
assume A1: G1.size() = G2.size();
card the_Edges_of G2 = G2.size() by GLIB_000:def 25
.= card the_Edges_of G1 by A1, GLIB_000:def 25;
then the_Edges_of G1 = the_Edges_of G2 by CARD_2:102;
hence thesis by Th19;
end;
theorem Th21:
for G1 being _finite Tree-like _Graph
for G2 being spanning Tree-like Subgraph of G1
holds G1 == G2
proof
let G1 be _finite Tree-like _Graph, G2 be spanning Tree-like Subgraph of G1;
G1.order() = G2.order() by GLIB_000:117;
then G1.size() + 1 = G2.order() by GLIB_002:47;
then G1.size() + 1 = G2.size() + 1 by GLIB_002:47;
hence thesis by GLIB_000:119;
end;
registration
let G be non _trivial _Graph;
cluster non spanning _trivial connected for Subgraph of G;
existence
proof
set v = the Vertex of G;
set H = the inducedSubgraph of G, {v};
the_Vertices_of H <> the_Vertices_of G
proof
assume A1: the_Vertices_of H = the_Vertices_of G;
1 = card the_Vertices_of G by A1, GLIB_000:def 19;
hence contradiction by GLIB_000:def 19;
end;
hence thesis by GLIB_000:def 33;
end;
end;
:: counterpart of GLIB_002:12
theorem Th22:
for G being _Graph, v1, v2 being Vertex of G st not v1 in G.reachableFrom(v2)
holds G.reachableFrom(v1) misses G.reachableFrom(v2)
proof
let G be _Graph, v1, v2 be Vertex of G;
assume A1: not v1 in G.reachableFrom(v2);
assume not G.reachableFrom(v1) misses G.reachableFrom(v2);
then G.reachableFrom(v1) /\ G.reachableFrom(v2) <> {} by XBOOLE_0:def 7;
then consider w being object such that
A2: w in G.reachableFrom(v1) /\ G.reachableFrom(v2) by XBOOLE_0:def 1;
A3: w in G.reachableFrom(v1) & w in G.reachableFrom(v2)
by A2, XBOOLE_0:def 4;
then consider W1 being Walk of G such that
A4: W1 is_Walk_from v1,w by GLIB_002:def 5;
consider W2 being Walk of G such that
A5: W2 is_Walk_from v2,w by A3, GLIB_002:def 5;
W1.reverse() is_Walk_from w,v1 by A4, GLIB_001:23;
then W2.append(W1.reverse()) is_Walk_from v2,v1 by A5, GLIB_001:31;
hence contradiction by A1, GLIB_002:def 5;
end;
theorem Th23:
for G being _Graph holds G.componentSet() is a_partition of the_Vertices_of G
proof
let G be _Graph;
set V = the_Vertices_of G;
A1: union G.componentSet() = V by GLIB_002:24;
for A being Subset of V st A in G.componentSet() holds A <> {} &
for B being Subset of V st B in G.componentSet() holds A = B or A misses B
proof
let A be Subset of V;
assume A in G.componentSet();
then consider v being Vertex of G such that
A2: A = G.reachableFrom(v) by GLIB_002:def 8;
thus A <> {} by A2;
let B be Subset of V;
assume B in G.componentSet();
then consider w being Vertex of G such that
A3: B = G.reachableFrom(w) by GLIB_002:def 8;
per cases;
suppose v in G.reachableFrom(w);
hence thesis by A2, A3, GLIB_002:12;
end;
suppose not v in G.reachableFrom(w);
hence thesis by A2, A3, Th22;
end;
end;
hence thesis by A1, EQREL_1:def 4;
end;
theorem Th24:
for G being _Graph, C being a_partition of the_Vertices_of G,
v being Vertex of G
st C = G.componentSet() holds EqClass(v,C) = G.reachableFrom(v)
proof
let G be _Graph, C be a_partition of the_Vertices_of G, v be Vertex of G;
assume A1: C = G.componentSet();
EqClass(v,C) in C by EQREL_1:def 6;
then consider w being Vertex of G such that
A2: EqClass(v,C) = G.reachableFrom(w) by A1, GLIB_002:def 8;
v in EqClass(v,C) by EQREL_1:def 6;
hence thesis by A2, GLIB_002:12;
end;
:: holds more generally when G is non trivial and v0 is non cut-vertex;
:: however, this theorem is used to show that endvertex implies non cut-vertex
theorem Th25:
for G1 being _Graph, v0, v1 being Vertex of G1
for G2 being removeVertex of G1,v0, v2 being Vertex of G2
st v0 is endvertex & v1 = v2 & v1 in G1.reachableFrom(v0)
holds G2.reachableFrom(v2) = G1.reachableFrom(v1) \ {v0}
proof
let G1 be _Graph, v0,v1 be Vertex of G1;
let G2 be removeVertex of G1, v0, v2 be Vertex of G2;
assume A1: v0 is endvertex & v1 = v2 & v1 in G1.reachableFrom(v0);
then A2: G1 is non _trivial by GLIB_000:122;
then A3: the_Vertices_of G2 = the_Vertices_of G1 \ {v0} by GLIB_000:47;
for w being object holds w in G2.reachableFrom(v2) iff
w in G1.reachableFrom(v1) & not w in {v0}
proof
let w be object;
thus w in G2.reachableFrom(v2) implies w in G1.reachableFrom(v1) &
not w in {v0} by A1, A3, GLIB_002:14, TARSKI:def 3, XBOOLE_0:def 5;
assume A4: w in G1.reachableFrom(v1) & not w in {v0};
then consider W being Walk of G1 such that
A5: W is_Walk_from v1, w by GLIB_002:def 5;
set P = the Path of W;
v1 is set & w is set by TARSKI:1;
then A6: P is_Walk_from v1, w by A5, GLIB_001:160;
not v0 in P.vertices()
proof
assume v0 in P.vertices();
then per cases by A1, GLIB_001:143;
suppose v0 = P.first();
then v0 = v2 by A1, A6, GLIB_001:def 23;
then not v0 in {v0} by A3, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
suppose v0 = P.last();
then v0 = w by A6, GLIB_001:def 23;
hence contradiction by A4, TARSKI:def 1;
end;
end;
then reconsider P as Walk of G2 by A2, GLIB_001:171;
P is_Walk_from v2, w by A1, A6, GLIB_001:19;
hence w in G2.reachableFrom(v2) by GLIB_002:def 5;
end;
hence thesis by XBOOLE_0:def 5;
end;
theorem Th26:
for G1 being non _trivial _Graph, v0,v1 being Vertex of G1
for G2 being removeVertex of G1, v0, v2 being Vertex of G2
st v1 = v2 & not v1 in G1.reachableFrom(v0)
holds G2.reachableFrom(v2) = G1.reachableFrom(v1)
proof
let G1 be non _trivial _Graph, v0,v1 be Vertex of G1;
let G2 be removeVertex of G1, v0, v2 be Vertex of G2;
assume A1: v1 = v2 & not v1 in G1.reachableFrom(v0);
then A2: G2.reachableFrom(v2) c= G1.reachableFrom(v1) by GLIB_002:14;
for w being object holds w in G1.reachableFrom(v1)
implies w in G2.reachableFrom(v2)
proof
let w be object;
assume w in G1.reachableFrom(v1);
then consider W being Walk of G1 such that
A3: W is_Walk_from v1, w by GLIB_002:def 5;
not v0 in W.vertices()
proof
assume A4: v0 in W.vertices();
reconsider m = 1 as odd Element of NAT by POLYFORM:4;
reconsider n = W.find(v0) as odd Element of NAT;
set U = W.cut(m,n);
m <= n & n <= len W by A4, GLIB_001:def 19, CHORD:2;
then U is_Walk_from W.m, W.n by GLIB_001:37;
then U is_Walk_from W.first(), W.n by GLIB_001:def 6;
then U is_Walk_from v1, W.n by A3, GLIB_001:def 23;
then U is_Walk_from v1, v0 by A4, GLIB_001:def 19;
then U.reverse() is_Walk_from v0, v1 by GLIB_001:23;
hence contradiction by A1, GLIB_002:def 5;
end;
then reconsider W2 = W as Walk of G2 by GLIB_001:171;
W2 is_Walk_from v2, w by A1, A3, GLIB_001:19;
hence w in G2.reachableFrom(v2) by GLIB_002:def 5;
end;
then G1.reachableFrom(v1) c= G2.reachableFrom(v2) by TARSKI:def 3;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem Th27:
for G being non _trivial _finite Tree-like _Graph, v being Vertex of G
st G.order() = 2 holds v is endvertex
proof
let G be non _trivial _finite Tree-like _Graph, v be Vertex of G;
assume G.order() = 2;
then card the_Vertices_of G = 2 by GLIB_000:def 24;
then consider v1, v2 being object such that
A1: v1 <> v2 & the_Vertices_of G = {v1,v2} by CARD_2:60;
consider w1,w2 being Vertex of G such that
A2: w1 <> w2 & w1 is endvertex & w2 is endvertex by GLIB_002:45;
(w1 = v1 or w1 = v2) & (w2 = v1 or w2 = v2) by A1, TARSKI:def 2;
then per cases by A2;
suppose w1 = v1 & w2 = v2;
hence thesis by A1, A2, TARSKI:def 2;
end;
suppose w1= v2 & w2 = v1;
hence thesis by A1, A2, TARSKI:def 2;
end;
end;
registration
let G be non _trivial connected _Graph, v be Vertex of G;
cluster v.allNeighbors() -> non empty;
coherence by GLIB_000:113;
end;
:: END into GLIB_002 ?
:: into HELLY ?
theorem
for T being _Tree, a being Vertex of T holds T.pathBetween(a,a) = T.walkOf(a)
proof
let T be _Tree, a be Vertex of T;
consider b being Vertex of T such that
A1: T.pathBetween(a,a) = T.walkOf(b) by GLIB_001:128;
{a} = T.pathBetween(a,a).vertices() by HELLY:30
.= {b} by A1, GLIB_001:90;
hence thesis by A1, ZFMISC_1:3;
end;
:: into HELLY ?
theorem Th29:
for T being _Tree, a,b being Vertex of T, e being object
st e Joins a,b,T holds T.pathBetween(a,b) = T.walkOf(a,e,b)
by GLIB_001:15, HELLY:def 2;
:: into HELLY ?
theorem Th30:
for T being non _trivial _finite _Tree, v being Vertex of T
ex v1, v2 being Vertex of T
st v1 <> v2 & v1 is endvertex & v2 is endvertex &
v in T.pathBetween(v1,v2).vertices()
proof
defpred P[Nat] means for T being non _trivial _finite _Tree
for v being Vertex of T st T.order() = $1 + 2 holds
ex v1, v2 being Vertex of T
st v1 <> v2 & v1 is endvertex & v2 is endvertex &
v in T.pathBetween(v1,v2).vertices();
A1: P[0]
proof
let T be non _trivial _finite _Tree, v be Vertex of T;
assume A2: T.order() = 0 + 2;
then card the_Vertices_of T = 2 by GLIB_000:def 24;
then consider v1, v2 being object such that
A3: v1 <> v2 & the_Vertices_of T = {v1,v2} by CARD_2:60;
reconsider v1, v2 as Vertex of T by A3, TARSKI:def 2;
take v1, v2;
thus v1 <> v2 by A3;
thus v1 is endvertex & v2 is endvertex by A2, Th27;
v = v1 or v = v2 by A3, TARSKI:def 2;
hence thesis by HELLY:29;
end;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
let T be non _trivial _finite _Tree, v be Vertex of T;
assume A6: T.order() = (k+1) + 2;
set v0 = the endvertex Vertex of T;
per cases;
suppose A7: v = v0;
consider v1, v2 being Vertex of T such that
A8: v1 <> v2 & v1 is endvertex & v2 is endvertex by GLIB_002:45;
per cases;
suppose A9: v <> v1;
take v, v1;
thus v <> v1 & v is endvertex & v1 is endvertex by A7, A8, A9;
thus thesis by HELLY:29;
end;
suppose A10: v = v1;
take v, v2;
thus v <> v2 & v is endvertex & v2 is endvertex by A8, A10;
thus thesis by HELLY:29;
end;
end;
suppose A11: v <> v0;
set T0 = the removeVertex of T, v0;
a12: T0.order() + 1 = k + 2 + 1 by A6, GLIB_000:48;
T0.order() <> 1
proof
assume T0.order() = 1;
then 0+1 = k + 1 + 1 by a12;
hence contradiction;
end;
then reconsider T0 as non _trivial _finite _Tree by GLIB_000:26;
not v in {v0} by A11, TARSKI:def 1;
then v in the_Vertices_of T \ {v0} by XBOOLE_0:def 5;
then v in the_Vertices_of T0 by GLIB_000:47;
then consider v1,v2 being Vertex of T0 such that
A13: v1 <> v2 & v1 is endvertex & v2 is endvertex and
A14: v in T0.pathBetween(v1,v2).vertices() by A5, a12;
the_Vertices_of T0 c= the_Vertices_of T by GLIB_000:def 32;
then reconsider w1 = v1, w2 = v2 as Vertex of T by TARSKI:def 3;
consider e0 being object such that
A15: v0.edgesInOut() = {e0} & not e0 Joins v0,v0,T by GLIB_000:def 51;
A16: the_Edges_of T0
= T.edgesBetween(the_Vertices_of T \ {v0}) by GLIB_000:47
.= T.edgesBetween(the_Vertices_of T) \ v0.edgesInOut() by GLIB_000:107
.= the_Edges_of T \ {e0} by A15, GLIB_000:34;
consider e1 being object such that
A17: v1.edgesInOut() = {e1} & not e1 Joins v1,v1,T0
by A13, GLIB_000:def 51;
consider e2 being object such that
A18: v2.edgesInOut() = {e2} & not e2 Joins v2,v2,T0
by A13, GLIB_000:def 51;
v0 in {v0} by TARSKI:def 1;
then not v0 in the_Vertices_of T \ {v0} by XBOOLE_0:def 5;
then A19: not v0 in the_Vertices_of T0 by GLIB_000:47;
A20: w1 <> v0.adj(e0) implies w1 is endvertex
proof
assume A21: w1 <> v0.adj(e0);
A22: v1.edgesInOut() c= w1.edgesInOut() by GLIB_000:78;
for e being object st e in w1.edgesInOut() holds e in v1.edgesInOut()
proof
let e be object;
assume A23: e in w1.edgesInOut();
e <> e0
proof
assume e = e0;
then A24: e0 Joins w1,w1.adj(e0),T by A23, GLIB_000:67;
e0 in v0.edgesInOut() by A15, TARSKI:def 1;
then e0 Joins v0,v0.adj(e0),T by GLIB_000:67;
then w1 = v0 or w1 = v0.adj(e0) by A24, GLIB_000:15;
hence contradiction by A19, A21;
end;
then not e in {e0} by TARSKI:def 1;
then A25: e in the_Edges_of T0 by A16, A23, XBOOLE_0:def 5;
then (the_Source_of T0).e = (the_Source_of T).e &
(the_Target_of T0).e = (the_Target_of T).e by GLIB_000:def 32;
then (the_Source_of T0).e = w1 or (the_Target_of T0).e = w1
by A23, GLIB_000:61;
hence thesis by A25, GLIB_000:61;
end;
then w1.edgesInOut() c= v1.edgesInOut() by TARSKI:def 3;
then v1.edgesInOut() = w1.edgesInOut() by A22, XBOOLE_0:def 10;
hence w1 is endvertex by A17, GLIB_000:18, GLIB_000:def 51;
end;
A26: w2 <> v0.adj(e0) implies w2 is endvertex
proof
assume A27: w2 <> v0.adj(e0);
A28: v2.edgesInOut() c= w2.edgesInOut() by GLIB_000:78;
for e being object st e in w2.edgesInOut() holds e in v2.edgesInOut()
proof
let e be object;
assume A29: e in w2.edgesInOut();
e <> e0
proof
assume e = e0;
then A30: e0 Joins w2,w2.adj(e0),T by A29, GLIB_000:67;
e0 in v0.edgesInOut() by A15, TARSKI:def 1;
then e0 Joins v0,v0.adj(e0),T by GLIB_000:67;
then w2 = v0 or w2 = v0.adj(e0) by A30, GLIB_000:15;
hence contradiction by A19, A27;
end;
then not e in {e0} by TARSKI:def 1;
then A31: e in the_Edges_of T0 by A16, A29, XBOOLE_0:def 5;
then (the_Source_of T0).e = (the_Source_of T).e &
(the_Target_of T0).e = (the_Target_of T).e by GLIB_000:def 32;
then (the_Source_of T0).e = w2 or (the_Target_of T0).e = w2
by A29, GLIB_000:61;
hence thesis by A31, GLIB_000:61;
end;
then w2.edgesInOut() c= v2.edgesInOut() by TARSKI:def 3;
then v2.edgesInOut() = w2.edgesInOut() by A28, XBOOLE_0:def 10;
hence w2 is endvertex by A18, GLIB_000:18, GLIB_000:def 51;
end;
A32: T0.pathBetween(v1,v2) = T.pathBetween(w1,w2) by HELLY:33;
per cases;
suppose A33: w1 = v0.adj(e0);
then A34: w2 <> v0.adj(e0) by A13;
take v0, w2;
thus v0 <> w2 & v0 is endvertex & w2 is endvertex by A19, A26, A34;
e0 in v0.edgesInOut() by A15, TARSKI:def 1;
then A35: e0 Joins v0, w1, T by A33, GLIB_000:67;
then A36: T.walkOf(v0,e0,w1) = T.pathBetween(v0,w1) by Th29;
set P1 = T.pathBetween(v0,w1), P2 = T.pathBetween(w1,w2);
set P = P1.append(P2);
A37: P1.last() = w1 & P2.first() = w1 by HELLY:28;
for x being object holds x in P1.vertices() /\ P2.vertices()
iff x = w1
proof
let x be object;
hereby
assume x in P1.vertices() /\ P2.vertices();
then A38: x in P1.vertices() & x in P2.vertices()
by XBOOLE_0:def 4;
then A39: x in {v0,w1} by A35, A36, GLIB_001:91;
x in T0.pathBetween(v1,v2).vertices() by A32, A38, GLIB_001:98;
then x in the_Vertices_of T0;
hence x = w1 by A19, A39, TARSKI:def 2;
end;
assume x = w1;
then x = P1.last() & x = P2.first() by HELLY:28;
then x in P1.vertices() & x in P2.vertices() by GLIB_001:88;
hence thesis by XBOOLE_0:def 4;
end;
then P1.vertices() /\ P2.vertices() = {P1.last()} by A37,TARSKI:def 1;
then reconsider P as Path of T by A37, HELLY:38;
P1 is_Walk_from v0,w1 & P2 is_Walk_from w1,w2 by HELLY:def 2;
then A40: P = T.pathBetween(v0,w2) by GLIB_001:31, HELLY:def 2;
T0.pathBetween(v1,v2).vertices() = P2.vertices()
by HELLY:33, GLIB_001:98;
then v in P1.vertices() \/ P2.vertices() by A14, XBOOLE_0:def 3;
hence thesis by A37, A40, GLIB_001:93;
end;
suppose A41: w2 = v0.adj(e0);
then A42: w1 <> v0.adj(e0) by A13;
take w1, v0;
thus w1 <> v0 & w1 is endvertex & v0 is endvertex by A19, A20, A42;
e0 in v0.edgesInOut() by A15, TARSKI:def 1;
then A43: e0 Joins w2, v0, T by A41, GLIB_000:67, GLIB_000:14;
then A44: T.walkOf(w2,e0,v0) = T.pathBetween(w2,v0) by Th29;
set P1 = T.pathBetween(w1,w2), P2 = T.pathBetween(w2,v0);
set P = P1.append(P2);
A45: P1.last() = w2 & P2.first() = w2 by HELLY:28;
for x being object holds x in P1.vertices() /\ P2.vertices()
iff x = w2
proof
let x be object;
hereby
assume x in P1.vertices() /\ P2.vertices();
then A46: x in P1.vertices() & x in P2.vertices()
by XBOOLE_0:def 4;
then A47: x in {w2,v0} by A43, A44, GLIB_001:91;
x in T0.pathBetween(v1,v2).vertices() by A32, A46, GLIB_001:98;
then x in the_Vertices_of T0;
hence x = w2 by A19, A47, TARSKI:def 2;
end;
assume x = w2;
then x in P1.vertices() & x in P2.vertices() by GLIB_001:88, A45;
hence thesis by XBOOLE_0:def 4;
end;
then P1.vertices() /\ P2.vertices() = {P1.last()} by A45,TARSKI:def 1;
then reconsider P as Path of T by A45, HELLY:38;
P1 is_Walk_from w1,w2 & P2 is_Walk_from w2,v0 by HELLY:def 2;
then A48: P = T.pathBetween(w1,v0) by GLIB_001:31, HELLY:def 2;
T0.pathBetween(v1,v2).vertices() = P1.vertices()
by HELLY:33, GLIB_001:98;
then v in P1.vertices() \/ P2.vertices() by A14, XBOOLE_0:def 3;
hence thesis by A45, A48, GLIB_001:93;
end;
suppose A49: w1 <> v0.adj(e0) & w2 <> v0.adj(e0);
take w1, w2;
thus w1<>w2 & w1 is endvertex & w2 is endvertex by A13, A20, A26, A49;
thus thesis by A14, GLIB_001:98, HELLY:33;
end;
end;
end;
A50: for k being Nat holds P[k] from NAT_1:sch 2(A1,A4);
let T be non _trivial _finite _Tree, v be Vertex of T;
T.order() >= 1 & T.order() <> 1 by GLIB_000:25, GLIB_000:26;
then T.order() > 1 by XXREAL_0:1;
then T.order() >= 1+1 by INT_1:7;
then consider k being Nat such that
A51: T.order() = 2 + k by NAT_1:10;
thus thesis by A50, A51;
end;
:: into HELLY ?
theorem Th31:
for G1 being non _trivial _finite Tree-like _Graph
for G2 being non spanning connected Subgraph of G1
ex v being Vertex of G1 st v is endvertex & not v in the_Vertices_of G2
proof
let G1 be non _trivial _finite Tree-like _Graph;
let G2 be non spanning connected Subgraph of G1;
assume A1: for v being Vertex of G1 holds not v is endvertex or
v in the_Vertices_of G2;
A2: not the_Vertices_of G1 c= the_Vertices_of G2
by GLIB_000:def 33, XBOOLE_0:def 10;
:: Now we show the negation
for x being object st x in the_Vertices_of G1 holds x in the_Vertices_of G2
proof
let x be object;
assume x in the_Vertices_of G1;
then reconsider v = x as Vertex of G1;
consider v1, v2 being Vertex of G1 such that
A3: v1 <> v2 & v1 is endvertex & v2 is endvertex and
A4: v in G1.pathBetween(v1,v2).vertices() by Th30;
reconsider w1 = v1, w2 = v2 as Vertex of G2 by A1, A3;
v in G2.pathBetween(w1,w2).vertices() by A4, HELLY:33, GLIB_001:98;
hence thesis;
end;
hence contradiction by A2, TARSKI:def 3;
end;
:: START into GLIB_006 ?
theorem Th32:
for G2, G3 being _Graph, V being set, G1 being addVertices of G2, V
st G2 == G3 holds G1 is addVertices of G3, V
proof
let G2, G3 be _Graph, V be set, G1 be addVertices of G2, V;
assume A1: G2 == G3;
then the_Vertices_of G3 = the_Vertices_of G2 &
the_Edges_of G3 = the_Edges_of G2 &
the_Target_of G3 = the_Target_of G2 &
the_Source_of G3 = the_Source_of G2 by GLIB_000:def 34;
then A2: the_Vertices_of G1 = the_Vertices_of G3 \/ V &
the_Edges_of G1 = the_Edges_of G3 &
the_Source_of G1 = the_Source_of G3 &
the_Target_of G1 = the_Target_of G3 by GLIB_006:def 10;
G2 is Supergraph of G3 by A1, GLIB_006:58;
then G1 is Supergraph of G3 by GLIB_006:62;
hence thesis by A2, GLIB_006:def 10;
end;
theorem Th33:
for G2 being _Graph, G1 being Supergraph of G2
st the_Edges_of G1 = the_Edges_of G2
holds G1 is addVertices of G2, the_Vertices_of G1 \ the_Vertices_of G2
proof
let G2 be _Graph, G1 be Supergraph of G2;
assume A1: the_Edges_of G1 = the_Edges_of G2;
the_Vertices_of G2 c= the_Vertices_of G1 by GLIB_006:def 9;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/
(the_Vertices_of G1 \ the_Vertices_of G2) by XBOOLE_1:45;
A3: the_Source_of G2 = (the_Source_of G1)|the_Edges_of G2 by GLIB_006:69
.= the_Source_of G1 by A1;
the_Target_of G2 = (the_Target_of G1)|the_Edges_of G2 by GLIB_006:69
.= the_Target_of G1 by A1;
hence thesis by A1, A2, A3, GLIB_006:def 10;
end;
theorem Th34:
for G1 being _finite _Graph, G2 being Subgraph of G1 st G1.size() = G2.size()
holds G1 is addVertices of G2, the_Vertices_of G1 \ the_Vertices_of G2
proof
let G1 be _finite _Graph, G2 be Subgraph of G1;
assume A1: G1.size() = G2.size();
card the_Edges_of G2 = G2.size() by GLIB_000:def 25
.= card the_Edges_of G1 by A1, GLIB_000:def 25;
then A2: the_Edges_of G1 = the_Edges_of G2 by CARD_2:102;
G1 is Supergraph of G2 by GLIB_006:57;
hence thesis by A2, Th33;
end;
theorem
for G1 being non _trivial _Graph, v being Vertex of G1
for G2 being removeVertex of G1, v st v is isolated
holds G1 is addVertex of G2, v
proof
let G1 be non _trivial _Graph, v be Vertex of G1;
let G2 be removeVertex of G1, v;
assume A1: v is isolated;
A2: G1 is Supergraph of G2 by GLIB_006:57;
A3: the_Vertices_of G1 = (the_Vertices_of G1 \ {v}) \/ {v} by ZFMISC_1:116
.= the_Vertices_of G2 \/ {v} by GLIB_000:47;
A4: the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34
.= G1.edgesBetween(the_Vertices_of G1 \ {v}) by A1, GLIB_000:108
.= the_Edges_of G2 by GLIB_000:47;
A5: dom the_Source_of G1 = the_Edges_of G1 by FUNCT_2:def 1
.= dom the_Source_of G2 by A4, FUNCT_2:def 1;
for e being object st e in dom the_Source_of G2 holds
(the_Source_of G2).e = (the_Source_of G1).e by GLIB_000:def 32;
then A6: the_Source_of G1 = the_Source_of G2 by A5, FUNCT_1:2;
A7: dom the_Target_of G1 = the_Edges_of G1 by FUNCT_2:def 1
.= dom the_Target_of G2 by A4, FUNCT_2:def 1;
for e being object st e in dom the_Target_of G2 holds
(the_Target_of G2).e = (the_Target_of G1).e by GLIB_000:def 32;
then the_Target_of G1 = the_Target_of G2 by A7, FUNCT_1:2;
hence thesis by A2, A3, A4, A6, GLIB_006:def 10;
end;
theorem Th36:
for G2, G3 being _Graph, v1,e,v2 being object, G1 being addEdge of G2,v1,e,v2
st G2 == G3 holds G1 is addEdge of G3,v1,e,v2
proof
let G2, G3 be _Graph, v1,e,v2 be object;
let G1 be addEdge of G2,v1,e,v2;
assume A1: G2 == G3;
then A2: the_Vertices_of G3 = the_Vertices_of G2 &
the_Edges_of G3 = the_Edges_of G2 &
the_Target_of G3 = the_Target_of G2 &
the_Source_of G3 = the_Source_of G2 by GLIB_000:def 34;
per cases;
suppose A3: v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
then A4: the_Vertices_of G1 = the_Vertices_of G3 &
the_Edges_of G1 = the_Edges_of G3 \/ {e} &
the_Source_of G1 = the_Source_of G3 +* (e .--> v1) &
the_Target_of G1 = the_Target_of G3 +* (e .--> v2)
by A2, GLIB_006:def 11;
G2 is Supergraph of G3 by A1, GLIB_006:58;
then G1 is Supergraph of G3 by GLIB_006:62;
hence thesis by A2, A3, A4, GLIB_006:def 11;
end;
suppose A5: not (v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2);
then G1 == G2 by GLIB_006:def 11;
then A6: G1 == G3 by A1, GLIB_000:85;
then G1 is Supergraph of G3 by GLIB_006:58;
hence thesis by A2, A5, A6, GLIB_006:def 11;
end;
end;
theorem Th37:
for G1 being _Graph, e being set, G2 being removeEdge of G1, e
st e in the_Edges_of G1
holds G1 is addEdge of G2, (the_Source_of G1).e, e, (the_Target_of G1).e
proof
let G1 be _Graph, e be set, G2 be removeEdge of G1, e;
assume A1: e in the_Edges_of G1;
set u = (the_Source_of G1).e, w = (the_Target_of G1).e;
A2: G1 is Supergraph of G2 by GLIB_006:57;
A3: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:51;
A4: the_Edges_of G1 = (the_Edges_of G1 \ {e}) \/ {e} by A1, ZFMISC_1:116
.= the_Edges_of G2 \/ {e} by GLIB_000:51;
A5: dom the_Source_of G1 = the_Edges_of G1 by FUNCT_2:def 1
.= dom the_Source_of G2 \/ dom({e} --> u) by A4, FUNCT_2:def 1
.= dom the_Source_of G2 \/ dom(e .--> u) by FUNCOP_1:def 9
.= dom(the_Source_of G2 +* (e .--> u)) by FUNCT_4:def 1;
for e0 being object st e0 in dom the_Source_of G1
holds (the_Source_of G1).e0 = (the_Source_of G2 +* (e .--> u)).e0
proof
let e0 be object;
assume A6: e0 in dom the_Source_of G1;
per cases;
suppose e0 = e;
hence (the_Source_of G1).e0
= (the_Source_of G2 +* (e .--> u)).e0 by FUNCT_4:113;
end;
suppose A7: e0 <> e;
then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G1 \ {e} by A6, XBOOLE_0:def 5;
then e0 in the_Edges_of G2 by GLIB_000:51;
hence (the_Source_of G1).e0 = (the_Source_of G2).e0 by GLIB_000:def 32
.= (the_Source_of G2 +* (e .--> u)).e0 by A7, FUNCT_4:83;
end;
end;
then A8: the_Source_of G1 = the_Source_of G2 +* (e .--> u) by A5, FUNCT_1:2;
A9: dom the_Target_of G1 = the_Edges_of G1 by FUNCT_2:def 1
.= dom the_Target_of G2 \/ dom({e} --> w) by A4, FUNCT_2:def 1
.= dom the_Target_of G2 \/ dom(e .--> w) by FUNCOP_1:def 9
.= dom(the_Target_of G2 +* (e .--> w)) by FUNCT_4:def 1;
for e0 being object st e0 in dom the_Target_of G1
holds (the_Target_of G1).e0 = (the_Target_of G2 +* (e .--> w)).e0
proof
let e0 be object;
assume A10: e0 in dom the_Target_of G1;
per cases;
suppose e0 = e;
hence (the_Target_of G1).e0
= (the_Target_of G2 +* (e .--> w)).e0 by FUNCT_4:113;
end;
suppose A11: e0 <> e;
then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G1 \ {e} by A10, XBOOLE_0:def 5;
then e0 in the_Edges_of G2 by GLIB_000:51;
hence (the_Target_of G1).e0 = (the_Target_of G2).e0 by GLIB_000:def 32
.= (the_Target_of G2 +* (e .--> w)).e0 by A11, FUNCT_4:83;
end;
end;
then A12: the_Target_of G1 = the_Target_of G2 +*(e .--> w) by A9, FUNCT_1:2;
A13: u in the_Vertices_of G2 & w in the_Vertices_of G2 by A1, A3, FUNCT_2:5;
e in {e} by TARSKI:def 1;
then not e in the_Edges_of G1 \ {e} by XBOOLE_0:def 5;
then not e in the_Edges_of G2 by GLIB_000:51;
hence thesis by A2, A3, A4, A8, A12, A13, GLIB_006:def 11;
end;
theorem Th38:
for G1 being non _trivial _Graph, v being Vertex of G1, e being object
for G2 being removeVertex of G1, v
st {e} = v.edgesInOut() & not e Joins v,v,G1 :: i.e. v is endvertex
holds G1 is addAdjVertex of G2, v.adj(e), e, v
or G1 is addAdjVertex of G2, v, e, v.adj(e)
proof
let G1 be non _trivial _Graph, v be Vertex of G1, e be object;
let G2 be removeVertex of G1, v;
assume A1: {e} = v.edgesInOut() & not e Joins v,v,G1;
A2: G1 is Supergraph of G2 by GLIB_006:57;
A3: the_Vertices_of G1 = (the_Vertices_of G1 \ {v}) \/ {v} by ZFMISC_1:116
.= the_Vertices_of G2 \/ {v} by GLIB_000:47;
A4: e in {e} by TARSKI:def 1;
A5: the_Edges_of G1 = (the_Edges_of G1 \ {e}) \/ {e} by A1, A4, ZFMISC_1:116
.= (G1.edgesBetween(the_Vertices_of G1) \ v.edgesInOut()) \/ {e}
by A1, GLIB_000:34
.= G1.edgesBetween(the_Vertices_of G1 \ {v}) \/ {e} by GLIB_000:107
.= the_Edges_of G2 \/ {e} by GLIB_000:47;
set u = (the_Source_of G1).e, w = (the_Target_of G1).e;
v in {v} by TARSKI:def 1;
then not v in the_Vertices_of G1 \ {v} by XBOOLE_0:def 5;
then A6: not v in the_Vertices_of G2 by GLIB_000:47;
not e in G1.edgesBetween(the_Vertices_of G1) \ v.edgesInOut()
by A1, A4, XBOOLE_0:def 5;
then not e in G1.edgesBetween(the_Vertices_of G1 \ {v}) by GLIB_000:107;
then A7: not e in the_Edges_of G2 by GLIB_000:47;
e in v.edgesInOut() by A1, TARSKI:def 1;
then A8: v <> v.adj(e) by A1, GLIB_000:67;
then not v.adj(e) in {v} by TARSKI:def 1;
then v.adj(e) in the_Vertices_of G1 \ {v} by XBOOLE_0:def 5;
then A9: v.adj(e) in the_Vertices_of G2 by GLIB_000:47;
A10: dom the_Source_of G1 = the_Edges_of G1 by FUNCT_2:def 1
.= dom the_Source_of G2 \/ {e} by A5, FUNCT_2:def 1;
A11: dom the_Target_of G1 = the_Edges_of G1 by FUNCT_2:def 1
.= dom the_Target_of G2 \/ {e} by A5, FUNCT_2:def 1;
e in v.edgesInOut() by A1, TARSKI:def 1;
then per cases by GLIB_000:61;
suppose A12: u = v;
then A13: w = v.adj(e) by A1, A4, A8, GLIB_000:def 41;
:: we show G1 is addAdjVertex of G2, v, e, v.adj(e)
:: using the second part of the definition
A14: dom the_Source_of G1 = dom the_Source_of G2 \/ dom({e} --> v)
by A10
.= dom(the_Source_of G2 +* ({e} --> v)) by FUNCT_4:def 1
.= dom(the_Source_of G2 +* (e .--> v)) by FUNCOP_1:def 9;
for e0 being object st e0 in dom the_Source_of G1
holds (the_Source_of G1).e0 = (the_Source_of G2 +* (e .--> v)).e0
proof
let e0 be object;
assume A15: e0 in dom the_Source_of G1;
per cases;
suppose e0 = e;
hence (the_Source_of G1).e0
= (the_Source_of G2 +* (e .--> v)).e0 by A12, FUNCT_4:113;
end;
suppose A16: e0 <> e;
then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G2 by A5, A15, XBOOLE_0:def 3;
hence (the_Source_of G1).e0 = (the_Source_of G2).e0 by GLIB_000:def 32
.= (the_Source_of G2 +* (e .--> v)).e0 by A16, FUNCT_4:83;
end;
end;
then A17: the_Source_of G1 = the_Source_of G2 +* (e .--> v)
by A14, FUNCT_1:2;
A18: dom the_Target_of G1 = dom the_Target_of G2 \/ dom({e} --> v.adj(e))
by A11
.= dom(the_Target_of G2 +* ({e} --> v.adj(e))) by FUNCT_4:def 1
.= dom(the_Target_of G2 +* (e .--> v.adj(e))) by FUNCOP_1:def 9;
for e0 being object st e0 in dom the_Target_of G1
holds (the_Target_of G1).e0 = (the_Target_of G2 +* (e .--> v.adj(e))).e0
proof
let e0 be object;
assume A19: e0 in dom the_Target_of G1;
per cases;
suppose e0 = e;
hence (the_Target_of G1).e0 =
(the_Target_of G2 +* (e .--> v.adj(e))).e0 by A13, FUNCT_4:113;
end;
suppose A20: e0 <> e;
then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G2 by A5, A19, XBOOLE_0:def 3;
hence (the_Target_of G1).e0 = (the_Target_of G2).e0 by GLIB_000:def 32
.= (the_Target_of G2 +* (e .--> v.adj(e))).e0 by A20, FUNCT_4:83;
end;
end;
then the_Target_of G1 = the_Target_of G2 +* (e .--> v.adj(e))
by A18, FUNCT_1:2;
hence thesis by A2, A3, A5, A6, A7, A9, A17, GLIB_006:def 12;
end;
suppose A21: w = v;
then A22: u = v.adj(e) by A1, A4, GLIB_000:def 41;
:: we show G1 is addAdjVertex of G2, v.adj(e), e, v
:: using the first part of the definition
A23: dom the_Target_of G1 = dom the_Target_of G2 \/ dom({e} --> v)
by A11
.= dom(the_Target_of G2 +* ({e} --> v)) by FUNCT_4:def 1
.= dom(the_Target_of G2 +* (e .--> v)) by FUNCOP_1:def 9;
for e0 being object st e0 in dom the_Target_of G1
holds (the_Target_of G1).e0 = (the_Target_of G2 +* (e .--> v)).e0
proof
let e0 be object;
assume A24: e0 in dom the_Target_of G1;
per cases;
suppose e0 = e;
hence (the_Target_of G1).e0 =
(the_Target_of G2 +* (e .--> v)).e0 by A21, FUNCT_4:113;
end;
suppose A25: e0 <> e;
then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G2 by A5, A24, XBOOLE_0:def 3;
hence (the_Target_of G1).e0 = (the_Target_of G2).e0 by GLIB_000:def 32
.= (the_Target_of G2 +* (e .--> v)).e0 by A25, FUNCT_4:83;
end;
end;
then A26: the_Target_of G1 = the_Target_of G2 +* (e .--> v)
by A23, FUNCT_1:2;
A27: dom the_Source_of G1 = dom the_Source_of G2 \/ dom({e} --> v.adj(e))
by A10
.= dom(the_Source_of G2 +* ({e} --> v.adj(e))) by FUNCT_4:def 1
.= dom(the_Source_of G2 +* (e .--> v.adj(e))) by FUNCOP_1:def 9;
for e0 being object st e0 in dom the_Source_of G1
holds (the_Source_of G1).e0 = (the_Source_of G2 +* (e .--> v.adj(e))).e0
proof
let e0 be object;
assume A28: e0 in dom the_Source_of G1;
per cases;
suppose e0 = e;
hence (the_Source_of G1).e0 =
(the_Source_of G2 +* (e .--> v.adj(e))).e0 by A22, FUNCT_4:113;
end;
suppose A29: e0 <> e;
then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G2 by A5, A28, XBOOLE_0:def 3;
hence (the_Source_of G1).e0 = (the_Source_of G2).e0 by GLIB_000:def 32
.= (the_Source_of G2 +* (e .--> v.adj(e))).e0 by A29, FUNCT_4:83;
end;
end;
then the_Source_of G1 = the_Source_of G2 +* (e .--> v.adj(e))
by A27, FUNCT_1:2;
hence thesis by A2, A3, A5, A6, A7, A9, A26, GLIB_006:def 12;
end;
end;
theorem Th39:
for G2 being _Graph, v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
for w being Vertex of G1, v being Vertex of G2
st v2 in G2.reachableFrom(v1) & v = w
holds G1.reachableFrom(w) = G2.reachableFrom(v)
proof
let G2 be _Graph, v1,v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
let w be Vertex of G1, v be Vertex of G2;
assume that
A1: v2 in G2.reachableFrom(v1) and
A2: w = v;
per cases;
suppose A3: not e in the_Edges_of G2;
G2 is Subgraph of G1 by GLIB_006:57;
then A4: G2.reachableFrom(v) c= G1.reachableFrom(w) by A2, GLIB_002:14;
for y being object holds y in G1.reachableFrom(w)
implies y in G2.reachableFrom(v)
proof
let y be object;
assume y in G1.reachableFrom(w);
then consider W1 being Walk of G1 such that
A5: W1 is_Walk_from w,y by GLIB_002:def 5;
set T = the Trail of W1;
y is set by TARSKI:1;
then A6: T is_Walk_from w,y by A5, GLIB_001:160;
per cases;
suppose not e in T.edges();
then reconsider W2 = T as Walk of G2 by GLIB_006:109;
W2 is_Walk_from v,y by A6, A2, GLIB_001:19;
hence y in G2.reachableFrom(v) by GLIB_002:def 5;
end;
suppose e in T.edges();
then consider w1, w2 being Vertex of G1, n being odd Element of NAT
such that
A7: n+2 <= len T and
A8: w1 = T.n & e = T.(n+1) & w2 = T.(n+2) and
A9: e Joins w1,w2,G1 by GLIB_001:103;
set E = G1.walkOf(w1,e,w2);
A10: E is_odd_substring_of T,0 by A7, A8, GLIB_006:27;
e DJoins v1,v2,G1 by A3, GLIB_006:105;
then A11: e Joins v1,v2,G1 by GLIB_000:16;
then per cases by A9, GLIB_000:15;
suppose A12: v1 = w1 & v2 = w2;
consider W2 being Walk of G2 such that
A13: W2 is_Walk_from v1,v2 by A1, GLIB_002:def 5;
reconsider W4 = W2 as Walk of G1 by GLIB_006:75;
not e in W2.edges() by A3;
then A14: not e in W4.edges() by GLIB_001:110;
set W5 = T.replaceEdgeWith(e,W4);
A15: W5 is_Walk_from v,y by A2, A6, GLIB_006:47;
W2.first() = v1 & W2.last() = v2 by A13, GLIB_001:def 23;
then W4.first() = v1 & W4.last() = v2 by GLIB_001:16;
then not e in W5.edges() by A11, A14, GLIB_006:40, A10, A12;
then reconsider W = W5 as Walk of G2 by GLIB_006:109;
W is_Walk_from v,y by A15, GLIB_001:19;
hence y in G2.reachableFrom(v) by GLIB_002:def 5;
end;
suppose A17: v1 = w2 & v2 = w1;
consider W3 being Walk of G2 such that
A18: W3 is_Walk_from v1,v2 by A1, GLIB_002:def 5;
A19: W3.reverse() is_Walk_from v2,v1 by A18, GLIB_001:23;
reconsider W4 = W3.reverse() as Walk of G1 by GLIB_006:75;
not e in W3.reverse().edges() by A3;
then A20: not e in W4.edges() by GLIB_001:110;
set W5 = T.replaceEdgeWith(e,W4);
A21: W5 is_Walk_from v,y by A2, A6, GLIB_006:47;
W3.reverse().first() = v2 & W3.reverse().last() = v1
by A19, GLIB_001:def 23;
then W4.first() = v2 & W4.last() = v1 by GLIB_001:16;
then not e in W5.edges()
by A11, A20, GLIB_006:40, GLIB_000:14, A10, A17;
then reconsider W = W5 as Walk of G2 by GLIB_006:109;
W is_Walk_from v,y by A21, GLIB_001:19;
hence y in G2.reachableFrom(v) by GLIB_002:def 5;
end;
end;
end;
then G1.reachableFrom(w) c= G2.reachableFrom(v) by TARSKI:def 3;
hence G1.reachableFrom(w) = G2.reachableFrom(v) by A4, XBOOLE_0:def 10;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 11;
hence thesis by A2, GLIB_002:17;
end;
end;
theorem Th40:
for G2 being _Graph, v1, v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
st v2 in G2.reachableFrom(v1) holds G1.componentSet() = G2.componentSet()
proof
let G2 be _Graph, v1,v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
assume A1: v2 in G2.reachableFrom(v1);
per cases;
suppose A2: not e in the_Edges_of G2;
then A3: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_006:def 11;
for x being set holds x in G2.componentSet() iff ex v being Vertex of G1
st x = G1.reachableFrom(v)
proof
let x be set;
hereby
assume x in G2.componentSet();
then consider v0 being Vertex of G2 such that
A4: x = G2.reachableFrom(v0) by GLIB_002:def 8;
reconsider v = v0 as Vertex of G1 by A2, GLIB_006:def 11;
take v;
thus x = G1.reachableFrom(v) by A1, A4, Th39;
end;
given v being Vertex of G1 such that
A5: x = G1.reachableFrom(v);
ex v0 being Vertex of G2 st x = G2.reachableFrom(v0)
proof
reconsider v0 = v as Vertex of G2 by A2, GLIB_006:def 11;
take v0;
thus thesis by A1, A5, Th39;
end;
hence x in G2.componentSet() by GLIB_002:def 8;
end;
hence G1.componentSet() = G2.componentSet() by A3, GLIB_002:def 8;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 11;
hence thesis by GLIB_002:26;
end;
end;
:: v1 and v2 are connected in supergraph
theorem Th41:
for G2 being _Graph, v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
for w1, w2 being Vertex of G1
st not e in the_Edges_of G2 & w1 = v1 & w2 = v2
holds w2 in G1.reachableFrom(w1)
proof
let G2 be _Graph, v1,v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
let w1, w2 be Vertex of G1;
assume that
A1: not e in the_Edges_of G2 and
A2: w1 = v1 & w2 = v2;
e DJoins v1,v2,G1 by A1, GLIB_006:105;
then e Joins w1,v2,G1 by A2, GLIB_000:16;
then G1.walkOf(w1,e,w2) is_Walk_from w1,w2 by A2, GLIB_001:15;
hence thesis by GLIB_002:def 5;
end;
:: their components are connected as well
theorem Th42:
for G2 being _Graph, v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
for w1 being Vertex of G1
st not e in the_Edges_of G2 & w1 = v1
holds G1.reachableFrom(w1) = G2.reachableFrom(v1) \/ G2.reachableFrom(v2)
proof
let G2 be _Graph, v1,v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2, w1 be Vertex of G1;
assume A1: not e in the_Edges_of G2 & w1 = v1;
A2: G2 is Subgraph of G1 by GLIB_006:57;
e DJoins v1,v2,G1 by A1, GLIB_006:105;
then A3: e Joins v1,v2,G1 by GLIB_000:16;
for x being object holds x in G1.reachableFrom(w1)
implies x in G2.reachableFrom(v1) \/ G2.reachableFrom(v2)
proof
let x be object;
assume A4: x in G1.reachableFrom(w1);
per cases;
suppose x = w1;
then x in G2.reachableFrom(v1) by GLIB_002:9, A1;
hence thesis by XBOOLE_0:def 3;
end;
suppose A5: x <> w1;
consider W1 being Walk of G1 such that
A6: W1 is_Walk_from w1, x by A4, GLIB_002:def 5;
set P1 = the Path of W1.reverse();
A7: W1.reverse() is_Walk_from x, w1 by A6, GLIB_001:23;
x is set by TARSKI:1;
then A8: P1 is_Walk_from x, w1 by A7, GLIB_001:160;
per cases;
suppose not e in P1.edges();
then reconsider W2 = P1 as Walk of G2 by GLIB_006:109;
W2 is_Walk_from x, w1 by A8, GLIB_001:19;
then W2.reverse() is_Walk_from v1, x by A1, GLIB_001:23;
then x in G2.reachableFrom(v1) by GLIB_002:def 5;
hence thesis by XBOOLE_0:def 3;
end;
suppose e in P1.edges();
then consider u1, u2 being Vertex of G1, n being odd Element of NAT
such that
A9: n+2 <= len P1 & u1 = P1.n & e = P1.(n+1) & u2 = P1.(n+2) and
A10: e Joins u1,u2,G1 by GLIB_001:103;
A11: v2 = u1 & v1 = u2
proof
assume not (v2 = u1 & v1 = u2);
then A12: v1 = P1.n by A3, A9, A10, GLIB_000:15;
A13: P1.len P1 = P1.last() by GLIB_001:def 7
.= v1 by A1, A8, GLIB_001:def 23;
n+2-2 < len P1 - 0 by A9, XREAL_1:15;
then n = 1 by A12, A13, GLIB_001:def 28;
then v1 = P1.first() by A12, GLIB_001:def 6
.= x by A8, GLIB_001:def 23;
hence contradiction by A1, A5;
end;
set P2 = P1.cut(1,n);
not e in P2.edges()
proof
assume e in P2.edges();
then consider u3, u4 being Vertex of G1, m being odd Element of NAT
such that
A14: m+2 <= len P2 & u3 = P2.m & e = P2.(m+1) & u4 = P2.(m+2) and
e Joins u3,u4,G1 by GLIB_001:103;
n+2-2 <= len P1 - 0 by A9, XREAL_1:13;
then A15: 1 <= n & n <= len P1 by ABIAN:12;
A16: m+2-2 < len P2 - 0 by A14, XREAL_1:15;
then A17: P1.(m+1) = P1.(n+1)
by A9, A14, A15, POLYFORM:4, GLIB_001:36;
A18: 1+0 <= m+1 & m < n by A15, A16, GLIB_001:45, XREAL_1:7;
then A19: m+1 < n+1 by XREAL_1:6;
n+2-1 <= len P1 - 0 by A9, XREAL_1:13;
hence contradiction by A17, A18, A19, GLIB_001:138;
end;
then reconsider W2 = P2 as Walk of G2 by GLIB_006:109;
n+2-2 <= len P1 - 0 by A9, XREAL_1:13;
then 1 <= n & n <= len P1 by ABIAN:12;
then P2 is_Walk_from P1.1, P1.n by POLYFORM:4, GLIB_001:37;
then W2 is_Walk_from P1.1, P1.n by GLIB_001:19;
then W2 is_Walk_from P1.first(), P1.n by GLIB_001:def 6;
then W2 is_Walk_from x, v2 by A8, A9, A11, GLIB_001:def 23;
then W2.reverse() is_Walk_from v2, x by GLIB_001:23;
then x in G2.reachableFrom(v2) by GLIB_002:def 5;
hence thesis by XBOOLE_0:def 3;
end;
end;
end;
then A20: G1.reachableFrom(w1)
c= G2.reachableFrom(v1) \/ G2.reachableFrom(v2) by TARSKI:def 3;
A21: G2.reachableFrom(v1) c= G1.reachableFrom(w1) by A1, A2, GLIB_002:14;
reconsider w2 = v2 as Vertex of G1 by GLIB_006:68;
G2.reachableFrom(v2) c= G1.reachableFrom(w2) by A2, GLIB_002:14;
then G2.reachableFrom(v2) c= G1.reachableFrom(w1)
by A1, Th41, GLIB_002:12;
then G2.reachableFrom(v1) \/ G2.reachableFrom(v2)
c= G1.reachableFrom(w1) by A21, XBOOLE_1:8;
hence thesis by A20, XBOOLE_0:def 10;
end;
:: the other components stay unaffected
theorem Th43:
for G2 being _Graph, v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
for w being Vertex of G1, v being Vertex of G2
st not e in the_Edges_of G2 & v = w &
not v in G2.reachableFrom(v1) & not v in G2.reachableFrom(v2)
holds G1.reachableFrom(w) = G2.reachableFrom(v)
proof
let G2 be _Graph, v1,v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
let w be Vertex of G1, v be Vertex of G2;
assume that
A1: not e in the_Edges_of G2 & v = w and
A2: not v in G2.reachableFrom(v1) & not v in G2.reachableFrom(v2);
e DJoins v1,v2,G1 by A1, GLIB_006:105;
then A3: e Joins v1,v2,G1 by GLIB_000:16;
for x being object holds
x in G1.reachableFrom(w) implies x in G2.reachableFrom(v)
proof
let x be object;
assume x in G1.reachableFrom(w);
then consider W1 being Walk of G1 such that
A4: W1 is_Walk_from w,x by GLIB_002:def 5;
set T1 = the Trail of W1;
x is set by TARSKI:1;
then A5: T1 is_Walk_from w,x by A4, GLIB_001:160;
not e in T1.edges()
proof
assume e in T1.edges();
then consider u1, u2 being Vertex of G1, n being odd Element of NAT
such that
A6: n+2 <= len T1 & u1 = T1.n & e = T1.(n+1) & u2 = T1.(n+2) and
A7: e Joins u1,u2,G1 by GLIB_001:103;
set T2 = T1.cut(1,n);
n+2-2 <= len T1 - 0 by A6, XREAL_1:13;
then A8: 1 <= n & n <= len T1 by ABIAN:12;
not e in T2.edges()
proof
assume e in T2.edges();
then consider u3, u4 being Vertex of G1, m being odd Element of NAT
such that
A9: m+2 <= len T2 & u3 = T2.m & e = T2.(m+1) & u4 = T2.(m+2) and
e Joins u3,u4,G1 by GLIB_001:103;
A10: m+2-2 < len T2 - 0 by A9, XREAL_1:15;
then A11: T1.(m+1) = T1.(n+1) by A6, A9, A8, POLYFORM:4, GLIB_001:36;
A12: 1+0 <= m+1 & m < n by A8, A10, XREAL_1:7, GLIB_001:45;
then A13: m+1 < n+1 by XREAL_1:6;
n+2-1 <= len T1 - 0 by A6, XREAL_1:13;
hence contradiction by A11, A12, A13, GLIB_001:138;
end;
then reconsider W2 = T2 as Walk of G2 by GLIB_006:109;
T2 is_Walk_from T1.1, T1.n by A8, POLYFORM:4, GLIB_001:37;
then T2 is_Walk_from T1.first(), T1.n by GLIB_001:def 6;
then T2 is_Walk_from w, T1.n by A5, GLIB_001:def 23;
then A14: W2 is_Walk_from v, u1 by A1, A6, GLIB_001:19;
per cases by A3, A7, GLIB_000:15;
suppose v1 = u1 & v2 = u2;
then W2.reverse() is_Walk_from v1, v by A14, GLIB_001:23;
hence contradiction by A2, GLIB_002:def 5;
end;
suppose v1 = u2 & v2 = u1;
then W2.reverse() is_Walk_from v2, v by A14, GLIB_001:23;
hence contradiction by A2, GLIB_002:def 5;
end;
end;
then reconsider W = T1 as Walk of G2 by GLIB_006:109;
W is_Walk_from w,x by A5, GLIB_001:19;
hence x in G2.reachableFrom(v) by A1, GLIB_002:def 5;
end;
then A15: G1.reachableFrom(w) c= G2.reachableFrom(v) by TARSKI:def 3;
G2 is Subgraph of G1 by GLIB_006:57;
then G2.reachableFrom(v) c= G1.reachableFrom(w) by A1, GLIB_002:14;
hence thesis by A15, XBOOLE_0:def 10;
end;
:: composition of component set in graph with added edge
theorem Th44:
for G2 being _Graph, v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
st not e in the_Edges_of G2
holds G1.componentSet() =
(G2.componentSet() \ {G2.reachableFrom(v1), G2.reachableFrom(v2)})
\/ {G2.reachableFrom(v1) \/ G2.reachableFrom(v2)}
proof
let G2 be _Graph, v1,v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2;
set V1 = G2.reachableFrom(v1), V2 = G2.reachableFrom(v2);
A2: G2 is Subgraph of G1 by GLIB_006:57;
for x being object holds x in G1.componentSet()
iff x in (G2.componentSet() \ {V1, V2}) \/ {V1 \/ V2}
proof
let x be object;
reconsider w1 = v1, w2 = v2 as Vertex of G1 by GLIB_006:68;
thus x in G1.componentSet()
implies x in (G2.componentSet() \ {V1, V2}) \/ {V1 \/ V2}
proof
assume x in G1.componentSet();
then consider w being Vertex of G1 such that
A3: x = G1.reachableFrom(w) by GLIB_002:def 8;
reconsider v = w as Vertex of G2 by GLIB_006:102;
per cases;
suppose A4: not v in G2.reachableFrom(v1) &
not v in G2.reachableFrom(v2);
then A5: G1.reachableFrom(w) = G2.reachableFrom(v) by A1, Th43;
G2.reachableFrom(v) <> V1 & G2.reachableFrom(v) <> V2 by A4, Th22;
then A6: not G1.reachableFrom(w) in {V1, V2} by A5, TARSKI:def 2;
G2.reachableFrom(v) in G2.componentSet() by GLIB_002:def 8;
then G1.reachableFrom(w) in G2.componentSet() \ {V1, V2}
by A5, A6, XBOOLE_0:def 5;
hence thesis by A3, XBOOLE_0:def 3;
end;
suppose v in G2.reachableFrom(v1);
then w in G1.reachableFrom(w1) by A2, TARSKI:def 3, GLIB_002:14;
then x = G1.reachableFrom(w1) by A3, GLIB_002:12
.= V1 \/ V2 by A1, Th42;
then x in {V1 \/ V2} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose v in G2.reachableFrom(v2);
then w in G1.reachableFrom(w2) by A2, TARSKI:def 3, GLIB_002:14;
then w in G1.reachableFrom(w1) by A1, Th41, GLIB_002:12;
then x = G1.reachableFrom(w1) by A3, GLIB_002:12
.= V1 \/ V2 by A1, Th42;
then x in {V1 \/ V2} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
assume x in (G2.componentSet() \ {V1, V2}) \/ {V1 \/ V2};
then per cases by XBOOLE_0:def 3;
suppose x in G2.componentSet() \ {V1, V2};
then A7: x in G2.componentSet() & not x in {V1, V2} by XBOOLE_0:def 5;
then A8: x <> V1 & x <> V2 by TARSKI:def 2;
consider v being Vertex of G2 such that
A9: x = G2.reachableFrom(v) by A7, GLIB_002:def 8;
reconsider w = v as Vertex of G1 by GLIB_006:68;
not v in V1 & not v in V2 by A8, A9, GLIB_002:12;
then G1.reachableFrom(w) = x by A1, A9, Th43;
hence thesis by GLIB_002:def 8;
end;
suppose x in {V1 \/ V2};
then x = V1 \/ V2 by TARSKI:def 1;
then x = G1.reachableFrom(w1) by A1, Th42;
hence thesis by GLIB_002:def 8;
end;
end;
hence thesis by TARSKI:2;
end;
Lm7:
for G2 being _Graph, v1,v2 being Vertex of G2
st not v2 in G2.reachableFrom(v1)
holds not G2.reachableFrom(v1) \/ G2.reachableFrom(v2) in G2.componentSet()
proof
let G2 be _Graph, v1,v2 be Vertex of G2;
assume A1: not v2 in G2.reachableFrom(v1);
set V1 = G2.reachableFrom(v1), V2 = G2.reachableFrom(v2);
reconsider C = G2.componentSet() as a_partition of the_Vertices_of G2
by Th23;
A2: V1 in C & V2 in C by GLIB_002:def 8;
A3: V1 misses V2 by A1, Th22;
assume V1 \/ V2 in G2.componentSet();
then per cases by A2, EQREL_1:def 4;
suppose V1 \/ V2 = V1;
then V2 c= V1 by XBOOLE_1:11;
hence contradiction by A3, XBOOLE_1:63, XBOOLE_1:66;
end;
suppose V1 \/ V2 misses V1;
then V1 misses V1 by XBOOLE_1:70;
hence contradiction;
end;
end;
:: the finite restriction is not neccessary, but all that's needed here
Lm8:
for G1 being _finite _Graph, e being set, G2 being removeEdge of G1, e
holds G1.numComponents() c= G2.numComponents()
proof
let G1 be _finite _Graph, e be set, G2 be removeEdge of G1, e;
per cases;
suppose A1: e in the_Edges_of G1;
set w1 = (the_Source_of G1).e, w2 = (the_Target_of G1).e;
reconsider w1, w2 as Vertex of G1 by A1, FUNCT_2:5;
A2: G1 is addEdge of G2,w1,e,w2 by A1, Th37;
reconsider v1 = w1, v2 = w2 as Vertex of G2 by GLIB_000:51;
reconsider G1 as addEdge of G2,v1,e,v2 by A2;
A3: the_Edges_of G2 = the_Edges_of G1 \ {e} by GLIB_000:51;
e in {e} by TARSKI:def 1;
then A4: not e in the_Edges_of G2 by A3, XBOOLE_0:def 5;
set V1 = G2.reachableFrom(v1), V2 = G2.reachableFrom(v2);
per cases;
suppose A5: not v2 in G2.reachableFrom(v1);
then not V1 \/ V2 in G2.componentSet() by Lm7;
then A6: not V1 \/ V2 in G2.componentSet() \ {V1,V2}
by XBOOLE_1:36, TARSKI:def 3;
V1 in G2.componentSet() & V2 in G2.componentSet() by GLIB_002:def 8;
then A7: {V1, V2} c= G2.componentSet() by ZFMISC_1:32;
A8: V1 <> V2 by A5, Th22;
G1.numComponents() = card G1.componentSet() by GLIB_002:def 9
.= card((G2.componentSet()\{V1,V2})\/{V1 \/ V2}) by A4, Th44
.= card(G2.componentSet()\{V1,V2}) + 1 by A6, CARD_2:41
.= card G2.componentSet() - card {V1,V2} + 1 by A7, CARD_2:44
.= card G2.componentSet() - 2 + 1 by A8, CARD_2:57
.= G2.numComponents() - 2 + 1 by GLIB_002:def 9
.= G2.numComponents() - 1;
then G2.numComponents() = G1.numComponents() +` 1;
hence thesis by CARD_2:94;
end;
suppose A9: v2 in G2.reachableFrom(v1);
G1.numComponents() = card G1.componentSet() by GLIB_002:def 9
.= card G2.componentSet() by A9, Th40
.= G2.numComponents() by GLIB_002:def 9;
hence thesis;
end;
end;
suppose not e in the_Edges_of G1;
then the_Edges_of G1 \ {e} = the_Edges_of G1 by ZFMISC_1:57
.= G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
hence thesis by GLIB_002:29, GLIB_000:94;
end;
end;
:: removing an endvertex doesn't change number of components
theorem Th45:
for G1 being _Graph, v being Vertex of G1, G2 being removeVertex of G1, v
st v is endvertex holds G1.numComponents() = G2.numComponents()
proof
let G1 be _Graph, v be Vertex of G1, G2 be removeVertex of G1, v;
assume A1: v is endvertex;
then A2: G1 is non _trivial by GLIB_000:122;
ex f being Function st f is one-to-one &
dom f = G1.componentSet() & rng f = G2.componentSet()
proof
reconsider C = G1.componentSet() as a_partition of the_Vertices_of G1
by Th23;
set V = EqClass(v,C);
set f = id C +* (V, V\{v});
take f;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume A3: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then A4: x1 in dom id C & x2 in dom id C by FUNCT_7:30;
A5: not V\{v} in C
proof
assume A6: V\{v} in C;
set w = the Element of V\{v};
w in V by A6, XBOOLE_1:36, TARSKI:def 3;
then w in V /\ (V\{v}) by A6, XBOOLE_0:def 4;
then A8: not V misses V\{v} by XBOOLE_0:def 7;
v in {v} by TARSKI:def 1;
then not v in V\{v} by XBOOLE_0:def 5;
then A9: V <> V \{v} by EQREL_1:def 6;
V in C by EQREL_1:def 6;
hence contradiction by A6, A8, A9, EQREL_1:def 4;
end;
per cases;
suppose x1 <> V & x2 <> V;
then f.x1 = (id C).x1 & f.x2 = (id C).x2 by FUNCT_7:32;
then f.x1 = x1 & f.x2 = x2 by A4, FUNCT_1:18;
hence thesis by A3;
end;
suppose x1 = V & x2 <> V;
then f.x1 = V\{v} & f.x2 = (id C).x2 by A4, FUNCT_7:31, FUNCT_7:32;
hence thesis by A5, A3, A4, FUNCT_1:18; :: by contradiction
end;
suppose x1 <> V & x2 = V;
then f.x2 = V\{v} & f.x1 = (id C).x1 by A4, FUNCT_7:31, FUNCT_7:32;
hence thesis by A5, A3, A4, FUNCT_1:18; :: by contradiction
end;
suppose x1 = V & x2 = V;
hence thesis;
end;
end;
hence f is one-to-one by FUNCT_1:def 4;
thus A10: dom f = dom id C by FUNCT_7:30
.= G1.componentSet();
for y being object holds y in rng f iff y in G2.componentSet()
proof
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A11: x in dom f & y = f.x by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
per cases;
suppose A12: x = V;
V in dom id C by EQREL_1:def 6;
then A13: y = V\{v} by A11, A12, FUNCT_7:31;
ex w being Vertex of G2 st V\{v} = G2.reachableFrom(w)
proof
consider e being object such that
A14: v.edgesInOut() = {e} & not e Joins v,v,G1
by A1, GLIB_000:def 51;
set w = v.adj(e);
A15: e in v.edgesInOut() by A14, TARSKI:def 1;
then A16: v <> w by A14, GLIB_000:67;
A17: the_Vertices_of G2 = the_Vertices_of G1 \ {v}
by A2, GLIB_000:47;
v in G1.reachableFrom(v) & e Joins v,w,G1
by A15, GLIB_000:67, GLIB_002:9;
then A18: w in G1.reachableFrom(v) by GLIB_002:10;
not w in {v} by A16, TARSKI:def 1;
then reconsider w0 = w as Vertex of G2 by A17, XBOOLE_0:def 5;
take w0;
thus V\{v} = G1.reachableFrom(v)\{v} by Th24
.= G1.reachableFrom(w)\{v} by A18, GLIB_002:12
.= G2.reachableFrom(w0) by A1, A18, Th25;
end;
hence y in G2.componentSet() by A13, GLIB_002:def 8;
end;
suppose A19: x <> V;
consider w being Vertex of G1 such that
A20: x = G1.reachableFrom(w) by A10, A11, GLIB_002:def 8;
A21: x in C & V in C by A10, A11, EQREL_1:def 6;
x misses V by A19, A21, EQREL_1:def 4;
then A22: x misses G1.reachableFrom(v) by Th24;
G1.reachableFrom(w) <> G1.reachableFrom(v) by A20, A22, XBOOLE_1:66;
then A23: not w in G1.reachableFrom(v) by GLIB_002:12;
then A24: v <> w by GLIB_002:9;
A25: the_Vertices_of G2 = the_Vertices_of G1 \ {v}
by A2, GLIB_000:47;
not w in {v} by A24, TARSKI:def 1;
then reconsider w0 = w as Vertex of G2 by A25, XBOOLE_0:def 5;
G1.reachableFrom(w) = G2.reachableFrom(w0) by A2, A23, Th26;
then A26: x in G2.componentSet() by A20, GLIB_002:def 8;
x = (id C).x by A10, A11, FUNCT_1:18
.= y by A11, A19, FUNCT_7:32;
hence y in G2.componentSet() by A26;
end;
end;
assume y in G2.componentSet();
then consider w0 being Vertex of G2 such that
A27: y = G2.reachableFrom(w0) by GLIB_002:def 8;
the_Vertices_of G2 c= the_Vertices_of G1;
then reconsider w = w0 as Vertex of G1 by TARSKI:def 3;
ex x being object st x in dom f & y = f.x
proof
per cases;
suppose A28: w in G1.reachableFrom(v);
then G2.reachableFrom(w0) = G1.reachableFrom(w) \ {v} by A1, Th25;
then y = G1.reachableFrom(v) \ {v} by A27, A28, GLIB_002:12;
then A29: y = V\{v} by Th24;
take V;
V = G1.reachableFrom(v) by Th24;
then A30: V in C by GLIB_002:def 8;
hence V in dom f by A10;
V in dom id C by A30;
hence y = f.V by A29, FUNCT_7:31;
end;
suppose A31: not w in G1.reachableFrom(v);
then A32: G2.reachableFrom(w0) = G1.reachableFrom(w) by A2, Th26;
set x = G1.reachableFrom(w);
take x;
A33: x in G1.componentSet() by GLIB_002:def 8;
hence x in dom f by A10;
x <> V
proof
assume x = V;
then x = G1.reachableFrom(v) by Th24;
hence contradiction by A31, GLIB_002:9;
end;
then f.x = (id C).x by FUNCT_7:32
.= x by A33, FUNCT_1:18;
hence y = f.x by A27, A32;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
hence rng f = G2.componentSet() by TARSKI:2;
end;
then card G1.componentSet() = card G2.componentSet()
by WELLORD2:def 4, CARD_1:5;
then G1.numComponents() = card G2.componentSet() by GLIB_002:def 9;
hence thesis by GLIB_002:def 9;
end;
registration
let G be _Graph;
cluster endvertex -> non cut-vertex for Vertex of G;
coherence
proof
let v be Vertex of G;
assume A1: v is endvertex;
set H = the removeVertex of G, v;
G.numComponents() = H.numComponents() by A1, Th45;
then not G.numComponents() in H.numComponents();
hence thesis by GLIB_002:def 10;
end;
end;
theorem
for G1 being non _trivial _finite connected _Graph
for G2 being non spanning connected Subgraph of G1
ex v being Vertex of G1 st v is non cut-vertex & not v in the_Vertices_of G2
proof
defpred P[Nat] means for G1 being non _trivial _finite connected _Graph
for G2 being non spanning connected Subgraph of G1
st G1.order() + $1 = G1.size() + 1
ex v being Vertex of G1
st v is non cut-vertex & not v in the_Vertices_of G2;
A1: P[0]
proof
let G1 be non _trivial _finite connected _Graph;
let G2 be non spanning connected Subgraph of G1;
assume G1.order() + 0 = G1.size() + 1;
then G1 is Tree-like by GLIB_002:47;
then consider v being Vertex of G1 such that
A2: v is endvertex & not v in the_Vertices_of G2 by Th31;
thus thesis by A2;
end;
A3: for k being Nat st P[k] holds P[k+1] :: remove an edge
proof
let k be Nat;
assume A4: P[k];
let G1 be non _trivial _finite connected _Graph;
let G2 be non spanning connected Subgraph of G1;
assume A5: G1.order() + (k+1) = G1.size() + 1;
G1 is non acyclic
proof
assume G1 is acyclic;
then k + 1 + (G1.size() + 1) = 0 + (G1.size() + 1) by A5, GLIB_002:46;
hence contradiction;
end;
then consider C being Walk of G1 such that
A6: C is Cycle-like by GLIB_002:def 2;
ex e being set st e in C.edges() &
(C.edges() c= the_Edges_of G2 or not e in the_Edges_of G2)
proof
per cases;
suppose A7: C.edges() c= the_Edges_of G2;
set e = the Element of C.edges();
C.edges() <> {} by A6, GLIB_001:136;
then e in C.edges();
hence thesis by A7;
end;
suppose not C.edges() c= the_Edges_of G2;
then A8: C.edges() \ the_Edges_of G2 <> {} by XBOOLE_1:37;
set e = the Element of C.edges() \ the_Edges_of G2;
e in C.edges() & not e in the_Edges_of G2 by A8, XBOOLE_0:def 5;
hence thesis;
end;
end;
then consider e being set such that
A9: e in C.edges() and
A10: C.edges() c= the_Edges_of G2 or not e in the_Edges_of G2;
set G3 = the removeEdge of G1, e;
reconsider G3 as non _trivial _Graph;
reconsider G3 as non _trivial _finite connected _Graph
by A6, A9, GLIB_002:5;
A11: the_Vertices_of G3 = the_Vertices_of G1 by GLIB_000:51;
A12: the_Edges_of G3 = the_Edges_of G1 \ {e} by GLIB_000:51;
A13: the_Edges_of G2 \ {e} c= the_Edges_of G3 by A12, XBOOLE_1:33;
set G4 = the removeEdge of G2, e;
reconsider G4 as Subgraph of G1 by GLIB_000:43;
A14: the_Vertices_of G4 = the_Vertices_of G2 &
the_Edges_of G4 = the_Edges_of G2 \ {e} by GLIB_000:51;
then reconsider G4 as Subgraph of G3 by A11, A13, GLIB_000:44;
G4 is connected
proof
per cases by A10;
suppose A15: C.edges() c= the_Edges_of G2;
reconsider C2 = C as Walk of G2 by A6, A15, GLIB_001:169;
A16: C2 is Cycle-like by A6, GLIB_006:24;
e in C2.edges() by A9, GLIB_001:110;
hence thesis by A16, GLIB_002:5;
end;
suppose not e in the_Edges_of G2;
then the_Edges_of G4 = the_Edges_of G2 by A14, ZFMISC_1:57;
hence thesis by A14, GLIB_000:86, GLIB_002:8;
end;
end;
then reconsider G4 as connected Subgraph of G3;
G4 is non spanning
proof
assume G4 is spanning;
then the_Vertices_of G2 = the_Vertices_of G1
by A11, A14, GLIB_000:def 33;
hence contradiction by GLIB_000:def 33;
end;
then reconsider G4 as non spanning connected Subgraph of G3;
G1.order() + k + 1 = G3.size() + 1 + 1 by A5, A9, GLIB_000:52;
then G3.order() + k = G3.size() + 1 by GLIB_000:52;
then consider v being Vertex of G3 such that
A17: v is non cut-vertex & not v in the_Vertices_of G4 by A4;
the_Vertices_of G3 c= the_Vertices_of G1 by GLIB_000:def 32;
then reconsider v0 = v as Vertex of G1 by TARSKI:def 3;
take v0;
now
let H1 be removeVertex of G1, v0;
set H2 = the removeVertex of G3, v;
A18: H2.numComponents() c= G3.numComponents() by A17, GLIB_002:35;
H2 is removeEdge of H1, e by GLIB_000:124;
then A19: H1.numComponents() c= H2.numComponents() by Lm8;
G1.numComponents() = 1 & G3.numComponents() = 1 by GLIB_002:28;
hence H1.numComponents() c= G1.numComponents() by A18, A19, XBOOLE_1:1;
end;
hence v0 is non cut-vertex by GLIB_002:35;
thus not v0 in the_Vertices_of G2 by A14, A17;
end;
A20: for k being Nat holds P[k] from NAT_1:sch 2(A1,A3);
let G1 be non _trivial _finite connected _Graph;
let G2 be non spanning connected Subgraph of G1;
ex k being Nat st
G1.order() + k = G1.size() + 1 by GLIB_002:40, NAT_1:10;
hence thesis by A20;
end;
:: improved in GLIB_007:61
:: not e in the_Edges_of G3 can then be followed by GLIB_006:def 9
Lm9:
for G3 being _Graph, v being object, V being set, v1 being Vertex of G3
for G1 being addAdjVertexAll of G3,v,V \/ {v1}
st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V
ex G2 being addAdjVertexAll of G3,v,V, e being object
st not e in the_Edges_of G2 &
(G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v)
by GLIB_007:61;
:: into GLIB_007 ?
theorem Th47:
for G1 being non _trivial simple _Graph, v being Vertex of G1
for G2 being removeVertex of G1, v
holds G1 is addAdjVertexAll of G2, v, v.allNeighbors()
proof
let G1 be non _trivial simple _Graph, v be Vertex of G1;
let G2 be removeVertex of G1, v;
A1: G1 is Supergraph of G2 by GLIB_006:57;
A2: the_Vertices_of G2 = the_Vertices_of G1 \ {v} by GLIB_000:47;
A3: the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ {v})
by GLIB_000:47
.= G1.edgesBetween(the_Vertices_of G1) \ v.edgesInOut() by GLIB_000:107
.= the_Edges_of G1 \ v.edgesInOut() by GLIB_000:34;
v in {v} by TARSKI:def 1;
then A4: not v in the_Vertices_of G2 by A2, XBOOLE_0:def 5;
for x being object holds
x in v.allNeighbors() implies x in the_Vertices_of G2
proof
let x be object;
assume A5: x in v.allNeighbors();
x <> v
proof
assume x = v;
then consider e being object such that
A6: e Joins v,v,G1 by A5, GLIB_000:71;
thus contradiction by A6, GLIB_000:18;
end;
then not x in {v} by TARSKI:def 1;
hence thesis by A2, A5, XBOOLE_0:def 5;
end;
then A7: v.allNeighbors() c= the_Vertices_of G2 by TARSKI:def 3;
:: show the properties of addAdjVertexAll
now
thus the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A2, ZFMISC_1:116;
hereby
let e be object;
thus not e Joins v,v,G1 by GLIB_000:18;
let v1 be object;
hereby
assume A8: not v1 in v.allNeighbors();
v1 is set by TARSKI:1;
hence not e Joins v1,v,G1 by A8, GLIB_000:71, GLIB_000:14;
end;
let v2 be object;
assume A9: v1 <> v & v2 <> v & e DJoins v1,v2,G1;
thus e DJoins v1,v2,G2
proof
assume not e DJoins v1,v2,G2;
then A10: not e in the_Edges_of G2 by A1, A9, GLIB_006:71;
e in the_Edges_of G1 by A9, GLIB_000:def 14;
then e in v.edgesInOut() by A3, A10, XBOOLE_0:def 5;
then per cases by GLIB_000:61;
suppose (the_Source_of G1).e = v;
hence contradiction by A9, GLIB_000:def 14;
end;
suppose (the_Target_of G1).e = v;
hence contradiction by A9, GLIB_000:def 14;
end;
end;
end;
reconsider E = v.edgesInOut() as set;
take E;
card E = v.degree() by GLIB_000:19;
hence card v.allNeighbors() = card E by GLIB_000:111;
E /\ the_Edges_of G2 = {}
proof
assume E /\ the_Edges_of G2 <> {};
then consider e being object such that
A11: e in E /\ the_Edges_of G2 by XBOOLE_0:def 1;
A12: e in E & e in the_Edges_of G2 by A11, XBOOLE_0:def 4;
then (the_Source_of G1).e = v or (the_Target_of G1).e = v by GLIB_000:61;
then (the_Source_of G2).e = v or (the_Target_of G2).e = v
by A12, GLIB_000:def 32;
then (the_Source_of G2).e in {v} or (the_Target_of G2).e in {v}
by TARSKI:def 1;
then not (the_Source_of G2).e in the_Vertices_of G2 or
not (the_Target_of G2).e in the_Vertices_of G2 by A2, XBOOLE_0:def 5;
hence contradiction by A12, FUNCT_2:5;
end;
hence E misses the_Edges_of G2 by XBOOLE_0:def 7;
A13: the_Edges_of G2 \/ E c= the_Edges_of G1 by XBOOLE_1:8;
for e being object holds
e in the_Edges_of G1 implies e in the_Edges_of G2 \/ E
proof
let e be object;
assume A14: e in the_Edges_of G1;
e in the_Edges_of G2 or e in E by A3, A14, XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
then the_Edges_of G1 c= the_Edges_of G2 \/ E by TARSKI:def 3;
hence the_Edges_of G1 = the_Edges_of G2 \/ E by A13, XBOOLE_0:def 10;
let v1 be object;
assume A15: v1 in v.allNeighbors();
then consider e1 being object such that
A16: e1 Joins v,v1,G1 by GLIB_000:71;
take e1;
v1 in the_Vertices_of G1 & e1 is set by A15, TARSKI:1;
hence e1 in E by A16, GLIB_000:64;
thus A17: e1 Joins v1,v,G1 by A16, GLIB_000:14;
let e2 be object;
assume e2 Joins v1,v,G1;
hence e1 = e2 by A17, GLIB_000:def 20;
end;
hence thesis by A1, A4, A7, GLIB_007:def 4;
end;
begin :: Edgeless and non edgeless graphs
definition
let G be _Graph;
attr G is edgeless means :Def1:
the_Edges_of G = {};
end;
theorem
for G being _Graph holds G is edgeless iff card the_Edges_of G = 0;
theorem Th49:
for G being _Graph holds G is edgeless iff G.size() = 0
proof
let G be _Graph;
hereby
assume G is edgeless;
then card the_Edges_of G = 0;
hence G.size() = 0 by GLIB_000:def 25;
end;
assume G.size() = 0;
then card the_Edges_of G = 0 by GLIB_000:def 25;
hence thesis;
end;
registration
let G be _Graph;
cluster -> edgeless for removeEdges of G, the_Edges_of G;
coherence
proof
let G2 be removeEdges of G, the_Edges_of G;
the_Edges_of G2 = the_Edges_of G \ the_Edges_of G by GLIB_000:53
.= {} by XBOOLE_1:37;
hence thesis;
end;
end;
registration
cluster edgeless for _Graph;
existence
proof
take the removeEdges of the _Graph, the_Edges_of the _Graph;
thus thesis;
end;
let G be _Graph;
cluster edgeless spanning for Subgraph of G;
existence
proof
take the removeEdges of G, the_Edges_of G;
thus thesis;
end;
cluster edgeless _trivial for Subgraph of G;
existence
proof
set G2 = the inducedSubgraph of G, {the Vertex of G};
reconsider G3 = the removeEdges of G2, the_Edges_of G2
as Subgraph of G by GLIB_000:43;
take G3;
thus thesis;
end;
end;
registration
let G be edgeless _Graph;
cluster the_Edges_of G -> empty;
coherence by Def1;
end;
registration
cluster edgeless -> non-multi non-Dmulti loopless simple Dsimple for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is edgeless;
then for e1,e2,v1,v2 being object
holds e1 Joins v1,v2,G & e2 Joins v1,v2,G implies e1 = e2
by GLIB_000:def 13;
hence A2: G is non-multi by GLIB_000:def 20;
for e1,e2,v1,v2 being object
holds e1 DJoins v1,v2,G & e2 DJoins v1,v2,G implies e1 = e2
by A1, GLIB_000:def 14;
hence G is non-Dmulti by GLIB_000:def 21;
not ex e being object st e in the_Edges_of G &
(the_Source_of G).e = (the_Target_of G).e by A1;
hence G is loopless by GLIB_000:def 18;
hence thesis by A2;
end;
cluster _trivial loopless -> edgeless for _Graph;
coherence by GLIB_000:23;
let V be non empty set, S,T be Function of {},V;
cluster createGraph(V,{},S,T) -> edgeless;
coherence;
end;
theorem
for G being edgeless_Graph, e,v1,v2 being object
holds not e Joins v1,v2,G & not e DJoins v1,v2,G
proof
let G be edgeless _Graph;
let e,v1,v2 be object;
not e Joins v1,v2,G
proof
assume e Joins v1,v2,G;
then e in the_Edges_of G by GLIB_000:def 13;
hence contradiction;
end;
hence thesis by GLIB_000:16;
end;
theorem
for G being edgeless_Graph, e being object, X, Y being set
holds not e SJoins X,Y,G & not e DSJoins X,Y,G
proof
let G be edgeless _Graph;
let e be object, X, Y be set;
thus not e SJoins X,Y,G
proof
assume e SJoins X,Y,G;
then e in the_Edges_of G by GLIB_000:def 15;
hence contradiction;
end;
thus not e DSJoins X,Y,G
proof
assume e DSJoins X,Y,G;
then e in the_Edges_of G by GLIB_000:def 16;
hence contradiction;
end;
end;
theorem Th52:
for G1, G2 being _Graph st G1 == G2
holds G1 is edgeless implies G2 is edgeless by GLIB_000:def 34;
registration
let G be edgeless _Graph;
cluster -> trivial for Walk of G;
coherence
proof
let W be Walk of G;
W.edges() = {};
hence thesis by GLIB_001:136;
end;
cluster -> edgeless for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
the_Edges_of G2 c= the_Edges_of G;
hence thesis;
end;
let X be set;
cluster G.edgesInto(X) -> empty;
coherence;
cluster G.edgesOutOf(X) -> empty;
coherence;
cluster G.edgesInOut(X) -> empty;
coherence;
cluster G.edgesBetween(X) -> empty;
coherence;
cluster G.set(WeightSelector, X) -> edgeless;
coherence by GLIB_003:7, Th52;
cluster G.set(ELabelSelector, X) -> edgeless;
coherence by GLIB_003:7, Th52;
cluster G.set(VLabelSelector, X) -> edgeless;
coherence by GLIB_003:7, Th52;
cluster -> edgeless for addVertices of G, X;
coherence
proof
let G1 be addVertices of G, X;
the_Edges_of G1 = the_Edges_of G by GLIB_006:def 10;
hence thesis;
end;
cluster -> edgeless for reverseEdgeDirections of G, X;
coherence
proof
let G1 be reverseEdgeDirections of G, X;
per cases;
suppose X c= the_Edges_of G;
hence thesis by GLIB_007:def 1;
end;
suppose not X c= the_Edges_of G;
then G1 == G by GLIB_007:def 1;
then the_Edges_of G1 = the_Edges_of G by GLIB_000:def 34;
hence thesis;
end;
end;
let Y be set;
cluster G.edgesBetween(X,Y) -> empty;
coherence;
cluster G.edgesDBetween(X,Y) -> empty;
coherence;
end;
registration
cluster edgeless -> acyclic chordal for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is edgeless;
then not ex W being Walk of G st W is Cycle-like;
hence G is acyclic by GLIB_002:def 2;
for W being Walk of G st W.length()>3 & W is Cycle-like holds W is chordal
by A1;
hence thesis by CHORD:def 11;
end;
cluster _trivial edgeless -> Tree-like for _Graph;
coherence;
cluster non _trivial edgeless -> non connected non Tree-like non complete
for _Graph;
coherence
proof
let G be _Graph;
assume A2: G is non _trivial edgeless;
then consider v1, v2 being Vertex of G such that
A3: v1 <> v2 by GLIB_000:21;
not ex W being Walk of G st W is_Walk_from v1, v2
proof
given W being Walk of G such that
A4: W is_Walk_from v1,v2;
W.first() = v1 & W.last() = v2 by A4, GLIB_001:def 23;
hence contradiction by A2, A3, GLIB_001:127;
end;
hence thesis by GLIB_002:def 1;
end;
cluster connected edgeless -> _trivial for _Graph;
coherence;
end;
theorem
for G1 being edgeless _Graph, G2 being Subgraph of G1
holds G1 is addVertices of G2, the_Vertices_of G1 \ the_Vertices_of G2
proof
let G1 be edgeless _Graph, G2 be Subgraph of G1;
A1: the_Edges_of G1 = the_Edges_of G2;
G1 is Supergraph of G2 by GLIB_006:57;
hence thesis by A1, Th33;
end;
theorem Th54:
for G2 being _Graph, v1, v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2
holds G1 is non edgeless
proof
let G2 be _Graph, v1, v2 be Vertex of G2, e be object;
let G1 be addEdge of G2, v1, e, v2;
assume not e in the_Edges_of G2;
then the_Edges_of G1 = the_Edges_of G2 \/ {e} by GLIB_006:def 11;
hence thesis;
end;
theorem Th55:
for G2 being _Graph, v1 being Vertex of G2, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2
holds G1 is non edgeless
proof
let G2 be _Graph, v1 be Vertex of G2, e, v2 be object;
let G1 be addAdjVertex of G2, v1, e, v2;
assume not v2 in the_Vertices_of G2 & not e in the_Edges_of G2;
then the_Edges_of G1 = the_Edges_of G2 \/ {e} by GLIB_006:def 13;
hence thesis;
end;
theorem Th56:
for G2 being _Graph, v1, e being object, v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2
holds G1 is non edgeless
proof
let G2 be _Graph, v1, e be object, v2 be Vertex of G2;
let G1 be addAdjVertex of G2, v1, e, v2;
assume not v1 in the_Vertices_of G2 & not e in the_Edges_of G2;
then the_Edges_of G1 = the_Edges_of G2 \/ {e} by GLIB_006:def 14;
hence thesis;
end;
theorem Th57:
for G2 being _Graph, v being object
for V being non empty Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2
holds G1 is non edgeless by GLIB_007:47;
registration
let G be _Graph;
cluster -> non edgeless for addAdjVertexToAll of G, the_Vertices_of G;
coherence
proof
the_Vertices_of G is non empty & the_Vertices_of G c= the_Vertices_of G;
then A1: not the_Vertices_of G in the_Vertices_of G &
the_Vertices_of G is non empty Subset of the_Vertices_of G;
let G1 be addAdjVertexToAll of G, the_Vertices_of G;
G1 is addAdjVertexToAll of G, the_Vertices_of G, the_Vertices_of G;
hence thesis by A1, Th57;
end;
cluster -> non edgeless for addAdjVertexFromAll of G, the_Vertices_of G;
coherence
proof
the_Vertices_of G is non empty & the_Vertices_of G c= the_Vertices_of G;
then A2: not the_Vertices_of G in the_Vertices_of G &
the_Vertices_of G is non empty Subset of the_Vertices_of G;
let G1 be addAdjVertexFromAll of G, the_Vertices_of G;
G1 is addAdjVertexFromAll of G, the_Vertices_of G, the_Vertices_of G;
hence thesis by A2, Th57;
end;
cluster -> non edgeless for addAdjVertexAll of G, the_Vertices_of G;
coherence
proof
the_Vertices_of G is non empty & the_Vertices_of G c= the_Vertices_of G;
then not the_Vertices_of G in the_Vertices_of G &
the_Vertices_of G is non empty Subset of the_Vertices_of G;
hence thesis by Th57;
end;
let v be Vertex of G;
cluster -> non edgeless for
addAdjVertex of G, v, the_Edges_of G, the_Vertices_of G;
coherence
proof
not the_Vertices_of G in the_Vertices_of G &
not the_Edges_of G in the_Edges_of G;
hence thesis by Th55;
end;
cluster -> non edgeless for
addAdjVertex of G, the_Vertices_of G, the_Edges_of G, v;
coherence
proof
not the_Vertices_of G in the_Vertices_of G &
not the_Edges_of G in the_Edges_of G;
hence thesis by Th56;
end;
let w be Vertex of G;
cluster -> non edgeless for addEdge of G, v, the_Edges_of G, w;
coherence
proof
not the_Edges_of G in the_Edges_of G;
hence thesis by Th54;
end;
end;
registration
let G be edgeless _Graph;
cluster -> _trivial for Component of G;
coherence;
let v be Vertex of G;
cluster v.edgesIn() -> empty;
coherence;
cluster v.edgesOut() -> empty;
coherence;
cluster v.edgesInOut() -> empty;
coherence;
end;
registration
let G be edgeless _Graph;
cluster -> isolated non cut-vertex non endvertex for Vertex of G;
coherence
proof
let v be Vertex of G;
v.edgesInOut() = {};
hence v is isolated by GLIB_000:def 49;
hence v is non cut-vertex;
thus v is non endvertex
proof
assume v is endvertex;
then consider e being object such that
A1: v.edgesInOut() = {e} & not e Joins v,v,G by GLIB_000:def 51;
thus contradiction by A1;
end;
end;
let v be Vertex of G;
cluster v.inDegree() -> empty;
coherence
proof
v.edgesIn() = {};
hence thesis by GLIB_000:def 42, CARD_1:27;
end;
cluster v.outDegree() -> empty;
coherence
proof
v.edgesOut() = {};
hence thesis by GLIB_000:def 43, CARD_1:27;
end;
cluster v.inNeighbors() -> empty;
coherence
proof
(the_Source_of G).:(v.edgesIn()) = {};
hence thesis by GLIB_000:def 46;
end;
cluster v.outNeighbors() -> empty;
coherence
proof
(the_Target_of G).:(v.edgesOut()) = {};
hence thesis by GLIB_000:def 47;
end;
end;
registration
let G be edgeless _Graph, v be Vertex of G;
cluster v.degree() -> empty;
coherence
proof
v.inDegree() +` v.outDegree() = 0 + 0;
hence thesis by GLIB_000:def 44;
end;
cluster v.allNeighbors() -> empty;
coherence
proof
v.inNeighbors() \/ v.outNeighbors() = {};
hence thesis by GLIB_000:def 48;
end;
end;
registration
cluster _trivial _finite edgeless for _Graph;
existence
proof
set G = the _trivial _finite _Graph;
take the removeEdges of G, the_Edges_of G;
thus thesis;
end;
cluster non _trivial _finite edgeless for _Graph;
existence
proof
set G = the non _trivial _finite _Graph;
take the removeEdges of G, the_Edges_of G;
thus thesis;
end;
cluster _trivial _finite non edgeless for _Graph;
existence
proof
set G = the _trivial _finite _Graph;
set v = the Vertex of G;
take the addEdge of G, v, the_Edges_of G, v;
thus thesis;
end;
cluster non _trivial _finite non edgeless for _Graph;
existence
proof
set G = the non _trivial _finite _Graph;
set v = the Vertex of G;
take the addEdge of G, v, the_Edges_of G, v;
thus thesis;
end;
end;
registration
let G be non edgeless _Graph;
cluster the_Edges_of G -> non empty;
coherence by Def1;
cluster -> non edgeless for Supergraph of G;
coherence
proof
let G1 be Supergraph of G;
assume A1: G1 is edgeless;
G is Subgraph of G1 by GLIB_006:57;
hence contradiction by A1;
end;
let X be set;
cluster -> non edgeless for reverseEdgeDirections of G, X;
coherence
proof
let G1 be reverseEdgeDirections of G, X;
per cases;
suppose X c= the_Edges_of G;
hence thesis by GLIB_007:def 1;
end;
suppose not X c= the_Edges_of G;
then G1 == G by GLIB_007:def 1;
then the_Edges_of G1 = the_Edges_of G by GLIB_000:def 34;
hence thesis;
end;
end;
cluster G.set(WeightSelector, X) -> non edgeless;
coherence
proof
G.set(WeightSelector, X) == G by GLIB_003:7;
hence thesis by Th52;
end;
cluster G.set(ELabelSelector, X) -> non edgeless;
coherence
proof
G.set(ELabelSelector, X) == G by GLIB_003:7;
hence thesis by Th52;
end;
cluster G.set(VLabelSelector, X) -> non edgeless;
coherence
proof
G.set(VLabelSelector, X) == G by GLIB_003:7;
hence thesis by Th52;
end;
end;
definition
let G be non edgeless _Graph;
mode Edge of G is Element of the_Edges_of G;
end;
theorem
for G1 being _finite edgeless _Graph, G2 being Subgraph of G1
st G1.order() = G2.order() holds G1 == G2
proof
let G1 be _finite edgeless _Graph, G2 be Subgraph of G1;
assume A1: G1.order() = G2.order();
A2: card the_Vertices_of G1 = G1.order() by GLIB_000:def 24
.= card the_Vertices_of G2 by A1, GLIB_000:def 24;
A3: the_Vertices_of G2 = the_Vertices_of G1 by A2, CARD_2:102;
A4: the_Edges_of G1 = the_Edges_of G2;
G1 is Subgraph of G1 by GLIB_000:40;
hence thesis by A3, A4, GLIB_000:86;
end;
definition
let GF be Graph-yielding Function;
attr GF is edgeless means :Def2:
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is edgeless;
end;
definition
let GF be non empty Graph-yielding Function;
redefine attr GF is edgeless means :: redefines edgeless (GLIB_008, definition)
:Def3:
for x being Element of dom GF holds GF.x is edgeless;
compatibility
proof
hereby
assume A1: GF is edgeless;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is edgeless by A1;
thus GF.x is edgeless by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is edgeless;
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;
Lm10: :: copied from GLIB_000
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 GSq be GraphSeq;
redefine attr GSq is edgeless means :Def4: :: redefines edgeless (GLIB_008, redefinition) → edgeless (GLIB_008, definition)
for n being Nat holds GSq.n is edgeless;
compatibility
proof
hereby
assume A1: GSq is edgeless;
let x be Nat;
x in dom GSq by Lm10;
hence GSq.x is edgeless by A1;
end;
assume A2: for x being Nat holds GSq.x is edgeless;
let x be Element of dom GSq;
thus thesis by A2;
end;
end;
registration
cluster _trivial loopless -> edgeless for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
assume A1: GF is _trivial loopless;
let x be object;
assume A2: x in dom GF;
consider G1 being _Graph such that
A3: GF.x = G1 & G1 is _trivial by A1, A2, GLIB_000:def 60;
consider G2 being _Graph such that
A4: GF.x = G2 & G2 is loopless by A1, A2, GLIB_000:def 59;
take G1;
thus thesis by A3, A4;
end;
cluster edgeless -> non-multi non-Dmulti loopless simple Dsimple acyclic
for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
assume A5: GF is edgeless;
now
let x be object;
assume x in dom GF;
then consider G being _Graph such that
A6: GF.x = G & G is edgeless by A5;
take G;
thus GF.x = G by A6;
thus G is non-multi by A6;
end;
hence GF is non-multi by GLIB_000:def 62;
now
let x be object;
assume x in dom GF;
then consider G being _Graph such that
A7: GF.x = G & G is edgeless by A5;
take G;
thus GF.x = G by A7;
thus G is non-Dmulti by A7;
end;
hence GF is non-Dmulti by GLIB_000:def 63;
now
let x be object;
assume x in dom GF;
then consider G being _Graph such that
A8: GF.x = G & G is edgeless by A5;
take G;
thus GF.x = G by A8;
thus G is loopless by A8;
end;
hence GF is loopless by GLIB_000:def 59;
now
let x be object;
assume x in dom GF;
then consider G being _Graph such that
A9: GF.x = G & G is edgeless by A5;
take G;
thus GF.x = G by A9;
thus G is simple by A9;
end;
hence GF is simple by GLIB_000:def 64;
now
let x be object;
assume x in dom GF;
then consider G being _Graph such that
A10: GF.x = G & G is edgeless by A5;
take G;
thus GF.x = G by A10;
thus G is Dsimple by A10;
end;
hence GF is Dsimple by GLIB_000:def 65;
now
let x be object;
assume x in dom GF;
then consider G being _Graph such that
A11: GF.x = G & G is edgeless by A5;
take G;
thus GF.x = G by A11;
thus G is acyclic by A11;
end;
hence GF is acyclic by GLIB_002:def 13;
end;
end;
registration
let GF be edgeless non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> edgeless;
coherence by Def3;
end;
registration
let GSq be edgeless GraphSeq, x be Nat;
cluster GSq.x -> edgeless;
coherence by Def4;
end;
begin :: Finite Graph sequences
registration
let G be _Graph;
cluster <* G *> -> Graph-yielding;
coherence
proof
let x be object;
assume x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is _Graph;
end;
end;
registration
let G be _finite _Graph;
cluster <* G *> -> _finite;
coherence
proof
let x be Element of dom <* G *>;
x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is _finite;
end;
end;
registration
let G be loopless _Graph;
cluster <* G *> -> loopless;
coherence
proof
let x be Element of dom <* G *>;
x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is loopless;
end;
end;
registration
let G be _trivial _Graph;
cluster <* G *> -> _trivial;
coherence
proof
let x be Element of dom <* G *>;
x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is _trivial;
end;
end;
registration
let G be non _trivial _Graph;
cluster <* G *> -> non-trivial;
coherence
proof
let x be Element of dom <* G *>;
x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is non _trivial;
end;
end;
registration
let G be non-multi _Graph;
cluster <* G *> -> non-multi;
coherence
proof
let x be Element of dom <* G *>;
x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is non-multi;
end;
end;
registration
let G be non-Dmulti _Graph;
cluster <* G *> -> non-Dmulti;
coherence
proof
let x be Element of dom <* G *>;
x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is non-Dmulti;
end;
end;
registration
let G be simple _Graph;
cluster <* G *> -> simple;
coherence;
end;
registration
let G be Dsimple _Graph;
cluster <* G *> -> Dsimple;
coherence;
end;
registration
let G be connected _Graph;
cluster <* G *> -> connected;
coherence
proof
let x be Element of dom <* G *>;
x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is connected;
end;
end;
registration
let G be acyclic _Graph;
cluster <* G *> -> acyclic;
coherence
proof
let x be Element of dom <* G *>;
x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is acyclic;
end;
end;
registration
let G be Tree-like _Graph;
cluster <* G *> -> Tree-like;
coherence;
end;
registration
let G be edgeless _Graph;
cluster <* G *> -> edgeless;
coherence
proof
let x be Element of dom <* G *>;
x in dom <* G *>;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <* G *>.x is edgeless;
end;
end;
registration
cluster empty Graph-yielding for FinSequence;
existence
proof
take the empty FinSequence;
thus thesis;
end;
cluster non empty Graph-yielding for FinSequence;
existence
proof
take <* the _Graph *>;
thus thesis;
end;
end;
registration
let p be non empty Graph-yielding FinSequence;
cluster p.1 -> Function-like Relation-like;
coherence
proof
1 in dom p by FINSEQ_5:6;
hence thesis;
end;
cluster p.len p -> Function-like Relation-like;
coherence
proof
len p in dom p by FINSEQ_5:6;
hence thesis;
end;
end;
registration
let p be non empty Graph-yielding FinSequence;
cluster p.1 -> finite NAT-defined;
coherence
proof
1 in dom p by FINSEQ_5:6;
hence thesis;
end;
cluster p.len p -> finite NAT-defined;
coherence
proof
len p in dom p by FINSEQ_5:6;
hence thesis;
end;
end;
registration
let p be non empty Graph-yielding FinSequence;
cluster p.1 -> [Graph-like];
coherence
proof
1 in dom p by FINSEQ_5:6;
hence thesis;
end;
cluster p.len p -> [Graph-like];
coherence
proof
len p in dom p by FINSEQ_5:6;
hence thesis;
end;
end;
registration
cluster non empty _finite loopless _trivial non-multi non-Dmulti simple
Dsimple
connected acyclic Tree-like edgeless for Graph-yielding FinSequence;
existence
proof
take <* the _finite _trivial edgeless _Graph *>;
thus thesis;
end;
cluster non empty _finite loopless non-trivial non-multi non-Dmulti simple
Dsimple connected acyclic Tree-like for Graph-yielding FinSequence;
existence
proof
take <* the _finite non _trivial Tree-like _Graph *>;
thus thesis;
end;
end;
registration
let p be Graph-yielding FinSequence, n be Nat;
cluster p | n -> Graph-yielding;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then p.x is _Graph by GLIB_000:def 53;
hence (p|n).x is _Graph by A1, A2, FUNCT_1:47;
end;
hence thesis by GLIB_000:def 53;
end;
cluster p /^ n -> Graph-yielding;
coherence
proof
per cases;
suppose A3: n <= len p;
now
let x be object;
assume A4: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A4, FINSEQ_5:26;
then p.(n+i) is _Graph by GLIB_000:def 53;
hence (p /^ n).x is _Graph by A3, A4, RFINSEQ:def 1;
end;
hence thesis by GLIB_000:def 53;
end;
suppose not n <= len p;
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> Graph-yielding;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> Graph-yielding;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p be _finite Graph-yielding FinSequence, n be Nat;
cluster p | n -> _finite;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is _finite by GLIB_000:def 58;
take G;
thus (p|n).x = G & G is _finite by A1, A3, A2, FUNCT_1:47;
end;
hence thesis by GLIB_000:def 58;
end;
cluster p /^ n -> _finite;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is _finite by GLIB_000:def 58;
take G;
thus (p /^ n).x = G & G is _finite by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis by GLIB_000:def 58;
end;
suppose not n <= len p;
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> _finite;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> _finite;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p be loopless Graph-yielding FinSequence, n be Nat;
cluster p | n -> loopless;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is loopless by GLIB_000:def 59;
take G;
thus (p|n).x = G & G is loopless by A1, A3, A2, FUNCT_1:47;
end;
hence thesis by GLIB_000:def 59;
end;
cluster p /^ n -> loopless;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is loopless by GLIB_000:def 59;
take G;
thus (p /^ n).x = G & G is loopless by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis by GLIB_000:def 59;
end;
suppose not n <= len p;
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> loopless;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> loopless;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p be _trivial Graph-yielding FinSequence, n be Nat;
cluster p | n -> _trivial;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is _trivial by GLIB_000:def 60;
take G;
thus (p|n).x = G & G is _trivial by A1, A3, A2, FUNCT_1:47;
end;
hence thesis by GLIB_000:def 60;
end;
cluster p /^ n -> _trivial;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is _trivial by GLIB_000:def 60;
take G;
thus (p /^ n).x = G & G is _trivial by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis by GLIB_000:def 60;
end;
suppose not n <= len p;
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> _trivial;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> _trivial;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p be non-trivial Graph-yielding FinSequence, n be Nat;
cluster p | n -> non-trivial;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is non _trivial by GLIB_000:def 61;
take G;
thus (p|n).x = G & G is non _trivial by A1, A3, A2, FUNCT_1:47;
end;
hence thesis by GLIB_000:def 61;
end;
cluster p /^ n -> non-trivial;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is non _trivial by GLIB_000:def 61;
take G;
thus (p /^ n).x = G & G is non _trivial by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis by GLIB_000:def 61;
end;
suppose not n <= len p;
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> non-trivial;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> non-trivial;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p be non-multi Graph-yielding FinSequence, n be Nat;
cluster p | n -> non-multi;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is non-multi by GLIB_000:def 62;
take G;
thus (p|n).x = G & G is non-multi by A1, A3, A2, FUNCT_1:47;
end;
hence thesis by GLIB_000:def 62;
end;
cluster p /^ n -> non-multi;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is non-multi by GLIB_000:def 62;
take G;
thus (p /^ n).x = G & G is non-multi by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis by GLIB_000:def 62;
end;
suppose not n <= len p;
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> non-multi;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> non-multi;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p be non-Dmulti Graph-yielding FinSequence, n be Nat;
cluster p | n -> non-Dmulti;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is non-Dmulti by GLIB_000:def 63;
take G;
thus (p|n).x = G & G is non-Dmulti by A1, A3, A2, FUNCT_1:47;
end;
hence thesis by GLIB_000:def 63;
end;
cluster p /^ n -> non-Dmulti;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is non-Dmulti by GLIB_000:def 63;
take G;
thus (p /^ n).x = G & G is non-Dmulti by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis by GLIB_000:def 63;
end;
suppose not n <= len p;
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> non-Dmulti;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> non-Dmulti;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p be simple Graph-yielding FinSequence, n be Nat;
cluster p | n -> simple;
coherence;
cluster p /^ n -> simple;
coherence;
let m be Nat;
cluster smid(p,m,n) -> simple;
coherence;
cluster (m,n)-cut p -> simple;
coherence;
end;
registration
let p be Dsimple Graph-yielding FinSequence, n be Nat;
cluster p | n -> Dsimple;
coherence;
cluster p /^ n -> Dsimple;
coherence;
let m be Nat;
cluster smid(p,m,n) -> Dsimple;
coherence;
cluster (m,n)-cut p -> Dsimple;
coherence;
end;
registration
let p be connected Graph-yielding FinSequence, n be Nat;
cluster p | n -> connected;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is connected by GLIB_002:def 12;
take G;
thus (p|n).x = G & G is connected by A1, A3, A2, FUNCT_1:47;
end;
hence thesis by GLIB_002:def 12;
end;
cluster p /^ n -> connected;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is connected by GLIB_002:def 12;
take G;
thus (p /^ n).x = G & G is connected by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis by GLIB_002:def 12;
end;
suppose not n <= len p;
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> connected;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> connected;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p be acyclic Graph-yielding FinSequence, n be Nat;
cluster p | n -> acyclic;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is acyclic by GLIB_002:def 13;
take G;
thus (p|n).x = G & G is acyclic by A1, A3, A2, FUNCT_1:47;
end;
hence thesis by GLIB_002:def 13;
end;
cluster p /^ n -> acyclic;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is acyclic by GLIB_002:def 13;
take G;
thus (p /^ n).x = G & G is acyclic by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis by GLIB_002:def 13;
end;
suppose not (n <= len p);
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> acyclic;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> acyclic;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p be Tree-like Graph-yielding FinSequence, n be Nat;
cluster p | n -> Tree-like;
coherence;
cluster p /^ n -> Tree-like;
coherence;
let m be Nat;
cluster smid(p,m,n) -> Tree-like;
coherence;
cluster (m,n)-cut p -> Tree-like;
coherence;
end;
registration
let p be edgeless Graph-yielding FinSequence, n be Nat;
cluster p | n -> edgeless;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is edgeless by Def2;
take G;
thus (p|n).x = G & G is edgeless by A1, A3, A2, FUNCT_1:47;
end;
hence thesis;
end;
cluster p /^ n -> edgeless;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is edgeless by Def2;
take G;
thus (p /^ n).x = G & G is edgeless by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis;
end;
suppose not (n <= len p);
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> edgeless;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> edgeless;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p, q be Graph-yielding FinSequence;
cluster p ^ q -> Graph-yielding;
coherence
proof
now
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & p.k is _Graph by FINSEQ_1:def 7, GLIB_000:def 53;
hence (p^q).x is _Graph;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & q.n is _Graph
by A2, FINSEQ_1:def 7, GLIB_000:def 53;
hence (p^q).x is _Graph by A2;
end;
end;
hence thesis by GLIB_000:def 53;
end;
cluster p ^' q -> Graph-yielding;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let p, q be _finite Graph-yielding FinSequence;
cluster p ^ q -> _finite;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is _finite
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is _finite
by FINSEQ_1:def 7, GLIB_000:def 58;
hence ex G being _Graph st (p^q).x = G & G is _finite;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G & G is _finite
by A2, FINSEQ_1:def 7, GLIB_000:def 58;
hence ex G being _Graph st (p^q).x = G & G is _finite by A2;
end;
end;
hence thesis by GLIB_000:def 58;
end;
cluster p ^' q -> _finite;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let p, q be loopless Graph-yielding FinSequence;
cluster p ^ q -> loopless;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is loopless
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is loopless
by FINSEQ_1:def 7, GLIB_000:def 59;
hence ex G being _Graph st (p^q).x = G & G is loopless;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G & G is loopless
by A2, FINSEQ_1:def 7, GLIB_000:def 59;
hence ex G being _Graph st (p^q).x = G & G is loopless by A2;
end;
end;
hence thesis by GLIB_000:def 59;
end;
cluster p ^' q -> loopless;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let p, q be _trivial Graph-yielding FinSequence;
cluster p ^ q -> _trivial;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is _trivial
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is _trivial
by FINSEQ_1:def 7, GLIB_000:def 60;
hence ex G being _Graph st (p^q).x = G & G is _trivial;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G & G is _trivial
by A2, FINSEQ_1:def 7, GLIB_000:def 60;
hence ex G being _Graph st (p^q).x = G & G is _trivial by A2;
end;
end;
hence thesis by GLIB_000:def 60;
end;
cluster p ^' q -> _trivial;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let p, q be non-trivial Graph-yielding FinSequence;
cluster p ^ q -> non-trivial;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is non _trivial
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is non _trivial
by FINSEQ_1:def 7, GLIB_000:def 61;
hence ex G being _Graph st (p^q).x = G & G is non _trivial;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G &
G is non _trivial by A2, FINSEQ_1:def 7, GLIB_000:def 61;
hence ex G being _Graph st (p^q).x = G & G is non _trivial by A2;
end;
end;
hence thesis by GLIB_000:def 61;
end;
cluster p ^' q -> non-trivial;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let p, q be non-multi Graph-yielding FinSequence;
cluster p ^ q -> non-multi;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is non-multi
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is non-multi
by FINSEQ_1:def 7, GLIB_000:def 62;
hence ex G being _Graph st (p^q).x = G & G is non-multi;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G & G is non-multi
by A2, FINSEQ_1:def 7, GLIB_000:def 62;
hence ex G being _Graph st (p^q).x = G & G is non-multi by A2;
end;
end;
hence thesis by GLIB_000:def 62;
end;
cluster p ^' q -> non-multi;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let p, q be non-Dmulti Graph-yielding FinSequence;
cluster p ^ q -> non-Dmulti;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is non-Dmulti
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is non-Dmulti
by FINSEQ_1:def 7, GLIB_000:def 63;
hence ex G being _Graph st (p^q).x = G & G is non-Dmulti;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G &
G is non-Dmulti by A2, FINSEQ_1:def 7, GLIB_000:def 63;
hence ex G being _Graph st (p^q).x = G & G is non-Dmulti by A2;
end;
end;
hence thesis by GLIB_000:def 63;
end;
cluster p ^' q -> non-Dmulti;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let p, q be simple Graph-yielding FinSequence;
cluster p ^ q -> simple;
coherence;
cluster p ^' q -> simple;
coherence;
end;
registration
let p, q be Dsimple Graph-yielding FinSequence;
cluster p ^ q -> Dsimple;
coherence;
cluster p ^' q -> Dsimple;
coherence;
end;
registration
let p, q be connected Graph-yielding FinSequence;
cluster p ^ q -> connected;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is connected
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is connected
by FINSEQ_1:def 7, GLIB_002:def 12;
hence ex G being _Graph st (p^q).x = G & G is connected;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G &
G is connected by A2, FINSEQ_1:def 7, GLIB_002:def 12;
hence ex G being _Graph st (p^q).x = G & G is connected by A2;
end;
end;
hence thesis by GLIB_002:def 12;
end;
cluster p ^' q -> connected;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let p, q be acyclic Graph-yielding FinSequence;
cluster p ^ q -> acyclic;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is acyclic
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is acyclic
by FINSEQ_1:def 7, GLIB_002:def 13;
hence ex G being _Graph st (p^q).x = G & G is acyclic;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G &
G is acyclic by A2, FINSEQ_1:def 7, GLIB_002:def 13;
hence ex G being _Graph st (p^q).x = G & G is acyclic by A2;
end;
end;
hence thesis by GLIB_002:def 13;
end;
cluster p ^' q -> acyclic;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let p, q be Tree-like Graph-yielding FinSequence;
cluster p ^ q -> Tree-like;
coherence;
cluster p ^' q -> Tree-like;
coherence;
end;
registration
let p, q be edgeless Graph-yielding FinSequence;
cluster p ^ q -> edgeless;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is edgeless
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is edgeless
by FINSEQ_1:def 7, Def2;
hence ex G being _Graph st (p^q).x = G & G is edgeless;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G &
G is edgeless by A2, FINSEQ_1:def 7, Def2;
hence ex G being _Graph st (p^q).x = G & G is edgeless by A2;
end;
end;
hence thesis;
end;
cluster p ^' q -> edgeless;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let G1, G2 be _Graph;
cluster <* G1, G2 *> -> Graph-yielding;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be _Graph;
cluster <* G1, G2, G3 *> -> Graph-yielding;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
registration
let G1, G2 be _finite _Graph;
cluster <* G1, G2 *> -> _finite;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be _finite _Graph;
cluster <* G1, G2, G3 *> -> _finite;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
registration
let G1, G2 be loopless _Graph;
cluster <* G1, G2 *> -> loopless;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be loopless _Graph;
cluster <* G1, G2, G3 *> -> loopless;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
registration
let G1, G2 be _trivial _Graph;
cluster <* G1, G2 *> -> _trivial;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be _trivial _Graph;
cluster <* G1, G2, G3 *> -> _trivial;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
registration
let G1, G2 be non _trivial _Graph;
cluster <* G1, G2 *> -> non-trivial;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be non _trivial _Graph;
cluster <* G1, G2, G3 *> -> non-trivial;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
registration
let G1, G2 be non-multi _Graph;
cluster <* G1, G2 *> -> non-multi;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be non-multi _Graph;
cluster <* G1, G2, G3 *> -> non-multi;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
registration
let G1, G2 be non-Dmulti _Graph;
cluster <* G1, G2 *> -> non-Dmulti;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be non-Dmulti _Graph;
cluster <* G1, G2, G3 *> -> non-Dmulti;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
registration
let G1, G2 be simple _Graph;
cluster <* G1, G2 *> -> simple;
coherence;
let G3 be simple _Graph;
cluster <* G1, G2, G3 *> -> simple;
coherence;
end;
registration
let G1, G2 be Dsimple _Graph;
cluster <* G1, G2 *> -> Dsimple;
coherence;
let G3 be Dsimple _Graph;
cluster <* G1, G2, G3 *> -> Dsimple;
coherence;
end;
registration
let G1, G2 be connected _Graph;
cluster <* G1, G2 *> -> connected;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be connected _Graph;
cluster <* G1, G2, G3 *> -> connected;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
registration
let G1, G2 be acyclic _Graph;
cluster <* G1, G2 *> -> acyclic;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be acyclic _Graph;
cluster <* G1, G2, G3 *> -> acyclic;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
registration
let G1, G2 be Tree-like _Graph;
cluster <* G1, G2 *> -> Tree-like;
coherence;
let G3 be Tree-like _Graph;
cluster <* G1, G2, G3 *> -> Tree-like;
coherence;
end;
registration
let G1, G2 be edgeless _Graph;
cluster <* G1, G2 *> -> edgeless;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be edgeless _Graph;
cluster <* G1, G2, G3 *> -> edgeless;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
begin :: Construction of finite Graphs
:: finite addition of vertices can be finitely constructed with addVertex only
theorem Th59:
for G2 being _Graph, V being finite set, G1 being addVertices of G2, V
ex p being non empty Graph-yielding FinSequence
st p.1 == G2 & p.len p = G1 & len p = card (V \ the_Vertices_of G2) + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G1
st p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n
proof
let G2 be _Graph;
defpred P[Nat] means for V being finite set, G1 being addVertices of G2, V
st card (V \ the_Vertices_of G2) = $1 holds
ex p being non empty Graph-yielding FinSequence
st p.1 == G2 & p.len p = G1 & len p = card (V \ the_Vertices_of G2) + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G1
st p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n;
A1: P[0]
proof
let V be finite set, G1 be addVertices of G2, V;
assume A2: card (V \ the_Vertices_of G2) = 0;
then V \ the_Vertices_of G2 = {};
then A3: G1 == G2 by XBOOLE_1:37, GLIB_006:78;
reconsider p = <* G1 *> as non empty Graph-yielding FinSequence;
take p;
thus p.1 == G2 by A3;
thus p.len p = p.1 by FINSEQ_1:40
.= G1;
thus len p = card (V \ the_Vertices_of G2) + 1 by A2, FINSEQ_1:40;
let n be Element of dom p;
1 <= n & n <= len p by FINSEQ_3:25;
then 1 <= n & n <= 1 by FINSEQ_1:40;
then A4: n = 1 by XXREAL_0:1;
assume n <= len p - 1;
then n <= 1 - 1 by FINSEQ_1:40;
hence thesis by A4; :: by contradiction
end;
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
let V be finite set, G1 be addVertices of G2, V;
assume A7: card (V \ the_Vertices_of G2) = k+1;
then A8: V \ the_Vertices_of G2 <> {};
set v0 = the Element of V \ the_Vertices_of G2;
set V0 = V \ {v0};
set G3 = the addVertices of G2, V0;
V0 \ the_Vertices_of G2 = V0 \ (V0 /\ the_Vertices_of G2) by XBOOLE_1:47;
then A9: card(V0 \ the_Vertices_of G2) =
card V0 - card(V0 /\ the_Vertices_of G2) by CARD_2:44, XBOOLE_1:17;
A10: v0 in V by A8, XBOOLE_0:def 5;
then A11: card V0 = card V - card {v0} by CARD_2:44, ZFMISC_1:31
.= card V - 1 by CARD_1:30;
A12: not v0 in the_Vertices_of G2 by A8, XBOOLE_0:def 5;
then the_Vertices_of G2 misses {v0} by ZFMISC_1:50;
then the_Vertices_of G2 /\ ({v0} \/ V0) = the_Vertices_of G2 /\ V0
by XBOOLE_1:78;
then the_Vertices_of G2 /\ V0 = the_Vertices_of G2 /\ V
by A10, ZFMISC_1:116;
then A13: card(V0 \ the_Vertices_of G2)
= card V - card(V /\ the_Vertices_of G2) - 1 by A9, A11
.= card(V \ (V /\ the_Vertices_of G2)) - 1 by CARD_2:44, XBOOLE_1:17
.= card(V \ the_Vertices_of G2) - 1 by XBOOLE_1:47
.= k by A7;
then consider p being non empty Graph-yielding FinSequence such that
A14: p.1 == G2 & p.len p = G3 &
len p = card (V0 \ the_Vertices_of G2) + 1 and
A15: for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G3
st p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n by A6;
reconsider q = p ^ <* G1 *> as non empty Graph-yielding FinSequence;
take q;
1 in dom p by FINSEQ_5:6;
hence q.1 == G2 by A14, FINSEQ_1:def 7;
A16: len q = len p + len <* G1 *> by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:40;
hence A17: q.len q = G1 by FINSEQ_1:42;
thus len q = card (V \ the_Vertices_of G2) + 1 by A7, A13, A14, A16;
G1 is addVertices of G2, {v0} \/ V0 by A10, ZFMISC_1:116;
then consider G4 being addVertices of G2, V0 such that
A18: G1 is addVertices of G4, {v0} by GLIB_006:83;
A19: G1 is addVertices of G3, {v0} by A18, Th32, GLIB_006:77;
let n be Element of dom q;
assume n <= len q - 1;
then per cases by Lm12;
suppose A20: n = len q - 1;
then A21: q.(n+1) = G1 by A17;
1 <= n by FINSEQ_3:25; then
n in dom p by A16, A20, FINSEQ_3:25;
then A24: q.n = G3 by A14, A16, A20, FINSEQ_1:def 7;
the_Vertices_of G1 = the_Vertices_of G2 \/ V by GLIB_006:def 10;
then reconsider v0 as Vertex of G1 by A10, TARSKI:def 3, XBOOLE_1:7;
take v0;
thus q.(n+1) is addVertex of q.n, v0 by A19, A21, A24;
v0 in {v0} by TARSKI:def 1;
then not v0 in V0 by XBOOLE_0:def 5;
then not v0 in the_Vertices_of G2 \/ V0 by A12, XBOOLE_0:def 3;
hence not v0 in the_Vertices_of q.n by A24, GLIB_006:def 10;
end;
suppose A25: n <= len p - 1;
then A26: n+0 <= len p - 1 + 1 by XREAL_1:7;
1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A26, FINSEQ_3:25;
consider v being Vertex of G3 such that
A27: p.(m+1) is addVertex of p.m, v & not v in the_Vertices_of p.m
by A15, A25;
1+0 <= n+1 & n+1 <= len p - 1 + 1 by A25, XREAL_1:6;
then n+1 in dom p by FINSEQ_3:25;
then A28: q.(n+1) = p.(m+1) by FINSEQ_1:def 7;
A29: q.n = p.m by FINSEQ_1:def 7;
the_Vertices_of G3 c= the_Vertices_of G1 by A19, GLIB_006:def 9;
then reconsider v as Vertex of G1 by TARSKI:def 3;
take v;
thus thesis by A27, A28, A29;
end;
end;
A30: for k being Nat holds P[k] from NAT_1:sch 2(A1,A5);
thus thesis by A30;
end;
theorem Th60:
for G being _finite _Graph, H being Subgraph of G st G.size() = H.size()
ex p being non empty _finite Graph-yielding FinSequence
st p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G
st p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n
proof
let G be _finite _Graph, H be Subgraph of G;
assume A1: G.size() = H.size();
set V = the_Vertices_of G \ the_Vertices_of H;
G is addVertices of H, V by A1, Th34;
then consider p being non empty Graph-yielding FinSequence such that
A2: p.1 == H & p.len p = G & len p = card (V \ the_Vertices_of H) + 1 and
A3: for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G
st p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n by Th59;
defpred P[Nat] means for n being Element of dom p st $1 = n
holds p.n is _finite;
A4: P[1] by A2, GLIB_000:89;
A5: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume A6: P[k];
let m be Element of dom p;
assume A7: k+1 = m;
then A8: k+1 <= len p by FINSEQ_3:25;
then A9: k+1-1 <= len p - 0 by XREAL_1:13;
1 <= k by NAT_1:14;
then reconsider n = k as Element of dom p by A9, FINSEQ_3:25;
k+1-1 <= len p - 1 by A8, XREAL_1:9;
then consider v being Vertex of G such that
A10: p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n by A3;
p.n is _finite by A6;
hence thesis by A7, A10;
end;
A11: for k being non zero Nat holds P[k] from NAT_1:sch 10(A4,A5);
for x being Element of dom p holds p.x is _finite
proof
let x be Element of dom p;
x is non zero Nat by FINSEQ_3:25;
hence thesis by A11;
end;
then reconsider p as non empty _finite Graph-yielding FinSequence
by GLIB_000:def 66;
take p;
thus p.1 == H & p.len p = G by A2;
V \ the_Vertices_of H = the_Vertices_of G \
(the_Vertices_of H \/ the_Vertices_of H) by XBOOLE_1:41
.= the_Vertices_of G \ the_Vertices_of H;
hence len p = card (the_Vertices_of G) - card(the_Vertices_of H) + 1
by A2, CARD_2:44
.= G.order() - card(the_Vertices_of H) + 1 by GLIB_000:def 24
.= G.order() - H.order() + 1 by GLIB_000:def 24;
thus thesis by A3;
end;
theorem Th61:
for G being _finite edgeless _Graph, H being Subgraph of G
ex p being non empty _finite edgeless Graph-yielding FinSequence
st p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G
st p.(n+1) is addVertex of p.n,v & not v in the_Vertices_of p.n
proof
let G be _finite edgeless _Graph, H be Subgraph of G;
G.size() = 0 by Th49
.= H.size() by Th49;
then consider p being non empty _finite Graph-yielding FinSequence such that
A1: p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 and
A2: for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G
st p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n
by Th60;
defpred P[Nat] means for n being Element of dom p st $1 = n
holds p.n is edgeless;
A3: P[1] by A1, Th52;
A4: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume A5: P[k];
let m be Element of dom p;
assume A6: k+1 = m;
then A7: k+1 <= len p by FINSEQ_3:25;
then A8: k+1-1 <= len p - 0 by XREAL_1:13;
1 <= k by NAT_1:14;
then reconsider n = k as Element of dom p by A8, FINSEQ_3:25;
k+1-1 <= len p - 1 by A7, XREAL_1:9;
then consider v being Vertex of G such that
A9: p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n by A2;
p.n is edgeless by A5;
hence thesis by A6, A9;
end;
A10: for k being non zero Nat holds P[k] from NAT_1:sch 10(A3,A4);
for x being Element of dom p holds p.x is edgeless
proof
let x be Element of dom p;
x is non zero Nat by FINSEQ_3:25;
hence thesis by A10;
end;
then p is edgeless;
then reconsider p as non empty _finite edgeless Graph-yielding FinSequence;
take p;
thus thesis by A1, A2;
end;
:: finite edgeless graphs can be finitely constructed with addVertex only
theorem Th62:
for G being _finite edgeless _Graph
ex p being non empty _finite edgeless Graph-yielding FinSequence
st p.1 is _trivial edgeless & p.len p = G & len p = G.order() &
for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G
st p.(n+1) is addVertex of p.n,v & not v in the_Vertices_of p.n
proof
let G be _finite edgeless _Graph;
set v0 = the Vertex of G;
set H = the inducedSubgraph of G, {v0};
consider p being non empty _finite edgeless Graph-yielding FinSequence
such that
A1: p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 and
A2: for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G
st p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n by Th61;
take p;
thus p.1 is _trivial edgeless by A1, Th52, GLIB_000:89;
thus p.len p = G by A1;
H.order() = 1 by GLIB_000:26;
hence len p = G.order() by A1;
thus thesis by A2;
end;
scheme
FinEdgelessGraphs { P[_finite _Graph] } :
for G being _finite edgeless _Graph holds P[G]
provided
A1: for G being _trivial edgeless _Graph holds P[G] and
A2: for G2 being _finite edgeless _Graph, v being object
for G1 being addVertex of G2,v
st not v in the_Vertices_of G2 & P[G2] holds P[G1]
proof
let G be _finite edgeless _Graph;
consider p being non empty _finite edgeless Graph-yielding FinSequence
such that
A3: p.1 is _trivial edgeless & p.len p = G & len p = G.order() and
A4: for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G
st p.(n+1) is addVertex of p.n,v & not v in the_Vertices_of p.n
by Th62;
defpred Q[Nat] means $1 + 1 <= len p implies
ex k being Element of dom p st k = $1 + 1 & P[p.k];
A5: Q[0]
proof
assume 0 + 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus k = 0 + 1;
thus P[p.k] by A1, A3;
end;
A6: for m being Nat st Q[m] holds Q[m+1]
proof
let m be Nat;
assume A7: Q[m];
assume A8: m+1 + 1 <= len p;
then m+1 +1 -1 <= len p - 0 by XREAL_1:13;
then consider k0 being Element of dom p such that
A9: k0 = m + 1 & P[p.k0] by A7;
set k = k0+1;
0+1 <= k by XREAL_1:6;
then reconsider k as Element of dom p by A8, A9, FINSEQ_3:25;
take k;
thus k = m+1 + 1 by A9;
k0 +1-1 <= len p - 1 by A8, A9, XREAL_1:9;
then consider v being Vertex of G such that
A10: p.k is addVertex of p.k0,v & not v in the_Vertices_of p.k0 by A4;
thus P[p.k] by A2, A9, A10;
end;
A11: for m being Nat holds Q[m] from NAT_1:sch 2(A5,A6);
len p - 1 is Nat & len p - 1 + 1 <= len p by INT_1:74;
then ex k being Element of dom p st k = len p - 1 + 1 & P[p.k] by A11;
hence thesis by A3;
end;
theorem
for p being non empty Graph-yielding FinSequence
st p.1 is edgeless &
for n being Element of dom p st n <= len p - 1 holds
ex v being object st p.(n+1) is addVertex of p.n,v
holds p.len p is edgeless
proof
defpred P[Nat] means for p being non empty Graph-yielding FinSequence
st len p = $1 & p.1 is edgeless &
for n being Element of dom p st n <= len p - 1 holds
ex v being object st p.(n+1) is addVertex of p.n,v
holds p.len p is edgeless;
A1: P[1];
A2: for m being non zero Nat st P[m] holds P[m+1]
proof
let m be non zero Nat;
assume A3: P[m];
let p be non empty Graph-yielding FinSequence;
assume that
A4: len p = m + 1 & p.1 is edgeless and
A5: for n being Element of dom p st n <= len p - 1 holds
ex v being object st p.(n+1) is addVertex of p.n,v;
reconsider q = p|m as non empty Graph-yielding FinSequence;
m+1-1 <= len p - 0 by A4, XREAL_1:10;
then A6: len q = m by FINSEQ_1:59;
A7: 1 <= m by INT_1:74;
then A8: q.1 is edgeless by A4, FINSEQ_3:112;
now
let n be Element of dom q;
assume A9: n <= len q - 1;
then n + 0 <= m - 1 + 1 by A6, XREAL_1:7;
then A10: n <= len p - 1 by A4;
A11: 1 <= n & n <= len q by FINSEQ_3:25;
then 1 <= n & n + 0 <= m + 1 by A6, XREAL_1:7;
then reconsider k = n as Element of dom p by A4, FINSEQ_3:25;
consider v being object such that
A12: p.(k+1) is addVertex of p.k,v by A5, A10;
take v;
n+1 <= len q - 1 + 1 by A9, XREAL_1:6;
then p.(k+1) = q.(n+1) & p.k = q.k by A6, A11, FINSEQ_3:112;
hence q.(n+1) is addVertex of q.n,v by A12;
end;
then A13: q.len q is edgeless by A3, A6, A8;
m+0 <= len p - 1 + 1 by A4, XREAL_1:6;
then reconsider k=m as Element of dom p by A7, FINSEQ_3:25;
consider v be object such that
A14: p.(k+1) is addVertex of p.k,v by A5, A4;
p.k = q.len q by A6, FINSEQ_3:112;
hence thesis by A13, A4, A14;
end;
A15: for m being non zero Nat holds P[m] from NAT_1:sch 10(A1,A2);
let p be non empty Graph-yielding FinSequence;
assume that
A16: p.1 is edgeless &
for n being Element of dom p st n <= len p - 1 holds
ex v being object st p.(n+1) is addVertex of p.n,v;
thus thesis by A15, A16;
end;
theorem Th64:
for G being _finite _Graph, H being spanning Subgraph of G
ex p being non empty _finite Graph-yielding FinSequence
st p.1 == H & p.len p = G & len p = G.size() - H.size() + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n
proof
let G be _finite _Graph;
defpred P[Nat] means for H being spanning Subgraph of G
st G.size() - H.size() = $1
ex p being non empty _finite Graph-yielding FinSequence
st p.1 == H & p.len p = G & len p = G.size() - H.size() + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n;
A1: P[0]
proof
let H be spanning Subgraph of G;
assume A2: G.size() - H.size() = 0;
then A3: G == H by GLIB_000:119;
reconsider p = <* G *> as non empty _finite Graph-yielding FinSequence;
take p;
thus p.1 == H by A3;
thus p.len p = p.1 by FINSEQ_1:40
.= G;
thus len p = G.size() - H.size() + 1 by A2, FINSEQ_1:40;
let n be Element of dom p;
1 <= n & n <= len p by FINSEQ_3:25;
then 1 <= n & n <= 1 by FINSEQ_1:40;
then A4: n = 1 by XXREAL_0:1;
assume n <= len p - 1;
then n <= 1 - 1 by FINSEQ_1:40;
hence thesis by A4; :: by contradiction
end;
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
let H be spanning Subgraph of G;
assume A7: G.size() - H.size() = k+1;
A8: the_Edges_of G \ the_Edges_of H <> {}
proof
assume A9: the_Edges_of G \ the_Edges_of H = {};
0 = card(the_Edges_of G \ the_Edges_of H) by A9
.= card the_Edges_of G - card the_Edges_of H by CARD_2:44
.= G.size() - card the_Edges_of H by GLIB_000:def 25
.= G.size() - H.size() by GLIB_000:def 25;
hence contradiction by A7;
end;
set e0 = the Element of the_Edges_of G \ the_Edges_of H;
A10: e0 in the_Edges_of G by A8, TARSKI:def 3;
then reconsider e0 as Element of the_Edges_of G;
set u = (the_Source_of G).e0, w = (the_Target_of G).e0;
reconsider u,w as Vertex of G by A10, FUNCT_2:5;
A11: the_Vertices_of G = the_Vertices_of H by GLIB_000:def 33;
set H1 = the addEdge of H, u, e0, w;
A12: not e0 in the_Edges_of H by A8, XBOOLE_0:def 5;
A13: k = G.size() - (H.size() + 1) by A7
.= G.size() - H1.size() by A12, A11, GLIB_006:111;
A14: the_Vertices_of H1 = the_Vertices_of H by A11, GLIB_006:102;
H1 is Subgraph of G
proof
for e being object holds
e in the_Edges_of H1 implies e in the_Edges_of G
proof
let e be object;
assume A15: e in the_Edges_of H1;
the_Edges_of H1 = the_Edges_of H \/ {e0} by A11, A12, GLIB_006:def 11;
then per cases by A15, XBOOLE_0:def 3;
suppose e in the_Edges_of H;
hence thesis;
end;
suppose e in {e0};
hence thesis by A10, TARSKI:def 1;
end;
end;
then A16: the_Edges_of H1 c= the_Edges_of G by TARSKI:def 3;
now
let e be set;
assume e in the_Edges_of H1;
then A17: e in the_Edges_of H \/ {e0} by A11, A12, GLIB_006:def 11;
per cases;
suppose e <> e0;
then not e in {e0} by TARSKI:def 1;
then A18: e in the_Edges_of H by A17, XBOOLE_0:def 3;
thus (the_Source_of H1).e = (the_Source_of H).e by A18
, GLIB_006:def 9
.= (the_Source_of G).e by A18, GLIB_000:def 32;
thus (the_Target_of H1).e = (the_Target_of H).e by A18
, GLIB_006:def 9
.= (the_Target_of G).e by A18, GLIB_000:def 32;
end;
suppose A19: e = e0;
then e DJoins u,w,H1 by A11, A12, GLIB_006:105;
hence (the_Source_of H1).e = (the_Source_of G).e &
(the_Target_of H1).e = (the_Target_of G).e by A19, GLIB_000:def 14;
end;
end;
hence thesis by A14, A16, GLIB_000:def 32;
end;
then H1 is spanning Subgraph of G by A11, A14, GLIB_000:def 33;
then consider p being non empty _finite Graph-yielding FinSequence
such that
A20: p.1 == H1 & p.len p = G & len p = G.size() - H1.size() + 1 and
A21: for n being Element of dom p st n <= len p - 1 holds
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n by A6, A13;
reconsider q = <* H *> ^ p
as non empty _finite Graph-yielding FinSequence;
take q;
A22: q.1 = H by FINSEQ_1:41;
thus q.1 == H by FINSEQ_1:41;
A23: len q = len <* H *> + len p by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:40;
len p in dom p by FINSEQ_5:6;
hence q.len q = G by A20, A23, FINSEQ_3:103;
A24: H.size() + 1 - 1 = H1.size() - 1 by A12, A11, GLIB_006:111;
thus len q = G.size() - H.size() + 1 by A20, A23, A24;
let n be Element of dom q;
assume n <= len q - 1;
then per cases by Lm13;
suppose A25: n = 1;
take u,w,e0;
1 in dom p by FINSEQ_5:6;
then A26: p.1 = q.(len <* H *> +1) by FINSEQ_1:def 7
.= q.(n+1) by A25, FINSEQ_1:40;
H1 is addEdge of q.n, u, e0, w by A25, FINSEQ_1:41;
hence q.(n+1) is addEdge of q.n, u, e0, w by A26, A20, GLIB_006:101;
thus e0 in the_Edges_of G \ the_Edges_of q.n
by A10, A12, A22, A25, XBOOLE_0:def 5;
thus u in the_Vertices_of q.n & w in the_Vertices_of q.n
by A11, A22, A25;
end;
suppose A27: n-1 in dom p & n-1 <= len p - 1;
then reconsider m = n-1 as Element of dom p;
consider v1,v2 being Vertex of G, e being object such that
A28: p.(m+1) is addEdge of p.m,v1,e,v2 and
A29: e in the_Edges_of G \ the_Edges_of p.m &
v1 in the_Vertices_of p.m & v2 in the_Vertices_of p.m by A21, A27;
take v1,v2,e;
A30: 1 <= n by FINSEQ_3:25;
n <= len p by A27, XREAL_1:9;
then n in dom p by A30, FINSEQ_3:25;
then
A31: p.n = q.(len <* H *> + n) by FINSEQ_1:def 7
.= q.(n+1) by FINSEQ_1:40;
p.m = q.(len <* H *> + m) by FINSEQ_1:def 7
.= q.(m+1) by FINSEQ_1:40
.= q.n;
hence thesis by A28, A29, A31;
end;
end;
A32: for k being Nat holds P[k] from NAT_1:sch 2(A1,A5);
let H be spanning Subgraph of G;
G.size() - H.size() is Nat by GLIB_000:75, NAT_1:21;
hence thesis by A32;
end;
theorem
for G being _finite _Graph
ex p being non empty _finite Graph-yielding FinSequence
st p.1 is edgeless & p.len p = G & len p = G.size() + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n
proof
let G be _finite _Graph;
set H = the edgeless spanning Subgraph of G;
consider p being non empty _finite Graph-yielding FinSequence such that
A1: p.1 == H & p.len p = G & len p = G.size() - H.size() + 1 and
A2: for n being Element of dom p st n <= len p - 1 holds
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n by Th64;
take p;
thus p.1 is edgeless & p.len p = G by A1, Th52;
thus len p = G.size() - 0 + 1 by A1, Th49 .= G.size() + 1;
thus thesis by A2;
end;
theorem Th66:
for G being _finite connected _Graph,
H being spanning connected Subgraph of G
ex p being non empty _finite connected Graph-yielding FinSequence
st p.1 == H & p.len p = G & len p = G.size() - H.size() + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n
proof
let G be _finite connected _Graph, H be spanning connected Subgraph of G;
consider p being non empty _finite Graph-yielding FinSequence such that
A1: p.1 == H & p.len p = G & len p = G.size() - H.size() + 1 and
A2: for n being Element of dom p st n <= len p - 1 holds
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n by Th64;
defpred P[Nat] means for n being Element of dom p st $1 = n
holds p.n is connected;
A3: P[1] by A1, GLIB_002:8;
A4: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume A5: P[k];
let m be Element of dom p;
assume A6: k+1 = m;
then A7: k+1 <= len p by FINSEQ_3:25;
then A8: k+1-1 <= len p - 0 by XREAL_1:13;
1 <= k by NAT_1:14;
then reconsider n = k as Element of dom p by A8, FINSEQ_3:25;
k+1-1 <= len p - 1 by A7, XREAL_1:9;
then consider v1,v2 being Vertex of G, e being object such that
A9: p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n by A2;
p.n is connected by A5;
hence thesis by A6, A9;
end;
A10: for k being non zero Nat holds P[k] from NAT_1:sch 10(A3,A4);
for x being Element of dom p holds p.x is connected
proof
let x be Element of dom p;
x is non zero Nat by FINSEQ_3:25;
hence thesis by A10;
end;
then reconsider p as non empty _finite connected Graph-yielding FinSequence
by GLIB_002:def 15;
take p;
thus thesis by A1, A2;
end;
theorem Th67:
for G1 being _finite _Graph, H being Subgraph of G1
ex G2 being spanning Subgraph of G1,
p being non empty _finite Graph-yielding FinSequence
st H.size() = G2.size() & p.1 == H & p.len p = G2 &
len p = G1.order() - H.order() + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G1 st p.(n+1) is addVertex of p.n, v &
not v in the_Vertices_of p.n
proof
let G1 be _finite _Graph, H be Subgraph of G1;
set V = the_Vertices_of G1 \ the_Vertices_of H;
set G2 = the addVertices of H, V;
consider p being non empty Graph-yielding FinSequence such that
A1: p.1 == H & p.len p = G2 & len p = card (V \ the_Vertices_of H) + 1 and
A2: for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G2
st p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n by Th59;
defpred P[Nat] means for n being Element of dom p st $1 = n
holds p.n is _finite;
A3: P[1] by A1, GLIB_000:89;
A4: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume A5: P[k];
let m be Element of dom p;
assume A6: k+1 = m;
then A7: k+1 <= len p by FINSEQ_3:25;
then A8: k+1-1 <= len p - 0 by XREAL_1:13;
1 <= k by NAT_1:14;
then reconsider n = k as Element of dom p by A8, FINSEQ_3:25;
k+1-1 <= len p - 1 by A7, XREAL_1:9;
then consider v being Vertex of G2 such that
A9: p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n by A2;
p.n is _finite by A5;
hence thesis by A6, A9;
end;
A10: for k being non zero Nat holds P[k] from NAT_1:sch 10(A3,A4);
for x being Element of dom p holds p.x is _finite
proof
let x be Element of dom p;
x is non zero Nat by FINSEQ_3:25;
hence thesis by A10;
end;
then reconsider p as non empty _finite Graph-yielding FinSequence
by GLIB_000:def 66;
A11: the_Vertices_of G2 = the_Vertices_of H \/
(the_Vertices_of G1 \ the_Vertices_of H) by GLIB_006:def 10
.= the_Vertices_of G1 by XBOOLE_1:45;
G2 is Subgraph of G1
proof
the_Edges_of G2 = the_Edges_of H &
the_Source_of G2 = the_Source_of H &
the_Target_of G2 = the_Target_of H by GLIB_006:def 10;
then the_Edges_of G2 c= the_Edges_of G1 &
for e being set st e in the_Edges_of G2 holds
(the_Source_of G2).e = (the_Source_of G1).e &
(the_Target_of G2).e = (the_Target_of G1).e by GLIB_000:def 32;
hence thesis by A11, GLIB_000:def 32;
end;
then reconsider G2 as spanning Subgraph of G1 by A11, GLIB_000:def 33;
take G2, p;
thus H.size() = G2.size() by GLIB_006:95;
thus p.1 == H & p.len p = G2 by A1;
V \ the_Vertices_of H = the_Vertices_of G1 \
(the_Vertices_of H \/ the_Vertices_of H) by XBOOLE_1:41
.= the_Vertices_of G1 \ the_Vertices_of H;
hence len p
= card (the_Vertices_of G1) - card(the_Vertices_of H) + 1 by A1, CARD_2:44
.= G1.order() - card(the_Vertices_of H) + 1 by GLIB_000:def 24
.= G1.order() - H.order() + 1 by GLIB_000:def 24;
let n be Element of dom p;
assume n <= len p - 1;
then consider v being Vertex of G2 such that
A12: p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n by A2;
the_Vertices_of G2 c= the_Vertices_of G1;
then reconsider v as Vertex of G1 by TARSKI:def 3;
take v;
thus thesis by A12;
end;
theorem Th68:
for G being _finite _Graph, H being Subgraph of G
ex p being non empty _finite Graph-yielding FinSequence
st p.1 == H & p.len p = G &
len p = G.order() + G.size() - (H.order() + H.size()) + 1 &
for n being Element of dom p st n <= len p - 1 holds
(ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n) or
(ex v being Vertex of G st p.(n+1) is addVertex of p.n, v &
not v in the_Vertices_of p.n)
proof
let G be _finite _Graph, H be Subgraph of G;
per cases;
suppose A1: G.size() <> H.size();
consider G2 being spanning Subgraph of G,
p being non empty _finite Graph-yielding FinSequence such that
A2: H.size() = G2.size() and
A3: p.1 == H & p.len p = G2 & len p = G.order() - H.order() + 1 and
A4:for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G st p.(n+1) is addVertex of p.n, v &
not v in the_Vertices_of p.n by Th67;
consider q being non empty _finite Graph-yielding FinSequence such that
A5: q.1 == G2 & q.len q = G & len q = G.size() - G2.size() + 1 and
A6: for n being Element of dom q st n <= len q - 1 holds
ex v1,v2 being Vertex of G, e being object
st q.(n+1) is addEdge of q.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of q.n &
v1 in the_Vertices_of q.n & v2 in the_Vertices_of q.n by Th64;
reconsider r = p ^' q as non empty _finite Graph-yielding FinSequence;
take r;
1 <= len p by FINSEQ_1:20;
hence r.1 == H by A3, FINSEQ_6:140;
A7: 1 < len q
proof
assume not 1 < len q;
then len q <= 1 & 1 <= len q by FINSEQ_1:20;
then len q = 1 by XXREAL_0:1;
hence contradiction by A1, A2, A5;
end;
hence r.len r = G by A5, FINSEQ_6:142;
len r + 1 = len p + len q by FINSEQ_6:139
.= G.order() + G.size() - (H.order() + H.size()) + 1 + 1 by A2, A3, A5;
hence len r = G.order() + G.size() - (H.order() + H.size()) + 1;
let n be Element of dom r;
assume A8: n <= len r - 1;
n < len p or n = len p or n > len p by XXREAL_0:1;
then n+1 <= len p or n = len p or n > len p by INT_1:7;
then n+1-1 <= len p - 1 or n = len p or n > len p by XREAL_1:9;
then per cases;
suppose A9: n <= len p - 1;
then A10: n+0 <= len p - 1+1 & n+1 <= len p -1+1 by XREAL_1:7;
A11: 1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A10, FINSEQ_3:25;
A12: r.n = p.m by A10, A11, FINSEQ_6:140;
1+0 <= n+1 by XREAL_1:7;
then r.(n+1) = p.(m+1) by A10, FINSEQ_6:140;
hence thesis by A4, A9, A12;
end;
suppose A13: n = len p;
then 1 <= n & n <= len p by FINSEQ_1:20;
then A14: r.n = G2 by A3, A13, FINSEQ_6:140;
reconsider m = 1 as Element of dom q by A7, FINSEQ_3:25;
A15: r.(n+1) = q.(m+1) by A13, A7, FINSEQ_6:141;
now
m+1 <= len q by A7, INT_1:7;
then m+1-1 <= len q - 1 by XREAL_1:9;
then consider v1,v2 being Vertex of G, e being object such that
A16: q.(m+1) is addEdge of q.m,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of q.m &
v1 in the_Vertices_of q.m & v2 in the_Vertices_of q.m by A6;
take v1,v2,e;
thus r.(n+1) is addEdge of r.n,v1,e,v2 by A14, A15, A5, A16, Th36;
thus e in the_Edges_of G \ the_Edges_of r.n &
v1 in the_Vertices_of r.n & v2 in the_Vertices_of r.n
by A14, A16, A5, GLIB_000:def 34;
end;
hence thesis;
end;
suppose A17: n > len p;
then reconsider n1 = n-1 as Nat by NAT_1:20;
n1+1 = n;
then len p <= n1 by A17, NAT_1:13;
then reconsider k1 = n1 - len p as Nat by NAT_1:21;
set k = k1+1;
A18: k+1 < len q
proof
assume len q <= k + 1;
then len q + len p <= k + 1 + len p by XREAL_1:6;
then len r + 1 <= n + 1 by FINSEQ_6:139;
then len r - 1 <= n - 1 by XREAL_1:6, XREAL_1:9;
then n <= n-1 by A8, XXREAL_0:2;
then n-n <= n-1-n by XREAL_1:9;
then 0 <= -1;
hence contradiction;
end;
then k+1-1 < len q - 0 by XREAL_1:14;
then r.(len p + k) = q.(k+1) by NAT_1:14, FINSEQ_6:141;
then A19: r.n = q.(k+1);
1+0 <= k+1 by XREAL_1:7;
then r.(len p +(k+1)) = q.((k+1)+1) by A18, FINSEQ_6:141;
then A20: r.(n+1) = q.((k+1)+1);
1+0 <= k+1 & k+1 <= len q by A18, XREAL_1:7;
then reconsider m=k+1 as Element of dom q by FINSEQ_3:25;
now
m+1 <= len q by A18, INT_1:7;
then m+1-1 <= len q - 1 by XREAL_1:9;
then consider v1,v2 being Vertex of G, e being object such that
A21: q.(m+1) is addEdge of q.m,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of q.m &
v1 in the_Vertices_of q.m & v2 in the_Vertices_of q.m by A6;
take v1,v2,e;
thus r.(n+1) is addEdge of r.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of r.n &
v1 in the_Vertices_of r.n & v2 in the_Vertices_of r.n
by A19, A20, A21;
end;
hence thesis;
end;
end;
suppose A22: G.size() = H.size();
then consider p being non empty _finite Graph-yielding FinSequence
such that
A23: p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 and
A24: for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G
st p.(n+1) is addVertex of p.n, v & not v in the_Vertices_of p.n
by Th60;
take p;
thus p.1 == H & p.len p = G by A23;
thus len p
= G.order() + G.size() - (H.order() + H.size()) + 1 by A22, A23;
let n be Element of dom p;
assume n <= len p - 1;
hence thesis by A24;
end;
end;
:: finite graphs can be finitely constructed with addVertex and addEdge only
theorem Th69:
for G being _finite _Graph
ex p being non empty _finite Graph-yielding FinSequence
st p.1 is _trivial edgeless & p.len p = G & len p = G.order() + G.size() &
for n being Element of dom p st n <= len p - 1 holds
(ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n) or
(ex v being Vertex of G st p.(n+1) is addVertex of p.n, v &
not v in the_Vertices_of p.n)
proof
let G be _finite _Graph;
set H = the _trivial edgeless Subgraph of G;
consider p being non empty _finite Graph-yielding FinSequence such that
A1: p.1 == H & p.len p = G and
A2: len p = G.order() + G.size() - (H.order() + H.size()) + 1 and
A3: for n being Element of dom p st n <= len p - 1 holds
(ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n) or
(ex v being Vertex of G st p.(n+1) is addVertex of p.n, v &
not v in the_Vertices_of p.n) by Th68;
take p;
thus p.1 is _trivial edgeless by A1, Th52, GLIB_000:89;
thus p.len p = G by A1;
thus len p = G.order() + G.size() - (H.order() + 0) + 1 by A2, Th49
.= G.order() + G.size() - 1 + 1 by GLIB_000:26
.= G.order() + G.size();
thus thesis by A3;
end;
scheme
FinGraphs { P[_finite _Graph] } : for G being _finite _Graph holds P[G]
provided
A1: for G being _trivial edgeless _Graph holds P[G] and
A2: for G2 being _finite _Graph, v being object
for G1 being addVertex of G2,v
st not v in the_Vertices_of G2 & P[G2] holds P[G1] and
A3: for G2 being _finite _Graph, v1, v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
st not e in the_Edges_of G2 & P[G2] holds P[G1]
proof
let G be _finite _Graph;
consider p being non empty _finite Graph-yielding FinSequence such that
A4: p.1 is _trivial edgeless & p.len p = G & len p = G.order() + G.size()
and A5: for n being Element of dom p st n <= len p - 1 holds
(ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n) or
(ex v being Vertex of G st p.(n+1) is addVertex of p.n, v &
not v in the_Vertices_of p.n) by Th69;
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & P[p.k];
A6: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus 1 = k;
thus P[p.k] by A1, A4;
end;
A7: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A8: Q[m];
assume A9: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A9, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A9, XREAL_1:13;
then consider k0 being Element of dom p such that
A10: m = k0 & P[p.k0] by A8;
m+1-1 <= len p - 1 by A9, XREAL_1:9;
then per cases by A5, A10;
suppose ex v1,v2 being Vertex of G, e being object
st p.(k0+1) is addEdge of p.k0,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.k0 &
v1 in the_Vertices_of p.k0 & v2 in the_Vertices_of p.k0;
then consider v1,v2 being Vertex of G, e being object such that
A11: p.(k0+1) is addEdge of p.k0,v1,e,v2 and
A12: e in the_Edges_of G \ the_Edges_of p.k0 &
v1 in the_Vertices_of p.k0 & v2 in the_Vertices_of p.k0;
reconsider v1, v2 as Vertex of p.k0 by A12;
A13: not e in the_Edges_of p.k0 by A12, XBOOLE_0:def 5;
A14: p.k is addEdge of p.k0,v1,e,v2 by A10, A11;
thus thesis by A3, A10, A13, A14;
end;
suppose ex v being Vertex of G st p.(k0+1) is addVertex of p.k0, v &
not v in the_Vertices_of p.k0;
then consider v being Vertex of G such that
A15: p.(k0+1) is addVertex of p.k0, v & not v in the_Vertices_of p.k0;
thus thesis by A2, A10, A15;
end;
end;
A16: for m being non zero Nat holds Q[m] from NAT_1:sch 10(A6,A7);
consider k being Element of dom p such that
A17: len p = k & P[p.k] by A16;
thus thesis by A4, A17;
end;
theorem
for p being non empty Graph-yielding FinSequence
st p.1 is _finite &
for n being Element of dom p st n <= len p - 1 holds
(ex v being object st p.(n+1) is addVertex of p.n,v) or
(ex v1,e,v2 being object st p.(n+1) is addEdge of p.n,v1,e,v2)
holds p.len p is _finite
proof
let p be non empty Graph-yielding FinSequence;
assume that A1: p.1 is _finite and
A2: for n being Element of dom p st n <= len p - 1 holds
(ex v being object st p.(n+1) is addVertex of p.n,v) or
(ex v1,e,v2 being object st p.(n+1) is addEdge of p.n,v1,e,v2);
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & p.k is _finite;
A3: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus thesis by A1;
end;
A4: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A5: Q[m];
assume A6: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A6, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A6, XREAL_1:13;
then consider k0 being Element of dom p such that
A7: m = k0 & p.k0 is _finite by A5;
m+1-1 <= len p - 1 by A6, XREAL_1:9;
then per cases by A2, A7;
suppose ex v being object st p.(k0+1) is addVertex of p.k0,v;
hence thesis by A7;
end;
suppose ex v1,e,v2 being object st p.(k0+1) is addEdge of p.k0,v1,e,v2;
hence thesis by A7;
end;
end;
A8: for m being non zero Nat holds Q[m] from NAT_1:sch 10(A3,A4);
consider k being Element of dom p such that
A9: len p = k & p.k is _finite by A8;
thus thesis by A9;
end;
theorem Th71:
for G being _finite Tree-like _Graph, H being connected Subgraph of G
ex p being non empty _finite Tree-like Graph-yielding FinSequence
st p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 &
for n being Element of dom p st n <= len p - 1
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n))
proof
defpred P[Nat] means for G being _finite Tree-like _Graph
for H being connected Subgraph of G st $1 = G.order() - H.order()
ex p being non empty _finite Tree-like Graph-yielding FinSequence
st p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 &
for n being Element of dom p st n <= len p - 1
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n));
A1: P[0]
proof
let G be _finite Tree-like _Graph, H be connected Subgraph of G;
assume A2: 0 = G.order() - H.order();
then H is spanning by GLIB_000:117;
then A3: G == H by Th21;
reconsider p = <* G *>
as non empty _finite Tree-like Graph-yielding FinSequence;
take p;
thus p.1 == H by A3;
thus p.len p = p.1 by FINSEQ_1:40
.= G;
thus len p = G.order() - H.order() + 1 by A2, FINSEQ_1:40;
let n be Element of dom p;
1 <= n & n <= len p by FINSEQ_3:25;
then 1 <= n & n <= 1 by FINSEQ_1:40;
then A4: n = 1 by XXREAL_0:1;
assume n <= len p - 1;
then n <= 1 - 1 by FINSEQ_1:40;
hence thesis by A4; :: by contradiction
end;
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
let G be _finite Tree-like _Graph, H be connected Subgraph of G;
assume A7: k+1 = G.order() - H.order();
then A8: G.order() = H.order() + k + 1;
G.order() <> H.order()
proof
assume G.order() = H.order();
then 0 + H.order() = k+1 + H.order() by A8;
hence contradiction;
end;
then A9: H is non spanning by GLIB_000:117;
G.order() <> 1 by A8, NAT_1:7;
then A10: G is non _trivial by GLIB_000:26;
then consider v being Vertex of G such that
A11: v is endvertex & not v in the_Vertices_of H by A9, Th31;
consider e0 being object such that
A12: v.edgesInOut() = {e0} & not e0 Joins v,v,G by A11, GLIB_000:def 51;
set G2 = the removeVertex of G, v;
A13: G2.order() + 1 = G.order() by A10, GLIB_000:48;
then A14: k = G2.order() - H.order() by A7;
A15: the_Edges_of G2 = G.edgesBetween(the_Vertices_of G \ {v})
by A10, GLIB_000:47
.= G.edgesBetween(the_Vertices_of G) \ v.edgesInOut() by GLIB_000:107
.= the_Edges_of G \ {e0} by A12, GLIB_000:34;
A16: H is Subgraph of G2
proof
the_Vertices_of H misses {v} by A11, ZFMISC_1:50;
then the_Vertices_of H c= the_Vertices_of G \ {v} by XBOOLE_1:86;
then A17: the_Vertices_of H c= the_Vertices_of G2 by A10, GLIB_000:47;
not e0 in the_Edges_of H
proof
assume A18: e0 in the_Edges_of H;
e0 in v.edgesInOut() by A12, TARSKI:def 1;
then per cases by GLIB_000:61;
suppose (the_Source_of G).e0 = v;
then (the_Source_of H).e0 = v by A18, GLIB_000:def 32;
hence contradiction by A11, A18, FUNCT_2:5;
end;
suppose (the_Target_of G).e0 = v;
then (the_Target_of H).e0 = v by A18, GLIB_000:def 32;
hence contradiction by A11, A18, FUNCT_2:5;
end;
end;
then the_Edges_of H misses {e0} by ZFMISC_1:50;
hence thesis by A15, A17, GLIB_000:44, XBOOLE_1:86;
end;
consider p being non empty _finite Tree-like Graph-yielding FinSequence
such that
A19: p.1 == H & p.len p = G2 & len p = G2.order() - H.order() + 1 and
A20: for n being Element of dom p st n <= len p - 1
ex v1,v2 being Vertex of G2, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of G2 \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n))
by A6, A14, A16, A10, A11;
reconsider q = p ^ <* G *>
as non empty _finite Tree-like Graph-yielding FinSequence;
take q;
1 in dom p by FINSEQ_5:6;
hence q.1 == H by A19, FINSEQ_1:def 7;
A21: len q = len p + len <* G *> by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:40;
hence A22: q.len q = G by FINSEQ_1:42;
thus len q = G.order() - H.order() + 1 by A13, A19, A21;
let n be Element of dom q;
assume n <= len q - 1;
then per cases by Lm12;
suppose A23: n = len q - 1;
then A24: q.(n+1) = G by A22;
1 <= n by FINSEQ_3:25;
then n in dom p by A21, A23, FINSEQ_3:25;
then A27: q.n = G2 by A19, A21, A23, FINSEQ_1:def 7;
A28: e0 in v.edgesInOut() by A12, TARSKI:def 1;
then A29: e0 in the_Edges_of G;
e0 in {e0} by TARSKI:def 1;
then A30: not e0 in the_Edges_of q.n by A15, A27, XBOOLE_0:def 5;
v in {v} by TARSKI:def 1;
then not v in the_Vertices_of G \ {v} by XBOOLE_0:def 5;
then A31: not v in the_Vertices_of q.n by A10, A27, GLIB_000:47;
v.adj(e0) <> v by A12, A28, GLIB_000:67;
then not v.adj(e0) in {v} by TARSKI:def 1;
then v.adj(e0) in the_Vertices_of G \ {v} by XBOOLE_0:def 5;
then A32: v.adj(e0) in the_Vertices_of q.n by A10, A27, GLIB_000:47;
per cases by A10, A12, Th38;
suppose A33: G is addAdjVertex of G2, v.adj(e0), e0, v;
take v.adj(e0), v, e0;
thus q.(n+1) is addAdjVertex of q.n, v.adj(e0), e0, v by A24, A27, A33;
thus thesis by A29, A30, A31, A32, XBOOLE_0:def 5;
end;
suppose A34: G is addAdjVertex of G2, v, e0, v.adj(e0);
take v, v.adj(e0), e0;
thus q.(n+1) is addAdjVertex of q.n, v, e0, v.adj(e0) by A24, A27, A34;
thus thesis by A29, A30, A31, A32, XBOOLE_0:def 5;
end;
end;
suppose A35: n <= len p - 1;
then A36: n+0 <= len p - 1 + 1 by XREAL_1:7;
1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A36, FINSEQ_3:25;
consider v1,v2 being Vertex of G2, e being object
such that A37: p.(m+1) is addAdjVertex of p.m,v1,e,v2 &
e in the_Edges_of G2 \ the_Edges_of p.m &
((v1 in the_Vertices_of p.m & not v2 in the_Vertices_of p.m) or
(not v1 in the_Vertices_of p.m & v2 in the_Vertices_of p.m))
by A20, A35;
1+0 <= n+1 & n+1 <= len p - 1 + 1 by A35, XREAL_1:6;
then n+1 in dom p by FINSEQ_3:25;
then A38: q.(n+1) = p.(m+1) by FINSEQ_1:def 7;
A39: q.n = p.m by FINSEQ_1:def 7;
the_Vertices_of G2 c= the_Vertices_of G;
then reconsider v1,v2 as Vertex of G by TARSKI:def 3;
take v1,v2,e;
the_Edges_of G2 \ the_Edges_of p.m c= the_Edges_of G \ the_Edges_of p.m
by XBOOLE_1:33;
hence thesis by A37, A38, A39;
end;
end;
A40: for k being Nat holds P[k] from NAT_1:sch 2(A1,A5);
let G be _finite Tree-like _Graph;
let H be connected Subgraph of G;
G.order() - H.order() is Nat by GLIB_000:75, NAT_1:21;
hence thesis by A40;
end;
:: finite trees can be finitely constructed with addAdjVertex only
theorem Th72:
for G being _finite Tree-like _Graph
ex p being non empty _finite Tree-like Graph-yielding FinSequence
st p.1 is _trivial edgeless & p.len p = G & len p = G.order() &
for n being Element of dom p st n <= len p - 1
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n))
proof
let G be _finite Tree-like _Graph;
set H = the _trivial Subgraph of G;
consider p being non empty _finite Tree-like Graph-yielding FinSequence
such that A1: p.1 == H & p.len p = G & len p = G.order() - H.order() +1 and
A2: for n being Element of dom p st n <= len p - 1
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n)) by Th71;
take p;
thus p.1 is _trivial edgeless by A1, Th52, GLIB_000:89;
thus p.len p = G by A1;
thus len p = G.order() - 1 + 1 by A1, GLIB_000:26 .= G.order();
thus thesis by A2;
end;
scheme
FinTrees { P[_finite _Graph] } :
for G being _finite Tree-like _Graph holds P[G]
provided
A1: for G being _trivial edgeless _Graph holds P[G] and
A2: for G2 being _finite Tree-like _Graph
for v being Vertex of G2, e, w being object
st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & P[G2]
holds (for G1 being addAdjVertex of G2,v,e,w holds P[G1]) &
(for G1 being addAdjVertex of G2,w,e,v holds P[G1])
proof
let G be _finite Tree-like _Graph;
consider p being non empty _finite Tree-like Graph-yielding FinSequence
such that A3: p.1 is _trivial edgeless & p.len p = G & len p = G.order()
and A4: for n being Element of dom p st n <= len p - 1
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n)) by Th72;
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & P[p.k];
A5: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus 1 = k;
thus P[p.k] by A1, A3;
end;
A6: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A7: Q[m];
assume A8: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A8, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A8, XREAL_1:13;
then consider k0 being Element of dom p such that
A9: m = k0 & P[p.k0] by A7;
m+1-1 <= len p - 1 by A8, XREAL_1:9;
then consider v1,v2 being Vertex of G, e being object such that
A10: p.(k0+1) is addAdjVertex of p.k0,v1,e,v2 and
A11: e in the_Edges_of G \ the_Edges_of p.k0 and
A12: (v1 in the_Vertices_of p.k0 & not v2 in the_Vertices_of p.k0) or
(not v1 in the_Vertices_of p.k0 & v2 in the_Vertices_of p.k0)
by A4, A9;
A13: not e in the_Edges_of p.k0 by A11, XBOOLE_0:def 5;
per cases by A12;
suppose v1 in the_Vertices_of p.k0 & not v2 in the_Vertices_of p.k0;
hence thesis by A2, A9, A10, A13;
end;
suppose not v1 in the_Vertices_of p.k0 & v2 in the_Vertices_of p.k0;
hence thesis by A2, A9, A10, A13;
end;
end;
A14: for m being non zero Nat holds Q[m] from NAT_1:sch 10(A5,A6);
consider k being Element of dom p such that
A15: len p = k & P[p.k] by A14;
thus thesis by A3, A15;
end;
theorem
for p being non empty Graph-yielding FinSequence
st p.1 is Tree-like &
for n being Element of dom p st n <= len p - 1
ex v1,e,v2 being object st p.(n+1) is addAdjVertex of p.n,v1,e,v2
holds p.len p is Tree-like
proof
let p be non empty Graph-yielding FinSequence;
assume that A1: p.1 is Tree-like and
A2: for n being Element of dom p st n <= len p - 1 holds
ex v1,e,v2 being object st p.(n+1) is addAdjVertex of p.n,v1,e,v2;
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & p.k is Tree-like;
A3: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus thesis by A1;
end;
A4: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A5: Q[m];
assume A6: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A6, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A6, XREAL_1:13;
then consider k0 being Element of dom p such that
A7: m = k0 & p.k0 is Tree-like by A5;
m+1-1 <= len p - 1 by A6, XREAL_1:9;
then consider v1,e,v2 being object such that
A8: p.(k0+1) is addAdjVertex of p.k0,v1,e,v2 by A2, A7;
thus thesis by A7, A8;
end;
A9: for m being non zero Nat holds Q[m] from NAT_1:sch 10(A3,A4);
consider k being Element of dom p such that
A10: len p = k & p.k is Tree-like by A9;
thus thesis by A10;
end;
:: finite connected graphs can be constructed with addAdjVertex and addEdge
theorem Th74:
for G being _finite connected _Graph
ex p being non empty _finite connected Graph-yielding FinSequence
st p.1 is _trivial edgeless & p.len p = G & len p = G.size() + 1 &
for n being Element of dom p st n <= len p - 1 holds
(ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n)) ) or
(ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n)
proof
let G be _finite connected _Graph;
per cases;
suppose A1: G is non acyclic;
set H = the spanning Tree-like Subgraph of G;
consider p being non empty _finite Tree-like Graph-yielding FinSequence
such that
A2: p.1 is _trivial edgeless & p.len p = H & len p = H.order() and
A3: for n being Element of dom p st n <= len p - 1
ex v1,v2 being Vertex of H, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of H \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n))
by Th72;
consider q being non empty _finite connected Graph-yielding FinSequence
such that
A4: q.1 == H & q.len q = G & len q = G.size() - H.size() + 1 and
A5: for n being Element of dom q st n <= len q - 1 holds
ex v1,v2 being Vertex of G, e being object
st q.(n+1) is addEdge of q.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of q.n &
v1 in the_Vertices_of q.n & v2 in the_Vertices_of q.n by Th66;
reconsider r = p ^' q
as non empty _finite connected Graph-yielding FinSequence;
take r;1 <= len p by FINSEQ_1:20;
hence r.1 is _trivial edgeless by A2, FINSEQ_6:140;
A6: 1 < len q
proof
assume not 1 < len q;
then len q <= 1 & 1 <= len q by FINSEQ_1:20;
then G == H by A4, XXREAL_0:1;
hence contradiction by A1, GLIB_002:44;
end;
hence r.len r = G by A4, FINSEQ_6:142;
len r + 1 = len p + len q by FINSEQ_6:139
.= H.order() + G.size() - H.size() + 1 by A2, A4
.= H.size() + 1 + G.size() - H.size() + 1 by GLIB_002:46
.= G.size() + 1 + 1;
hence len r = G.size() + 1;
let n be Element of dom r;
assume A7: n <= len r - 1;
n < len p or n = len p or n > len p by XXREAL_0:1;
then n+1 <= len p or n = len p or n > len p by INT_1:7;
then n+1-1 <= len p - 1 or n = len p or n > len p by XREAL_1:9;
then per cases;
suppose A8: n <= len p - 1;
then A9: n+0 <= len p - 1+1 & n+1 <= len p -1+1 by XREAL_1:7;
A10: 1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A9, FINSEQ_3:25;
A11: r.n = p.m by A9, A10, FINSEQ_6:140;
1+0 <= n+1 by XREAL_1:7;
then A12: r.(n+1) = p.(m+1) by A9, FINSEQ_6:140;
now
consider v1,v2 being Vertex of H, e being object such that
A13: p.(m+1) is addAdjVertex of p.m,v1,e,v2 &
e in the_Edges_of H \ the_Edges_of p.m &
((v1 in the_Vertices_of p.m & not v2 in the_Vertices_of p.m) or
(not v1 in the_Vertices_of p.m & v2 in the_Vertices_of p.m))
by A3, A8;
the_Vertices_of H c= the_Vertices_of G;
then reconsider v1, v2 as Vertex of G by TARSKI:def 3;
take v1,v2,e;
the_Edges_of H \ the_Edges_of p.m c= the_Edges_of G \ the_Edges_of p.m
by XBOOLE_1:33;
hence r.(n+1) is addAdjVertex of r.n, v1,e,v2 &
e in the_Edges_of G \ the_Edges_of r.n &
((v1 in the_Vertices_of r.n & not v2 in the_Vertices_of r.n) or
(not v1 in the_Vertices_of r.n & v2 in the_Vertices_of r.n))
by A11, A12, A13;
end;
hence thesis;
end;
suppose A14: n = len p;
then 1 <= n & n <= len p by FINSEQ_1:20;
then A15: r.n = H by A2, A14, FINSEQ_6:140;
reconsider m = 1 as Element of dom q by A6, FINSEQ_3:25;
A16: r.(n+1) = q.(m+1) by A14, A6, FINSEQ_6:141;
now
m+1 <= len q by A6, INT_1:7;
then m+1-1 <= len q - 1 by XREAL_1:9;
then consider v1,v2 being Vertex of G, e being object such that
A17: q.(m+1) is addEdge of q.m,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of q.m &
v1 in the_Vertices_of q.m & v2 in the_Vertices_of q.m by A5;
take v1,v2,e;
thus r.(n+1) is addEdge of r.n,v1,e,v2 by A4, A15, A16, A17, Th36;
thus e in the_Edges_of G \ the_Edges_of r.n &
v1 in the_Vertices_of r.n & v2 in the_Vertices_of r.n
by A4, A15, A17, GLIB_000:def 34;
end;
hence thesis;
end;
suppose A18: n > len p;
then reconsider n1 = n-1 as Nat by NAT_1:20;
n1+1 = n;
then len p <= n1 by A18, NAT_1:13;
then reconsider k1 = n1 - len p as Nat by NAT_1:21;
set k = k1+1;
A19: k+1 < len q
proof
assume len q <= k + 1;
then len q + len p <= k + 1 + len p by XREAL_1:6;
then len r + 1 <= n + 1 by FINSEQ_6:139;
then len r - 1 <= n - 1 by XREAL_1:6, XREAL_1:9;
then n <= n-1 by A7, XXREAL_0:2;
then n-n <= n-1-n by XREAL_1:9;
then 0 <= -1;
hence contradiction;
end;
then k+1-1 < len q - 0 by XREAL_1:14;
then r.(len p + k) = q.(k+1) by NAT_1:14, FINSEQ_6:141;
then A20: r.n = q.(k+1);
1+0 <= k+1 by XREAL_1:7;
then r.(len p +(k+1)) = q.((k+1)+1) by A19, FINSEQ_6:141;
then A21: r.(n+1) = q.((k+1)+1);
1+0 <= k+1 & k+1 <= len q by A19, XREAL_1:7;
then reconsider m=k+1 as Element of dom q by FINSEQ_3:25;
now
m+1 <= len q by A19, INT_1:7;
then m+1-1 <= len q - 1 by XREAL_1:9;
then consider v1,v2 being Vertex of G, e being object such that
A22: q.(m+1) is addEdge of q.m,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of q.m &
v1 in the_Vertices_of q.m & v2 in the_Vertices_of q.m by A5;
take v1,v2,e;
thus r.(n+1) is addEdge of r.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of r.n &
v1 in the_Vertices_of r.n & v2 in the_Vertices_of r.n
by A20, A21, A22;
end;
hence thesis;
end;
end;
suppose A23: G is acyclic;
then consider p being non empty _finite Tree-like Graph-yielding FinSequence
such that
A24: p.1 is _trivial edgeless & p.len p = G & len p = G.order() and
A25: for n being Element of dom p st n <= len p - 1
ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n))
by Th72;
take p;
thus thesis by A24, A25, A23, GLIB_002:46;
end;
end;
scheme
FinConnectedGraphs { P[_finite _Graph] } :
for G being _finite connected _Graph holds P[G]
provided
A1: for G being _trivial edgeless _Graph holds P[G] and
A2: for G2 being _finite connected _Graph
for v being Vertex of G2, e, w being object
st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & P[G2]
holds (for G1 being addAdjVertex of G2,v,e,w holds P[G1]) &
(for G1 being addAdjVertex of G2,w,e,v holds P[G1]) and
A3: for G2 being _finite connected _Graph
for v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
st not e in the_Edges_of G2 & P[G2] holds P[G1]
proof
let G be _finite connected _Graph;
consider p being non empty _finite connected Graph-yielding FinSequence
such that
A4: p.1 is _trivial edgeless & p.len p = G & len p = G.size() + 1
and A5: for n being Element of dom p st n <= len p - 1 holds
(ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addAdjVertex of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
((v1 in the_Vertices_of p.n & not v2 in the_Vertices_of p.n) or
(not v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n)) ) or
(ex v1,v2 being Vertex of G, e being object
st p.(n+1) is addEdge of p.n,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.n &
v1 in the_Vertices_of p.n & v2 in the_Vertices_of p.n) by Th74;
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & P[p.k];
A6: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus 1 = k;
thus P[p.k] by A1, A4;
end;
A7: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A8: Q[m];
assume A9: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A9, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A9, XREAL_1:13;
then consider k0 being Element of dom p such that
A10: m = k0 & P[p.k0] by A8;
m+1-1 <= len p - 1 by A9, XREAL_1:9;
then per cases by A5, A10;
suppose ex v1,v2 being Vertex of G, e being object
st p.(k0+1) is addAdjVertex of p.k0,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.k0 &
((v1 in the_Vertices_of p.k0 & not v2 in the_Vertices_of p.k0) or
(not v1 in the_Vertices_of p.k0 & v2 in the_Vertices_of p.k0));
then consider v1,v2 being Vertex of G, e being object such that
A11: p.(k0+1) is addAdjVertex of p.k0,v1,e,v2 and
A12: e in the_Edges_of G \ the_Edges_of p.k0 and
A13: (v1 in the_Vertices_of p.k0 & not v2 in the_Vertices_of p.k0) or
(not v1 in the_Vertices_of p.k0 & v2 in the_Vertices_of p.k0);
A14: not e in the_Edges_of p.k0 by A12, XBOOLE_0:def 5;
per cases by A13;
suppose v1 in the_Vertices_of p.k0 & not v2 in the_Vertices_of p.k0;
hence thesis by A2, A10, A11, A14;
end;
suppose not v1 in the_Vertices_of p.k0 & v2 in the_Vertices_of p.k0;
hence thesis by A2, A10, A11, A14;
end;
end;
suppose ex v1,v2 being Vertex of G, e being object
st p.(k0+1) is addEdge of p.k0,v1,e,v2 &
e in the_Edges_of G \ the_Edges_of p.k0 &
v1 in the_Vertices_of p.k0 & v2 in the_Vertices_of p.k0;
then consider v1,v2 being Vertex of G, e being object such that
A15: p.(k0+1) is addEdge of p.k0,v1,e,v2 and
A16: e in the_Edges_of G \ the_Edges_of p.k0 &
v1 in the_Vertices_of p.k0 & v2 in the_Vertices_of p.k0;
reconsider v1, v2 as Vertex of p.k0 by A16;
A17: not e in the_Edges_of p.k0 by A16, XBOOLE_0:def 5;
p.k is addEdge of p.k0,v1,e,v2 by A10, A15;
hence thesis by A3, A10, A17;
end;
end;
for m being non zero Nat holds Q[m] from NAT_1:sch 10(A6,A7); then
ex k being Element of dom p st len p = k & P[p.k];
hence thesis by A4;
end;
theorem
for p being non empty Graph-yielding FinSequence
st p.1 is connected &
for n being Element of dom p st n <= len p - 1
ex v1,e,v2 being object st p.(n+1) is addAdjVertex of p.n,v1,e,v2
or p.(n+1) is addEdge of p.n,v1,e,v2
holds p.len p is connected
proof
let p be non empty Graph-yielding FinSequence;
assume that A1: p.1 is connected and
A2: for n being Element of dom p st n <= len p - 1 holds
ex v1,e,v2 being object st p.(n+1) is addAdjVertex of p.n,v1,e,v2
or p.(n+1) is addEdge of p.n,v1,e,v2;
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & p.k is connected;
A3: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus thesis by A1;
end;
A4: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A5: Q[m];
assume A6: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A6, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A6, XREAL_1:13;
then consider k0 being Element of dom p such that
A7: m = k0 & p.k0 is connected by A5;
m+1-1 <= len p - 1 by A6, XREAL_1:9;
then consider v1,e,v2 being object such that
A8: p.(k0+1) is addAdjVertex of p.k0,v1,e,v2 or
p.(k0+1) is addEdge of p.k0,v1,e,v2 by A2, A7;
thus thesis by A7, A8;
end;
for m being non zero Nat holds Q[m] from NAT_1:sch 10(A3,A4); then
ex k being Element of dom p st len p = k & p.k is connected;
hence thesis;
end;
theorem Th76:
for G2 being _Graph, v being object
for V1 being set, V2 being finite set
for G1 being addAdjVertexAll of G2, v, V1 \/ V2
st V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
V1 misses V2
ex p being non empty Graph-yielding FinSequence
st p.1 = G2 & p.len p = G1 & len p = card V2 + 2 &
p.2 is addAdjVertexAll of G2, v, V1 &
for n being Element of dom p st 2 <= n & n <= len p - 1 holds
ex w being Vertex of G2, e being object
st e in the_Edges_of G1 \ the_Edges_of p.n &
(p.(n+1) is addEdge of p.n,v,e,w or p.(n+1) is addEdge of p.n,w,e,v)
proof
let G2 be _Graph, v be object, V1 be set;
defpred P[Nat] means for V2 being finite set
for G1 being addAdjVertexAll of G2, v, V1 \/ V2
st V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 &
V1 misses V2 & card V2 = $1
ex p being non empty Graph-yielding FinSequence
st p.1 = G2 & p.len p = G1 & len p = card V2 + 2 &
p.2 is addAdjVertexAll of G2, v, V1 &
for n being Element of dom p st 2 <= n & n <= len p - 1 holds
ex w being Vertex of G2, e being object
st e in the_Edges_of G1 \ the_Edges_of p.n &
(p.(n+1) is addEdge of p.n,v,e,w or p.(n+1) is addEdge of p.n,w,e,v);
A1: P[0]
proof
let V2 be finite set;
let G1 be addAdjVertexAll of G2, v, V1 \/ V2;
assume that
V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A2: V1 misses V2 & card V2 = 0;
reconsider p = <* G2, G1 *> as non empty Graph-yielding FinSequence;
take p;
thus p.1 = G2;
thus p.len p = p.2 by FINSEQ_1:44
.= G1;
thus len p = card V2 + 2 by A2, FINSEQ_1:44;
V2 = {} by A2;
hence p.2 is addAdjVertexAll of G2, v, V1;
let n be Element of dom p;
assume 2 <= n & n <= len p - 1;
then 2 <= n & n <= 2 - 1 by FINSEQ_1:44;
hence thesis by XXREAL_0:2; :: by contradiction
end;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
let V2 be finite set, G1 be addAdjVertexAll of G2, v, V1 \/ V2;
assume that
A5: V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 and
A6: V1 misses V2 & card V2 = k+1;
set v0 = the Element of V2;
set V3 = V2 \ {v0};
A7: V2 is non empty by A6;
A8: V2 = V3 \/ {v0} by A7, ZFMISC_1:116;
V1 \/ V3 c= V1 \/ V2 by XBOOLE_1:9;
then A9: V1 \/ V3 c= the_Vertices_of G2 by A5, XBOOLE_1:1;
A10: V1 misses V3 by A6, XBOOLE_1:64;
v0 in {v0} by TARSKI:def 1;
then A11: not v0 in V3 by XBOOLE_0:def 5;
then A12: card V2 = card V3 + 1 by A8, CARD_2:41;
then A13: card V3 = k by A6;
v0 in V1 \/ V2 by A7, XBOOLE_1:7, TARSKI:def 3;
then reconsider v0 as Vertex of G2 by A5;
V1 /\ V2 = {} by A6, XBOOLE_0:def 7;
then not v0 in V1 by A7, XBOOLE_0:def 4;
then A14: not v0 in V1 \/ V3 by A11, XBOOLE_0:def 3;
G1 is addAdjVertexAll of G2,v,(V1 \/ V3) \/ {v0} by A8, XBOOLE_1:4;
then consider G3 being addAdjVertexAll of G2,v,V1 \/ V3, e being object
such that A15: not e in the_Edges_of G3 and
A16: G1 is addEdge of G3,v,e,v0 or G1 is addEdge of G3,v0,e,v
by A5, A9, A14, Lm9;
consider p being non empty Graph-yielding FinSequence such that
A17: p.1 = G2 & p.len p = G3 & len p = card V3 + 2 &
p.2 is addAdjVertexAll of G2, v, V1 and
A18: for n being Element of dom p st 2 <= n & n <= len p - 1 holds
ex w being Vertex of G2, e being object
st e in the_Edges_of G3 \ the_Edges_of p.n &
(p.(n+1) is addEdge of p.n,v,e,w or p.(n+1) is addEdge of p.n,w,e,v)
by A4, A5, A9, A10, A13;
reconsider q = p ^ <* G1 *> as non empty Graph-yielding FinSequence;
take q;
1 in dom p by FINSEQ_5:6;
hence q.1 = G2 by A17, FINSEQ_1:def 7;
A19: len q = len p + len <* G1 *> by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:40;
hence A20: q.len q = G1 by FINSEQ_1:42;
thus len q = card V2 + 2 by A12, A17, A19;
2 + card V3 - card V3 <= len p - 0 by A17, XREAL_1:13;
then 2 in dom p by FINSEQ_3:25;
hence q.2 is addAdjVertexAll of G2, v, V1 by A17, FINSEQ_1:def 7;
let n be Element of dom q;
assume A21: 2 <= n & n <= len q - 1;
then per cases by Lm12;
suppose A22: n = len q - 1;
then A23: q.(n+1) = G1 by A20;
1 <= n by FINSEQ_3:25;
then n in dom p by A19, A22, FINSEQ_3:25;
then A26: q.n = G3 by A17, A19, A22, FINSEQ_1:def 7;
v0 in the_Vertices_of G3 & v in the_Vertices_of G3
proof
A27: v0 in the_Vertices_of G2;
the_Vertices_of G2 c= the_Vertices_of G3 by GLIB_006:def 9;
hence v0 in the_Vertices_of G3 by A27;
v is Vertex of G3 by A5, A9, GLIB_007:50;
hence v in the_Vertices_of G3;
end;
then e DJoins v,v0,G1 or e DJoins v0,v,G1 by A15, A16, GLIB_006:105;
then A28: e in the_Edges_of G1 by GLIB_000:def 14;
take v0, e;
thus e in the_Edges_of G1 \ the_Edges_of q.n
by A15, A26, A28, XBOOLE_0:def 5;
thus q.(n+1) is addEdge of q.n,v,e,v0 or q.(n+1) is addEdge of q.n,v0,e,v
by A16, A23, A26;
end;
suppose A29: n <= len p - 1;
then A30: n+0 <= len p - 1 + 1 by XREAL_1:7;
1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A30, FINSEQ_3:25;
consider w being Vertex of G2, e being object such that
A31: e in the_Edges_of G3 \ the_Edges_of p.m &
(p.(m+1) is addEdge of p.m,v,e,w or p.(m+1) is addEdge of p.m,w,e,v)
by A18, A21, A29;
1+0 <= n+1 & n+1 <= len p - 1 + 1 by A29, XREAL_1:6;
then n+1 in dom p by FINSEQ_3:25;
then A32: q.(n+1) = p.(m+1) by FINSEQ_1:def 7;
A33: q.n = p.m by FINSEQ_1:def 7;
the_Edges_of G3 c= the_Edges_of G1 by A16, GLIB_006:def 9;
then A34: the_Edges_of G3 \ the_Edges_of p.m
c= the_Edges_of G1 \ the_Edges_of p.m by XBOOLE_1:33;
take w,e;
thus thesis by A31, A32, A33, A34;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem
for G2 being _Graph, v being object
for V being finite set, G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
ex p being non empty Graph-yielding FinSequence
st p.1 = G2 & p.len p = G1 & len p = card V + 2 & p.2 is addVertex of G2,v &
for n being Element of dom p st 2 <= n & n <= len p - 1 holds
ex w being Vertex of G2, e being object
st e in the_Edges_of G1 \ the_Edges_of p.n &
(p.(n+1) is addEdge of p.n,v,e,w or p.(n+1) is addEdge of p.n,w,e,v)
proof
let G2 be _Graph, v be object, V be finite set;
let G1 be addAdjVertexAll of G2, v, V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
V = V \/ {} & {} misses V by XBOOLE_1:65;
then consider p being non empty Graph-yielding FinSequence such that
A2: p.1 = G2 & p.len p = G1 & len p = card V + 2 and
A3: p.2 is addAdjVertexAll of G2, v, {} and
A4: for n being Element of dom p st 2 <= n & n <= len p - 1 holds
ex w being Vertex of G2, e being object
st e in the_Edges_of G1 \ the_Edges_of p.n &
(p.(n+1) is addEdge of p.n,v,e,w or p.(n+1) is addEdge of p.n,w,e,v)
by A1, Th76;
take p;
thus p.1 = G2 & p.len p = G1 & len p = card V + 2 by A2;
thus p.2 is addVertex of G2, v by A3, GLIB_007:55;
thus thesis by A4;
end;
theorem
for G2 being _Graph, v being object
for V being non empty finite set, G1 being addAdjVertexAll of G2, v, V
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
ex p being non empty Graph-yielding FinSequence
st p.1 = G2 & p.len p = G1 & len p = card V + 1 &
(ex w being Vertex of G2, e being object
st e in the_Edges_of G1 \ the_Edges_of G2 &
(p.2 is addAdjVertex of G2,v,e,w or p.2 is addAdjVertex of G2,w,e,v)) &
for n being Element of dom p st 2 <= n & n <= len p - 1 holds
ex w being Vertex of G2, e being object
st e in the_Edges_of G1 \ the_Edges_of p.n &
(p.(n+1) is addEdge of p.n,v,e,w or p.(n+1) is addEdge of p.n,w,e,v)
proof
let G2 be _Graph, v be object, V be non empty finite set;
let G1 be addAdjVertexAll of G2, v, V;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
set v0 = the Element of V;
set V0 = V \ {v0};
v0 in {v0} by TARSKI:def 1;
then not v0 in V0 by XBOOLE_0:def 5;
then V = V0 \/ {v0} & {v0} misses V0 by ZFMISC_1:50, ZFMISC_1:116;
then consider p being non empty Graph-yielding FinSequence such that
A2: p.1 = G2 & p.len p = G1 & len p = card V0 + 2 and
A3: p.2 is addAdjVertexAll of G2, v, {v0} and
A4: for n being Element of dom p st 2 <= n & n <= len p - 1 holds
ex w being Vertex of G2, e being object
st e in the_Edges_of G1 \ the_Edges_of p.n &
(p.(n+1) is addEdge of p.n,v,e,w or p.(n+1) is addEdge of p.n,w,e,v)
by A1, Th76;
take p;
thus p.1 = G2 & p.len p = G1 by A2;
thus len p = card V - card {v0} + 2 by A2, CARD_2:44
.= card V - 1 + 2 by CARD_1:30
.= card V + 1;
hereby
reconsider w = v0 as Vertex of G2 by A1, TARSKI:def 3;
consider e being object such that
A5: not e in the_Edges_of G2 and
A6: p.2 is addAdjVertex of G2,v,e,w or p.2 is addAdjVertex of G2,w,e,v
by A1, A3, GLIB_007:56;
A7: e in the_Edges_of G1
proof
defpred P[Nat] means $1 + 2 <= len p implies ex k being Element of dom p
st k = $1 + 2 & e in the_Edges_of p.k;
A8: P[0]
proof
assume 0 + 2 <= len p;
card V0 + 2 - card V0 <= len p - 0 by A2, XREAL_1:10;
then reconsider k = 2 as Element of dom p by FINSEQ_3:25;
take k;
thus k = 0 + 2;
per cases by A6;
suppose p.k is addAdjVertex of G2,v,e,w;
then e Joins v,w,p.k by A1, A5, GLIB_006:132;
hence e in the_Edges_of p.k by GLIB_000:def 13;
end;
suppose p.k is addAdjVertex of G2,w,e,v;
then e Joins w,v,p.k by A1, A5, GLIB_006:131;
hence e in the_Edges_of p.k by GLIB_000:def 13;
end;
end;
A9: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume A10: P[m];
assume A11: m+1 + 2 <= len p;
then m+1 + 2 - 1 <= len p - 0 by XREAL_1:13;
then consider k0 being Element of dom p such that
A12: k0 = m + 2 & e in the_Edges_of p.k0 by A10;
1+0 <= m+1+2 by XREAL_1:7;
then reconsider k = m+1 + 2 as Element of dom p by A11, FINSEQ_3:25;
take k;
thus k = m+1 + 2;
A13: 0+(1+1) <= m+(1+1) by XREAL_1:7;
m+1 + 2 - 1 <= len p - 1 by A11, XREAL_1:9;
then consider u being Vertex of G2, f being object
such that f in the_Edges_of G1 \ the_Edges_of p.k0 and
A14: (p.(k0+1) is addEdge of p.k0,v,f,u or
p.(k0+1) is addEdge of p.k0,u,f,v) by A4, A12, A13;
the_Edges_of p.k0 c= the_Edges_of p.k by A12, A14, GLIB_006:def 9;
hence thesis by A12;
end;
A15: for m being Nat holds P[m] from NAT_1:sch 2(A8,A9);
reconsider m = len p - 2 as Nat by A2;
consider k being Element of dom p such that
A16: k = m + 2 & e in the_Edges_of p.k by A15;
thus thesis by A2, A16;
end;
take w,e;
thus e in the_Edges_of G1 \ the_Edges_of G2 &
(p.2 is addAdjVertex of G2,v,e,w or p.2 is addAdjVertex of G2,w,e,v)
by A5, A6, A7, XBOOLE_0:def 5;
end;
thus thesis by A4;
end;
theorem Th79:
for G being _finite simple _Graph
for W being set, H being inducedSubgraph of G, W
ex p being non empty _finite simple Graph-yielding FinSequence
st p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 &
for n being Element of dom p st n <= len p - 1
ex v being object, V being finite set
st v in the_Vertices_of G \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V
proof
defpred P[Nat] means for G being _finite simple _Graph
for W being set, H being inducedSubgraph of G, W
st G.order() - H.order() = $1
ex p being non empty _finite simple Graph-yielding FinSequence
st p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 &
for n being Element of dom p st n <= len p - 1
ex v being object, V being finite set
st v in the_Vertices_of G \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V;
A1: P[0]
proof
let G be _finite simple _Graph;
let W be set, H be inducedSubgraph of G, W;
assume A2: G.order() - H.order() = 0;
then H is spanning by GLIB_000:117;
then A3: G == H by GLIB_000:120;
set p = <* G *>;
take p;
thus p.1 == H by A3;
thus p.len p = p.1 by FINSEQ_1:40
.= G;
thus len p = G.order() - H.order() + 1 by A2, FINSEQ_1:40;
let n be Element of dom p;
1 <= n & n <= len p by FINSEQ_3:25;
then 1 <= n & n <= 1 by FINSEQ_1:40;
then A4: n = 1 by XXREAL_0:1;
assume n <= len p - 1;
then n <= 1 - 1 by FINSEQ_1:40;
hence thesis by A4; :: by contradiction
end;
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
let G be _finite simple _Graph;
let W be set, H be inducedSubgraph of G, W;
assume A7: G.order() - H.order() = k+1;
A8: the_Vertices_of G \ the_Vertices_of H <> {}
proof
assume the_Vertices_of G \ the_Vertices_of H = {};
then the_Vertices_of G c= the_Vertices_of H by XBOOLE_1:37;
then A9: the_Vertices_of G = the_Vertices_of H by XBOOLE_0:def 10;
G.order() = card the_Vertices_of G by GLIB_000:def 24
.= H.order() by A9, GLIB_000:def 24;
then 0 = k+1 by A7;
hence contradiction;
end;
set v0 = the Element of the_Vertices_of G \ the_Vertices_of H;
v0 in the_Vertices_of G \ the_Vertices_of H by A8;
then reconsider v0 as Vertex of G;
set G2 = the removeVertex of G,v0;
A10: the_Vertices_of G <> the_Vertices_of H by A8, XBOOLE_1:37;
then A11: G is non _trivial by GLIB_000:121, GLIB_000:def 33;
then A12: G2.order() + 1 = G.order() by GLIB_000:48;
then A13: G2.order() - H.order() = k by A7;
A14: the_Edges_of G2
= G.edgesBetween(the_Vertices_of G \ {v0}) by A11, GLIB_000:47
.= G.edgesBetween(the_Vertices_of G) \ v0.edgesInOut() by GLIB_000:107
.= the_Edges_of G \ v0.edgesInOut() by GLIB_000:34;
the_Vertices_of H c= the_Vertices_of G2 & the_Edges_of H c= the_Edges_of G2
proof
A15: not v0 in the_Vertices_of H by A8, XBOOLE_0:def 5;
the_Vertices_of H c= the_Vertices_of G \ {v0} by A15, ZFMISC_1:34;
hence the_Vertices_of H c= the_Vertices_of G2 by A11, GLIB_000:47;
the_Edges_of H /\ v0.edgesInOut() = {}
proof
assume A16: the_Edges_of H /\ v0.edgesInOut() <> {};
set e = the Element of the_Edges_of H /\ v0.edgesInOut();
A17: e in the_Edges_of H & e in v0.edgesInOut() by A16, XBOOLE_0:def 4;
then per cases by GLIB_000:61;
suppose (the_Source_of G).e = v0;
then (the_Source_of H).e = v0 by A17, GLIB_000:def 32;
hence contradiction by A15, A17, FUNCT_2:5;
end;
suppose (the_Target_of G).e = v0;
then (the_Target_of H).e = v0 by A17, GLIB_000:def 32;
hence contradiction by A15, A17, FUNCT_2:5;
end;
end;
then the_Edges_of H = the_Edges_of H \ v0.edgesInOut()
by XBOOLE_0:def 7, XBOOLE_1:83;
hence thesis by A14, XBOOLE_1:33;
end;
then A18: H is Subgraph of G2 by GLIB_000:44;
H is inducedSubgraph of G2, W
proof
H != G by A10, GLIB_000:def 34;
then W is non empty Subset of the_Vertices_of G by GLIB_000:def 37;
then A19: the_Vertices_of H = W & the_Edges_of H = G.edgesBetween(W)
by GLIB_000:def 37;
then A20: W is non empty Subset of the_Vertices_of G2
by A18, GLIB_000:def 32;
for x being object
st x in G.edgesBetween(W) holds x in G2.edgesBetween(W)
proof
let x be object;
assume A21: x in G.edgesBetween(W);
reconsider e = x as set by TARSKI:1;
A22: (the_Source_of G).e in W & (the_Target_of G).e in W
by A21, GLIB_000:31;
A23: e in the_Edges_of G2
proof
assume not e in the_Edges_of G2;
then e in v0.edgesInOut() by A14, A21, XBOOLE_0:def 5;
then per cases by GLIB_000:61;
suppose (the_Source_of G).e = v0;
hence contradiction by A8, A19, A22, XBOOLE_0:def 5;
end;
suppose (the_Target_of G).e = v0;
hence contradiction by A8, A19, A22, XBOOLE_0:def 5;
end;
end;
then (the_Source_of G2).e = (the_Source_of G).e &
(the_Target_of G2).e = (the_Target_of G).e by GLIB_000:def 32;
hence thesis by A22, A23, GLIB_000:31;
end;
then A24: G.edgesBetween(W) c= G2.edgesBetween(W) by TARSKI:def 3;
G2.edgesBetween(W) c= G.edgesBetween(W) by GLIB_000:76;
then G2.edgesBetween(W) = the_Edges_of H by A19, A24, XBOOLE_0:def 10;
hence thesis by A18, A19, A20, GLIB_000:def 37;
end;
then consider p being non empty _finite simple Graph-yielding FinSequence
such that
A25: p.1 == H & p.len p = G2 & len p = G2.order() - H.order() + 1 and
A26: for n being Element of dom p st n <= len p - 1
ex v being object, V being finite set
st v in the_Vertices_of G2 \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V
by A6, A13;
set q = p ^ <* G *>;
take q;
1 in dom p by FINSEQ_5:6;
hence q.1 == H by A25, FINSEQ_1:def 7;
A27: len q = len p + len <* G *> by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:40;
hence A28: q.len q = G by FINSEQ_1:42;
thus len q = G.order() - H.order() + 1 by A12, A25, A27;
let n be Element of dom q;
assume n <= len q - 1;
then per cases by Lm12;
suppose A29: n = len q - 1;
then A30: q.(n+1) = G by A28;
A31: 1 <= n by FINSEQ_3:25;
A32: n = len p by A27, A29;
then n in dom p by A31, FINSEQ_3:25;
then A33: q.n = G2 by A25, A32, FINSEQ_1:def 7;
reconsider V = v0.allNeighbors() as finite set;
take v0,V;
v0 in {v0} by TARSKI:def 1;
then not v0 in the_Vertices_of G \ {v0} by XBOOLE_0:def 5;
then not v0 in the_Vertices_of G2 by A11, GLIB_000:47;
hence v0 in the_Vertices_of G \ the_Vertices_of q.n
by A33, XBOOLE_0:def 5;
for x being object st x in V holds x in the_Vertices_of G2
proof
let x be object;
assume A34: x in V;
then x <> v0 by GLIB_000:112;
then A35: not x in {v0} by TARSKI:def 1;
x in the_Vertices_of G \ {v0} by A34, A35, XBOOLE_0:def 5;
hence thesis by A11, GLIB_000:47;
end;
hence V c= the_Vertices_of q.n by A33, TARSKI:def 3;
thus q.(n+1) is addAdjVertexAll of q.n,v0,V by A11, A30, A33, Th47;
end;
suppose A36: n <= len p - 1;
then A37: n+0 <= len p - 1 + 1 by XREAL_1:7;
1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A37, FINSEQ_3:25;
consider v being object, V being finite set such that
A38: v in the_Vertices_of G2 \ the_Vertices_of p.m &
V c= the_Vertices_of p.m & p.(m+1) is addAdjVertexAll of p.m,v,V
by A26, A36;
1+0 <= n+1 & n+1 <= len p - 1 + 1 by A36, XREAL_1:6;
then n+1 in dom p by FINSEQ_3:25;
then A39: q.(n+1) = p.(m+1) by FINSEQ_1:def 7;
A40: q.n = p.m by FINSEQ_1:def 7;
take v,V;
the_Vertices_of G2 \ the_Vertices_of p.m
c= the_Vertices_of G \ the_Vertices_of p.m by XBOOLE_1:33;
hence v in the_Vertices_of G \ the_Vertices_of q.n
by A38, A40;
thus thesis by A38, A39, A40;
end;
end;
A41: for k being Nat holds P[k] from NAT_1:sch 2(A1,A5);
let G be _finite simple _Graph;
let W be set, H be inducedSubgraph of G, W;
G.order() - H.order() is Nat by GLIB_000:75, NAT_1:21;
hence thesis by A41;
end;
theorem Th80:
for G being _finite simple _Graph
ex p being non empty _finite simple Graph-yielding FinSequence
st p.1 is _trivial edgeless & p.len p = G & len p = G.order() &
for n being Element of dom p st n <= len p - 1
ex v being object, V being finite set
st v in the_Vertices_of G \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V
proof
let G be _finite simple _Graph;
set v0 = the Vertex of G;
set H = the inducedSubgraph of G,{v0};
consider p being non empty _finite simple Graph-yielding FinSequence
such that
A1: p.1 == H & p.len p = G & len p = G.order() - H.order() + 1 and
A2: for n being Element of dom p st n <= len p - 1
ex v being object, V being finite set
st v in the_Vertices_of G \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V
by Th79;
take p;
thus p.1 is _trivial edgeless by A1, Th52, GLIB_000:89;
thus p.len p = G by A1;
H.order() = 1 by GLIB_000:26;
hence len p = G.order() by A1;
thus thesis by A2;
end;
scheme
FinSimpleGraphs { P[_finite _Graph] } :
for G being _finite simple _Graph holds P[G]
provided
A1: for G being _trivial edgeless _Graph holds P[G] and
A2: for G2 being _finite simple _Graph, v being object, V being finite set
for G1 being addAdjVertexAll of G2,v,V
st not v in the_Vertices_of G2 & V c= the_Vertices_of G2 & P[G2]
holds P[G1]
proof
let G be _finite simple _Graph;
consider p being non empty _finite simple Graph-yielding FinSequence
such that A3: p.1 is _trivial edgeless & p.len p = G & len p = G.order()
and A4: for n being Element of dom p st n <= len p - 1
ex v being object, V being finite set
st v in the_Vertices_of G \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V
by Th80;
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & P[p.k];
A5: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus 1 = k;
thus P[p.k] by A1, A3;
end;
A6: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A7: Q[m];
assume A8: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A8, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A8, XREAL_1:13;
then consider k0 being Element of dom p such that
A9: m = k0 & P[p.k0] by A7;
m+1-1 <= len p - 1 by A8, XREAL_1:9;
then consider v being object, V being finite set such that
A10: v in the_Vertices_of G \ the_Vertices_of p.k0 and
A11: V c= the_Vertices_of p.k0 & p.(k0+1) is addAdjVertexAll of p.k0,v,V
by A4, A9;
not v in the_Vertices_of p.k0 by A10, XBOOLE_0:def 5;
hence thesis by A2, A9, A11;
end;
for m being non zero Nat holds Q[m] from NAT_1:sch 10(A5,A6); then
ex k being Element of dom p st len p = k & P[p.k];
hence thesis by A3;
end;
theorem
for p being non empty Graph-yielding FinSequence
st p.1 is simple &
for n being Element of dom p st n <= len p - 1
ex v being object, V being set st p.(n+1) is addAdjVertexAll of p.n,v,V
holds p.len p is simple
proof
let p be non empty Graph-yielding FinSequence;
assume that A1: p.1 is simple and
A2: for n being Element of dom p st n <= len p - 1 holds
ex v being object, V being set st p.(n+1) is addAdjVertexAll of p.n,v,V;
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & p.k is simple;
A3: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus thesis by A1;
end;
A4: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A5: Q[m];
assume A6: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A6, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A6, XREAL_1:13;
then consider k0 being Element of dom p such that
A7: m = k0 & p.k0 is simple by A5;
m+1-1 <= len p - 1 by A6, XREAL_1:9;
then consider v being object, V being set such that
A8: p.(k0+1) is addAdjVertexAll of p.k0,v,V by A2, A7;
thus thesis by A7, A8;
end;
for m being non zero Nat holds Q[m] from NAT_1:sch 10(A3,A4); then
ex k being Element of dom p st len p = k & p.k is simple;
hence thesis;
end;
theorem Th82:
for G being _finite simple connected _Graph
ex p being non empty _finite simple connected Graph-yielding FinSequence
st p.1 is _trivial edgeless & p.len p = G & len p = G.order() &
for n being Element of dom p st n <= len p - 1
ex v being object, V being non empty finite set
st v in the_Vertices_of G \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V
proof
defpred P[Nat] means for G being _finite simple connected _Graph
st G.order() = $1
ex p being non empty _finite simple connected Graph-yielding FinSequence
st p.1 is _trivial edgeless & p.len p = G & len p = G.order() &
for n being Element of dom p st n <= len p - 1
ex v being object, V being non empty finite set
st v in the_Vertices_of G \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V;
A1: P[1]
proof
let G be _finite simple connected _Graph;
assume A2: G.order() = 1;
set p = <* G *>;
take p;
G is _trivial by A2, GLIB_000:26;
hence p.1 is _trivial edgeless;
thus p.len p = p.1 by FINSEQ_1:40
.= G;
thus len p = G.order() by A2, FINSEQ_1:40;
let n be Element of dom p;
1 <= n & n <= len p by FINSEQ_3:25;
then 1 <= n & n <= 1 by FINSEQ_1:40;
then A3: n = 1 by XXREAL_0:1;
assume n <= len p - 1;
then n <= 1 - 1 by FINSEQ_1:40;
hence thesis by A3;
end;
A4: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume A5: P[k];
let G be _finite simple connected _Graph;
assume A6: G.order() = k+1;
A7: G is non _trivial
proof
assume G is _trivial;
then G.order() = 0 + 1 by GLIB_000:26;
hence contradiction by A6;
end;
then consider v9, v0 being Vertex of G such that
v9 <> v0 & v9 is non cut-vertex and
A8: v0 is non cut-vertex by GLIB_002:37;
set G2 = the removeVertex of G,v0;
A9: G2.order() + 1 = G.order() by A7, GLIB_000:48;
then A10: G2.order() = k by A6;
G2 is connected by A8, GLIB_002:36;
then consider p being
non empty _finite simple connected Graph-yielding FinSequence such that
A11: p.1 is _trivial edgeless & p.len p = G2 & len p = G2.order() and
A12: for n being Element of dom p st n <= len p - 1
ex v being object, V being non empty finite set
st v in the_Vertices_of G2 \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V
by A5, A10;
set q = p ^ <* G *>;
take q;
1 in dom p by FINSEQ_5:6;
hence q.1 is _trivial edgeless by A11, FINSEQ_1:def 7;
A13: len q = len p + len <* G *> by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:40;
hence A14: q.len q = G by FINSEQ_1:42;
thus len q = G.order() by A9, A11, A13;
let n be Element of dom q;
assume n <= len q - 1;
then per cases by Lm12;
suppose A15: n = len q - 1;
then A16: q.(n+1) = G by A14;
A17: 1 <= n by FINSEQ_3:25;
A18: n = len p by A13, A15;
then n in dom p by A17, FINSEQ_3:25;
then A19: q.n = G2 by A11, A18, FINSEQ_1:def 7;
reconsider V = v0.allNeighbors() as non empty finite set by A7;
take v0,V;
v0 in {v0} by TARSKI:def 1;
then not v0 in the_Vertices_of G \ {v0} by XBOOLE_0:def 5;
then not v0 in the_Vertices_of G2 by A7, GLIB_000:47;
hence v0 in the_Vertices_of G \ the_Vertices_of q.n
by A19, XBOOLE_0:def 5;
for x being object st x in V holds x in the_Vertices_of G2
proof
let x be object;
assume A20: x in V;
then x <> v0 by GLIB_000:112;
then A21: not x in {v0} by TARSKI:def 1;
x in the_Vertices_of G \ {v0} by A20, A21, XBOOLE_0:def 5;
hence thesis by A7, GLIB_000:47;
end;
hence V c= the_Vertices_of q.n by A19, TARSKI:def 3;
thus q.(n+1) is addAdjVertexAll of q.n,v0,V by A7, A16, A19, Th47;
end;
suppose A22: n <= len p - 1;
then A23: n+0 <= len p - 1 + 1 by XREAL_1:7;
1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A23, FINSEQ_3:25;
consider v being object, V being non empty finite set such that
A24: v in the_Vertices_of G2 \ the_Vertices_of p.m &
V c= the_Vertices_of p.m & p.(m+1) is addAdjVertexAll of p.m,v,V
by A12, A22;
1+0 <= n+1 & n+1 <= len p - 1 + 1 by A22, XREAL_1:6;
then n+1 in dom p by FINSEQ_3:25;
then A25: q.(n+1) = p.(m+1) by FINSEQ_1:def 7;
A26: q.n = p.m by FINSEQ_1:def 7;
take v,V;
the_Vertices_of G2 \ the_Vertices_of p.m
c= the_Vertices_of G \ the_Vertices_of p.m by XBOOLE_1:33;
hence v in the_Vertices_of G \ the_Vertices_of q.n by A24, A26;
thus thesis by A24, A25, A26;
end;
end;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A1,A4);
hence thesis;
end;
scheme
FinSimpleConnectedGraphs { P[_finite _Graph] } :
for G being _finite simple connected _Graph holds P[G]
provided
A1: for G being _trivial edgeless _Graph holds P[G] and
A2: for G2 being _finite simple connected _Graph
for v being object, V being non empty finite set
for G1 being addAdjVertexAll of G2,v,V
st not v in the_Vertices_of G2 & V c= the_Vertices_of G2 & P[G2]
holds P[G1]
proof
let G be _finite simple connected _Graph;
consider p being non empty _finite simple connected Graph-yielding
FinSequence
such that A3: p.1 is _trivial edgeless & p.len p = G & len p = G.order()
and A4: for n being Element of dom p st n <= len p - 1
ex v being object, V being non empty finite set
st v in the_Vertices_of G \ the_Vertices_of p.n &
V c= the_Vertices_of p.n & p.(n+1) is addAdjVertexAll of p.n,v,V
by Th82;
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & P[p.k];
A5: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus 1 = k;
thus P[p.k] by A1, A3;
end;
A6: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A7: Q[m];
assume A8: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A8, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A8, XREAL_1:13;
then consider k0 being Element of dom p such that
A9: m = k0 & P[p.k0] by A7;
m+1-1 <= len p - 1 by A8, XREAL_1:9;
then consider v being object, V being non empty finite set such that
A10: v in the_Vertices_of G \ the_Vertices_of p.k0 and
A11: V c= the_Vertices_of p.k0 & p.(k0+1) is addAdjVertexAll of p.k0,v,V
by A4, A9;
not v in the_Vertices_of p.k0 by A10, XBOOLE_0:def 5;
hence thesis by A2, A9, A11;
end;
for m being non zero Nat holds Q[m] from NAT_1:sch 10(A5,A6); then
ex k being Element of dom p st len p = k & P[p.k];
hence thesis by A3;
end;
theorem
for p being non empty Graph-yielding FinSequence
st p.1 is simple connected &
for n being Element of dom p st n <= len p - 1
ex v being object, V being non empty set
st p.(n+1) is addAdjVertexAll of p.n,v,V
holds p.len p is simple connected
proof
let p be non empty Graph-yielding FinSequence;
assume that A1: p.1 is simple connected and
A2: for n being Element of dom p st n <= len p - 1 holds
ex v being object, V being non empty set
st p.(n+1) is addAdjVertexAll of p.n,v,V;
defpred Q[Nat] means $1 <= len p implies ex k being Element of dom p
st $1 = k & p.k is simple connected;
A3: Q[1]
proof
assume 1 <= len p;
then reconsider k = 1 as Element of dom p by FINSEQ_3:25;
take k;
thus thesis by A1;
end;
A4: for m being non zero Nat st Q[m] holds Q[m+1]
proof
let m be non zero Nat;
assume A5: Q[m];
assume A6: m+1 <= len p;
0+1 <= m+1 by XREAL_1:6;
then reconsider k = m+1 as Element of dom p by A6, FINSEQ_3:25;
take k;
thus m+1 = k;
m+1-1 <= len p - 0 by A6, XREAL_1:13;
then consider k0 being Element of dom p such that
A7: m = k0 & p.k0 is simple connected by A5;
m+1-1 <= len p - 1 by A6, XREAL_1:9;
then consider v being object, V being non empty set such that
A8: p.(k0+1) is addAdjVertexAll of p.k0,v,V by A2, A7;
thus thesis by A7, A8;
end;
for m being non zero Nat holds Q[m] from NAT_1:sch 10(A3,A4); then
ex k being Element of dom p st len p = k & p.k is simple connected;
hence thesis;
end;