:: About Supergraphs, Part {I}
:: by Sebastian Koch
::
:: Received June 29, 2018
:: Copyright (c) 2018-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, GLIB_006, ABIAN, REWRITE1, CHORD, RCOMP_1, WAYBEL_0, FINSEQ_8,
GRAPH_1, JORDAN3, RFINSEQ, XCMPLX_0, INT_1, MSAFREE2, CARD_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_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, CHORD;
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,
RELSET_1, FUNCT_3, CHORD, NAT_D, GRAPH_2, RFINSEQ, FINSEQ_6, CARD_2,
FUNCT_7, FINSEQ_1, SUBSET_1;
registrations XBOOLE_0, ORDINAL1, FUNCOP_1, FINSET_1, ABIAN, XREAL_0, NAT_1,
FINSEQ_1, GLIB_000, GLIB_001, HELLY, GLIB_002, CHORD, INT_1, CARD_1,
HURWITZ2, RELSET_1, RAMSEY_1;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ORDINAL1, XXREAL_0, RELAT_1, CARD_1,
CARD_2, FUNCT_2, FUNCOP_1, FUNCT_4, NAT_D, 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, RFINSEQ, INT_1, HELLY, GRFUNC_1, PARTFUN1,
ENUMSET1;
schemes SUBSET_1, NAT_1;
begin :: general preliminaries
:: into ABIAN ?
theorem Th1:
for n being even Integer, m being odd Integer st n <= m holds n+1 <= m
proof
let n be even Integer, m be odd Integer;
assume A1: n <= m;
consider k1 being Integer such that
A2: n = 2*k1 by ABIAN:11;
consider k2 being Integer such that
A3: m = 2*k2+1 by ABIAN:1;
per cases;
suppose k1 <= k2;
then 2*k1 <= 2*k2 by XREAL_1:64;
hence n+1 <= m by A2, A3, XREAL_1:6;
end;
suppose k1 > k2;
then k2 + 1 <= k1 by INT_1:7;
then 2*(k2+1) <= 2*k1 by XREAL_1:64;
then 2*k2+2 <= 2*k2+1 by A1, A2, A3, XXREAL_0:2;
hence thesis by XREAL_1:6;
end;
end;
:: into ABIAN ?
theorem Th2:
for n being even Integer, m being odd Integer st m <= n holds m+1 <= n
proof
let n be even Integer, m be odd Integer;
assume A1: m <= n;
consider k1 being Integer such that
A2: n = 2*k1 by ABIAN:11;
consider k2 being Integer such that
A3: m+1 = 2*k2 by ABIAN:11;
per cases;
suppose k2 <= k1;
hence m+1 <= n by A2, A3, XREAL_1:64;
end;
suppose k2 > k1;
then k1 + 1 <= k2 by INT_1:7;
then A4: 2*(k1+1) <= 2*k2 by XREAL_1:64;
m+1 <= (2*k1)+1 by A1, A2, XREAL_1:6;
then 2*k1+2 <= 2*k1+1 by A3, A4, XXREAL_0:2;
hence thesis by XREAL_1:6;
end;
end;
:: into NAT_D ?
theorem Th3:
for i, j being Nat st i > i -' 1 + j holds j = 0
proof
let i, j be Nat;
assume i > i-'1+j;
then i-j+j > i-'1+j;
then A2: i-j > i-'1 by XREAL_1:6;
i-j >= 1
proof
assume A4: i-j < 1;
i-j+j > 0+j by A2, XREAL_1:6;
then i-j is Nat by NAT_1:21;
hence thesis by A2, A4, NAT_1:14;
end;
then i-j = i-'j by NAT_D:39;
hence j = 0 by A2, NAT_1:14, NAT_D:41;
end;
:: BEGIN into FINSEQ_6 or JORDAN4 ?
theorem Th6:
for f, g being FinSequence, i being Nat
st i <= len f & mid(f,i,i-'1+len g) = g
holds i-'1+len g <= len f
proof
let f, g be FinSequence, i be Nat;
set j = i-'1+len g;
assume that
A1: i <= len f and
A2: mid(f,i,j) = g;
per cases;
suppose A3: i <= j;
then A4: mid(f,i,j) = (f/^(i-'1))|(j-'i+1) by FINSEQ_6:def 3;
A5: i-'1 <= len f -' 1 by A1, NAT_D:42;
len f -' 1 <= len f by NAT_D:35;
then i-'1 <= len f by A5, XXREAL_0:2;
then A6: len (f/^(i-'1)) = len f - (i-'1) by RFINSEQ:def 1;
per cases;
suppose i > 0;
then A8: i-'1 = i-1 by NAT_1:14, XREAL_1:233;
per cases;
suppose len g >= 1;
then A10: len g - 1 = len g -' 1 by XREAL_1:233;
A11: (-1+len g)+i-'i = -1+len g by A10, NAT_D:34;
A12: j-'i+1 = len g by A8, A11;
per cases;
suppose len g <= len f - (i-'1);
then j+1-'i <= len f - (i-1) by A3, A12, A8, NAT_D:38;
then j+1-i <= len f - (i-1) by A3, NAT_D:37;
then j-(i-1) <= len f - (i-1);
hence thesis by XREAL_1:9;
end;
suppose len g > len f - (i-'1);
then (f/^(i-'1))|(j-'i+1) = (f/^(i-'1)) by A6, A12, FINSEQ_1:58;
hence thesis by A2, A4,A6;
end;
end;
suppose len g < 1;
then len g = 0 by NAT_1:14;
then j <= i by NAT_D:35;
hence thesis by A1, XXREAL_0:2;
end;
end;
suppose A14: i = 0;
0-'1 <= 0 by NAT_D:35;
then A15: i-'1 = 0 by A14;
A16: j-'i+1 = len g + 1 by A14, A15, NAT_D:40;
per cases;
suppose len g + 1 <= len f - (i-'1);
then A17: j+1 <= len f by A15;
j+0 <= j+1 by XREAL_1:6;
hence thesis by A17, XXREAL_0:2;
end;
suppose len g + 1 > len f - (i-'1);
then (f/^(i-'1))|(j-'i+1) = (f/^(i-'1)) by A6, A16, FINSEQ_1:58;
hence thesis by A2, A4, A6;
end;
end;
end;
suppose i > j;
then A20: len g = 0 by Th3;
i-'1 <= i by NAT_D:35;
hence thesis by A1, A20, XXREAL_0:2;
end;
end;
Th7:
for p being FinSequence, n being Nat st n in dom p
holds mid(p,n,n) = <*p.n*> by FINSEQ_6:193;
Th8: for p being FinSequence, k1,k2 being Nat
st k1 < k2 & k1 in dom p holds mid(p,k1,k2) = <*p.k1*> ^ mid(p,k1+1,k2)
by FINSEQ_6:126;
theorem Th9:
for p being FinSequence, n being Nat st n in dom p & n+1 <= len p
holds mid(p,n,n+1) = <*p.n, p.(n+1)*>
proof
let p be FinSequence, n be Nat;
assume A1: n in dom p & n+1 <= len p;
then n+1 in dom p by FINSEQ_3:25, XREAL_1:31;
then A2: mid(p,n+1,n+1) = <*p.(n+1)*> by Th7;
thus mid(p,n,n+1) = <*p.n*> ^ mid(p,n+1,n+1) by A1, Th8, XREAL_1:29
.= <*p.n, p.(n+1)*> by A2, FINSEQ_1:def 9;
end;
theorem Th10:
for p being FinSequence, n being Nat st n in dom p & n+2 <= len p
holds mid(p,n,n+2) = <*p.n, p.(n+1),p.(n+2)*>
proof
let p be FinSequence, n be Nat;
assume A1: n in dom p & n+2 <= len p;
then A2: 1 <= n & (n+1)+1 <= len p by FINSEQ_3:25;
A3: 1 <= n+1 by XREAL_1:31;
n+1+1-1 <= len p - 0 by A1, XREAL_1:13;
then A5: n+1 in dom p by A3, FINSEQ_3:25;
A6: mid(p,n+1,n+2) = <*p.(n+1), p.(n+2)*> by A2, A5, Th9;
thus mid(p,n,n+2) = <*p.n*> ^ mid(p,n+1,n+2) by A1, Th8, XREAL_1:29
.= <*p.n*> ^ (<*p.(n+1)*>^<*p.(n+2)*>) by A6, FINSEQ_1:def 9
.= <*p.n*> ^ <*p.(n+1)*> ^ <*p.(n+2)*> by FINSEQ_1:32
.= <*p.n, p.(n+1),p.(n+2)*> by FINSEQ_1:def 10;
end;
:: END into FINSEQ_6 or JORDAN 4 ?
:: during research the author noticed the strong similiariy between
:: (m,n)-cut p and smid(p,m,n) (from GRAPH_2 and FINSEQ_8)
:: but no theorems about that will be made here
:: SOLVED: added theorem at the end of FINSEQ_8
:: BEGIN into FINSEQ_8 ?
theorem Th11:
for D being non empty set, f,g being FinSequence of D, n being Nat
st g is_substring_of f,n holds len g = 0 or
(1 <= n-'1+len g & n-'1+len g <= len f & n <= n-'1+len g)
proof
let D be non empty set, f,g be FinSequence of D, n be Nat;
assume A1: g is_substring_of f,n;
per cases;
suppose A2: len g > 0;
then consider i being Nat such that
A3: n<=i & i<=len f and
A4: mid(f,i,(i-'1)+len g)=g by A1,FINSEQ_8:def 7;
A5: 1 <= n-'1+len g by A2, NAT_1:14;
A6: n <= n-'1+len g
proof
A7: n-'1+1 <= n-'1+len g by A2, NAT_1:14, XREAL_1:6;
per cases;
suppose n-'1 >= 1;
hence n <= n-'1+len g by A7, NAT_D:43;
end;
suppose n-'1 < 1;
then A8: n-'1 = 0 by NAT_1:14;
then n <= 0+1 by NAT_D:36;
then per cases by NAT_1:9;
suppose n = 0;
hence thesis;
end;
suppose n = 1;
hence n <= n-'1+len g by A7, A8;
end;
end;
end;
A9: (i-'1)+len g <= len f by A3, A4, Th6;
n-'1 <= i-'1 by A3, NAT_D:42;
then (n-'1)+len g <= (i-'1)+len g by XREAL_1:6;
hence thesis by A5, A6, A9, XXREAL_0:2;
end;
suppose len g = 0;
hence thesis;
end;
end;
definition
let D be non empty set, f,g be FinSequence of D, n be Nat;
pred g is_odd_substring_of f,n means
len g > 0 implies ex i being odd Nat
st n <= i & i <= len f & mid(f,i,(i-'1)+len g) = g;
pred g is_even_substring_of f,n means
len g > 0 implies ex i being even Nat
st n <= i & i <= len f & mid(f,i,(i-'1)+len g) = g;
end;
theorem Th12:
for D being non empty set, f,g being FinSequence of D, n being Nat
holds g is_odd_substring_of f,n implies g is_substring_of f,n
by FINSEQ_8:def 7;
theorem
for D being non empty set, f,g being FinSequence of D, n being Nat
holds g is_even_substring_of f,n implies g is_substring_of f,n
by FINSEQ_8:def 7;
theorem
for D being non empty set, f,g being FinSequence of D,
n,m being Nat st m >= n
holds (g is_odd_substring_of f,m implies g is_odd_substring_of f,n) &
(g is_even_substring_of f,m implies g is_even_substring_of f,n)
proof
let D be non empty set, f,g be FinSequence of D, n,m be Nat;
assume A1: m >= n;
hereby
assume A2: g is_odd_substring_of f,m;
per cases;
suppose len g > 0;
then consider i being odd Nat such that
A3: m<=i & i<=len f & mid(f,i,(i-'1)+len g) = g by A2;
n <= i by A1, A3, XXREAL_0:2;
hence g is_odd_substring_of f,n by A3;
end;
suppose not len g > 0;
hence g is_odd_substring_of f,n;
end;
end;
assume A4: g is_even_substring_of f,m;
per cases;
suppose len g > 0;
then consider i being even Nat such that
A5: m<=i & i<=len f & mid(f,i,(i-'1)+len g) = g by A4;
n <= i by A1, A5, XXREAL_0:2;
hence g is_even_substring_of f,n by A5;
end;
suppose not len g > 0;
hence g is_even_substring_of f,n;
end;
end;
theorem Th15:
for D being non empty set, f being FinSequence of D
st 1 <= len f holds f is_odd_substring_of f,0
proof
let D be non empty set, f be FinSequence of D;
assume A1: 1 <= len f;
now
assume len f > 0;
reconsider i = 1 as odd Element of NAT by POLYFORM:4;
take i;
thus 0 <= i;
thus i <= len f by A1;
thus mid(f,i,(i-'1)+len f) = mid(f,i,0+len f) by XREAL_1:232
.= f by A1, FINSEQ_6:120;
end;
hence thesis;
end;
theorem Th16:
for D being non empty set, f,g being FinSequence of D,
n being even Element of NAT
st g is_odd_substring_of f,n holds g is_odd_substring_of f,n+1 by Th1;
theorem
for D being non empty set, f,g being FinSequence of D,
n being odd Element of NAT
st g is_even_substring_of f,n holds g is_even_substring_of f,n+1 by Th2;
theorem Th18:
for D being non empty set, f,g being FinSequence of D
st g is_odd_substring_of f,0 holds g is_odd_substring_of f,1
proof
let D be non empty set, f,g be FinSequence of D;
reconsider n = 0 as even Element of NAT;
assume g is_odd_substring_of f,0;
then g is_odd_substring_of f,n+1 by Th16;
hence thesis;
end;
:: There are plenty theorems regarding predicate is_substring_of and
:: its even/odd equivalents that could be written here.
:: Many of them regard if the predicate holds with certain FinSequence
:: functors, e.g.
:: theorem for D being non empty set, f being FinSequence of D, m,n being Nat
:: st 1 <= m & m <= n & n <= len f holds (m,n)-cut p is_substring_of p,m
:: theorem for D being non empty set, f being FinSequence of D, m,n being Nat
:: holds (m,n)-cut p is_substring_of p,0
:: However, these theorems will not be proven here. Another set of theorems
:: deals with the transitivity properties of the predicate, e.g.
:: theorem for D being non empty set, f,g,h being FinSequence of D,
:: n,m being Element of NAT
:: st g is_substring_of f,n & h is_substring_of g,m
:: holds h is_substring_of f,n+m-'1
:: theorem for D being non empty set, f,g,h being FinSequence of D,
:: n,m being Element of NAT
:: st g is_even_substring_of f,n & h is_even_substring_of g,m
:: holds h is_odd_substring_of f,n+m-'1
:: These theorems will not be further investigated here either.
:: However, the author proposes the writing of an article that
:: deals with these properties along with the aforementioned
:: -cut/smid similiarity (maybe as FINSEQ_9 or add it to FINSEQ_8).
:: END into FINSEQ_8 ?
begin :: graph preliminaries
::$CT 7
:: definitely into GLIB_001
registration
let G be _Graph;
cluster closed Trail-like non trivial -> Circuit-like for Walk of G;
coherence by GLIB_001:def 30;
cluster closed Path-like non trivial -> Cycle-like for Walk of G;
coherence by GLIB_001:def 31;
end;
:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?
theorem Th26:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is Trail-like implies W2 is Trail-like
proof
let G1, G2 be _Graph;
let W1 be Walk of G1, W2 be Walk of G2;
assume W1 = W2;
then A2: W1.edgeSeq() = W2.edgeSeq() by GLIB_001:86;
assume W1 is Trail-like;
then W2.edgeSeq() is one-to-one by A2, GLIB_001:def 27;
hence W2 is Trail-like by GLIB_001:def 27;
end;
:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?
theorem Th27:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is Path-like implies W2 is Path-like
proof
let G1, G2 be _Graph;
let W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1 = W2;
assume W1 is Path-like;
then W2 is Trail-like & for m, n being odd Element of NAT
st m < n & n <= len W2 holds W2.m = W2.n implies m = 1 & n = len W2
by A1, Th26, GLIB_001:def 28;
hence W2 is Path-like by GLIB_001:def 28;
end;
:: generalizes part of GLIB_001:175 and GLIB_001:176
:: more general version of CHORD:24
:: into GLIB_001 ?
theorem
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is Cycle-like implies W2 is Cycle-like
proof
let G1, G2 be _Graph;
let W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1 = W2;
assume W1 is Cycle-like;
then W2 is closed Path-like non trivial
by A1, Th27, GLIB_001:121;
hence thesis;
end;
:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?
theorem
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is vertex-distinct implies W2 is vertex-distinct
proof
let G1, G2 be _Graph;
let W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1 = W2;
assume W1 is vertex-distinct;
then for m,n being odd Element of NAT st
m <= len W2 & n <= len W2 & W2.m = W2.n holds m = n by A1, GLIB_001:def 29;
hence W2 is vertex-distinct by GLIB_001:def 29;
end;
:: BEGIN into GLIB_001 ?
:: Four theorems have been left out, as they need more theorems
:: about is_substring_of (and the even/odd equivalents),
:: and that is not part of this article.
:: The theorems left out here are:
:: theorem for G being _Graph, W being Walk of G, m,n being odd Nat,
:: m2 being Element of NAT
:: st m <= n & n <= len W & m = m2 holds W.cut(m,n) is_odd_substring_of W,m2
:: theorem for G being _Graph, W being Walk of G, m,n being Nat holds
:: W.cut(m,n) is_odd_substring_of W,0
:: theorem for G being _Graph, W1, W2 being Walk of G st W1.last() = W2.first()
:: holds W2 is_odd_substring_of W1.append(W2),len W1
:: theorem for G being _Graph, W1, W2 being Walk of G
:: holds W1 is_odd_substring_of W1.append(W2),0
theorem
for G being _Graph, W being Walk of G, v being Vertex of G
st v in W.vertices() holds G.walkOf(v) is_substring_of W, 0
proof
let G be _Graph, W be Walk of G, v be Vertex of G;
assume v in W.vertices();
then consider n being odd Element of NAT such that
A1: n <= len W & W.n = v by GLIB_001:87;
now
assume len G.walkOf(v) > 0;
take n;
thus 0 <= n;
thus n <= len W by A1;
A3: (n-'1)+len G.walkOf(v) = n-'1+1 by GLIB_001:13
.= n+1-'1 by ABIAN:12, NAT_D:38
.= n+1-1 by NAT_D:37
.= n;
1 <= n by ABIAN:12;
then A4: n in dom W by A1, FINSEQ_3:25;
thus mid(W,n,(n-'1)+len G.walkOf(v)) = <*W.n*> by A3, A4, Th7
.= G.walkOf(v) by A1, GLIB_001:def 4;
end;
hence thesis by FINSEQ_8:def 7;
end;
theorem Th31:
for G being _Graph, W being Walk of G, n being odd Element of NAT
st n+2 <= len W holds G.walkOf(W.n,W.(n+1),W.(n+2)) is_odd_substring_of W, 0
proof
let G be _Graph, W be Walk of G, n be odd Element of NAT;
assume A1: n+2 <= len W;
then A2: n < len W by GLIB_001:1;
set W2 = G.walkOf(W.n,W.(n+1),W.(n+2));
now
assume len W2 > 0;
take n;
thus 0 <= n;
n+2-2 <= len W - 0 by A1, XREAL_1:13;
hence A3: n <= len W;
A5: W.(n+1) Joins W.n,W.(n+2),G by A2, GLIB_001:def 3;
then A6: (n-'1) + len W2 = (n -' 1) + 3 by GLIB_001:14
.= n + 3 -' 1 by ABIAN:12, NAT_D:38
.= n + 3 - 1 by NAT_D:37
.= n + 2;
1 <= n by ABIAN:12;
then n in dom W by A3, FINSEQ_3:25;
then mid(W,n,n+2) = <*W.n,W.(n+1),W.(n+2)*> by A1, Th10;
hence mid(W,n,(n-'1)+len W2)=W2 by A5, A6, GLIB_001:def 5;
end;
hence thesis;
end;
theorem
for G being _Graph, W being Walk of G, u,e,v being object
st e Joins u,v,G & e in W.edges()
holds G.walkOf(u,e,v) is_odd_substring_of W, 0
or G.walkOf(v,e,u) is_odd_substring_of W, 0
proof
let G be _Graph, W be Walk of G;
let u,e,v be object;
assume that
A1: e Joins u,v,G and
A2: e in W.edges();
consider n being odd Element of NAT such that
A3: n < len W & W.(n+1) = e by A2, GLIB_001:100;
n+2 <= len W by A3, GLIB_001:1;
then A4: G.walkOf(W.n,e,W.(n+2)) is_odd_substring_of W, 0 by A3, Th31;
e Joins W.n,W.(n+2),G by A3, GLIB_001:def 3;
then per cases by A1, GLIB_000:15;
suppose W.n = u & W.(n+2) = v;
hence thesis by A4;
end;
suppose W.n = v & W.(n+2) = u;
hence thesis by A4;
end;
end;
theorem
for G being _Graph, W being Walk of G, u,e,v being object
st e Joins u,v,G & G.walkOf(u,e,v) is_odd_substring_of W, 0
holds e in W.edges() & u in W.vertices() & v in W.vertices()
proof
let G be _Graph, W be Walk of G, u,e,v be object;
set W2 = G.walkOf(u,e,v);
assume e Joins u,v,G & W2 is_odd_substring_of W, 0;
then A1: e Joins u,v,G & W2 is_odd_substring_of W, 1 by Th18;
then A2: len W2 = 3 by GLIB_001:14;
consider i being odd Nat such that
A4: 1<=i & i<=len W & mid(W,i,(i-'1)+len W2) = W2 by A1;
set j = (i-'1)+len W2;
set M = the_Vertices_of G \/ the_Edges_of G;
W2 is_odd_substring_of W, i by A4;
then W2 is_substring_of W, i by Th12;
then A5: 1 <= j & j <= len W & i <= j by Th11;
len mid(W,i,j) = 3 by A1, A4, GLIB_001:14;
then A8: mid(W,i,j).1 = W.(1+i-'1) & mid(W,i,j).2 = W.(2+i-'1) &
mid(W,i,j).3 = W.(3+i-'1) by A4, A5, FINSEQ_6:118;
1+i-'1 = 1+i-1 & 2+i-'1 = 2+i-1 & 3+i-'1 = 3+i-1 by NAT_D:37;
then A9: W2.1 = W.i & W2.2 = W.(i+1) & W2.3 = W.(i+2) by A8, A4;
W2 = <*u,e,v*> by A1, GLIB_001:def 5;
then A10: W.i = u & W.(i+1) = e & W.(i+2) = v by A9;
j = i+3-'1 by A2, A4, NAT_D:38
.= i+3-1 by NAT_D:37
.= i+2;
then A11: 1 <= i+2 & i+2 <= len W by A5;
i+0 <= i+1 & i+1 <= i+2 by XREAL_1:6;
then A12: 1 <= i+1 & i+1 <= len W by A4, A11, XXREAL_0:2;
reconsider k=i+1 as even Element of NAT;
reconsider l=i+2 as odd Element of NAT;
thus e in W.edges() by A12, A10, GLIB_001:99;
i in NAT by ORDINAL1:def 12;
hence u in W.vertices() by A4, A10, GLIB_001:87;
thus v in W.vertices() by A11, A10, GLIB_001:87;
end;
definition
let G be _Graph, W1, W2 be Walk of G;
func W1.findFirstVertex(W2) -> odd Element of NAT means
:Def3:
it <= len W1 & ex k being even Nat st it = k+1 &
(for n being Nat st 1 <= n & n <= len W2 holds W1.(k+n) = W2.n) &
for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k <= l
if W2 is_odd_substring_of W1, 0
otherwise it = len W1;
existence
proof
hereby
defpred P[Nat] means $1 is even & $1 <= len W1 &
for n being Nat st 1 <= n & n <= len W2 holds W1.($1+n) = W2.n;
assume W2 is_odd_substring_of W1, 0;
then W2 is_odd_substring_of W1, 1 by Th18;
then consider i being odd Nat such that
A2: 1 <= i & i <= len W1 and
A3: mid(W1,i,(i-'1)+len W2) = W2;
A4: ex n being Nat st P[n]
proof
set j = (i-'1)+len W2;
reconsider k = i-1 as Nat by CHORD:2;
take k;
thus k is even;
i-1 <= len W1 - 0 by A2, XREAL_1:13;
hence k <= len W1;
let n be Nat;
assume A5: 1 <= n & n <= len W2;
then A6: 1 <= n & n <= len mid(W1,i,j) by A3;
1-1 <= len W2 - 1 by FINSEQ_1:20, XREAL_1:9;
then A8: 0 <= len W2 - 1;
j = i + len W2 -' 1 by A2, NAT_D:38
.= i + len W2 - 1 by A2, NAT_D:37;
then A10: i + (len W2 - 1) - (len W2 - 1) <= j - 0 by A8, XREAL_1:13;
then A11: 1 <= j by A2, XXREAL_0:2;
A12: 1 <= j & j <= len W1 by A11, A2, A3, Th6;
thus W1.(k+n) = W1.(n+i-1)
.= W1.(n+i-'1) by A5, NAT_D:37
.= W2.n by A2, A3, A6, A10, A12, FINSEQ_6:118;
end;
consider k being Nat such that
A13: P[k] and
A14: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A4);
reconsider k as even Nat by A13;
reconsider j = k+1 as odd Element of NAT;
take j;
thus j <= len W1 by A13, Th1;
take k;
thus j = k+1;
thus for n being Nat st 1 <= n & n <= len W2
holds W1.(k+n) = W2.n by A13;
let l be even Nat;
assume
A15: for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n;
per cases;
suppose l <= len W1;
hence k <= l by A14, A15;
end;
suppose l > len W1;
hence k <= l by A13, XXREAL_0:2;
end;
end;
assume not (W2 is_odd_substring_of W1, 0);
thus thesis;
end;
uniqueness
proof
let n1, n2 be odd Element of NAT;
hereby
assume that
W2 is_odd_substring_of W1, 0 & n1 <= len W1 and
A18: ex k1 being even Nat st n1 = k1+1 &
(for n being Nat st 1 <= n & n <= len W2 holds W1.(k1+n) = W2.n) &
for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k1 <= l and
n2 <= len W1 and
A20: ex k2 being even Nat st n2 = k2+1 &
(for n being Nat st 1 <= n & n <= len W2 holds W1.(k2+n) = W2.n) &
for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k2 <= l;
consider k1 being even Nat such that
A21: n1 = k1+1 and
A22: for n being Nat st 1 <= n & n <= len W2 holds W1.(k1+n) = W2.n and
A23: for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k1 <= l by A18;
consider k2 being even Nat such that
A24: n2 = k2+1 and
A25: for n being Nat st 1 <= n & n <= len W2 holds W1.(k2+n) = W2.n and
A26: for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k2 <= l by A20;
A27: k1 <= k2 by A23, A25;
k2 <= k1 by A22, A26;
hence n1 = n2 by A21, A24, A27, XXREAL_0:1;
end;
assume not (W2 is_odd_substring_of W1, 0) & n1 = len W1 & n2 = len W1;
hence thesis;
end;
consistency;
func W1.findLastVertex(W2) -> odd Element of NAT means
:Def4:
it <= len W1 & ex k being even Nat st it = k+len W2 &
(for n being Nat st 1 <= n & n <= len W2 holds W1.(k+n) = W2.n) &
for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k <= l
if W2 is_odd_substring_of W1, 0
otherwise it = len W1;
existence
proof
hereby
defpred P[Nat] means $1 is even & $1 <= len W1 - len W2 &
for n being Nat st 1 <= n & n <= len W2 holds W1.($1+n) = W2.n;
assume W2 is_odd_substring_of W1, 0;
then W2 is_odd_substring_of W1, 1 by Th18;
then consider i being odd Nat such that
A29: 1 <= i & i <= len W1 and
A30: mid(W1,i,(i-'1)+len W2) = W2;
A31: ex n being Nat st P[n]
proof
set j = (i-'1)+len W2;
set k = i-'1;
take k;
A32: i-'1 = i-1 by A29, XREAL_1:233;
hence k is even;
(i-'1)+len W2 <= len W1 by A29, A30, Th6;
then (i-'1)+len W2 - len W2 <= len W1 - len W2 by XREAL_1:9;
hence k <= len W1 - len W2;
let n be Nat;
assume A33: 1 <= n & n <= len W2;
then A34: 1 <= n & n <= len mid(W1,i,j) by A30;
len W2 >= 1 by FINSEQ_1:20;
then A36: 1-1 <= len W2 - 1 by XREAL_1:9;
j = i + len W2 -' 1 by A29, NAT_D:38
.= i + len W2 - 1 by A29, NAT_D:37;
then A38: i + (len W2 - 1) - (len W2 - 1) <= j - 0 by A36, XREAL_1:13;
A39: 1 <= j by A29, A38, XXREAL_0:2;
A40: 1 <= j & j <= len W1 by A39, A29, A30, Th6;
thus W1.(k+n) = W1.(n+i-1) by A32
.= W1.(n+i-'1) by A33, NAT_D:37
.= W2.n by A29, A30, A34, A38, A40, FINSEQ_6:118;
end;
consider k being Nat such that
A41: P[k] and
A42: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A31);
reconsider k as even Nat by A41;
reconsider j = k+len W2 as odd Element of NAT;
take j;
k + len W2 <= len W1 - len W2 + len W2 by A41, XREAL_1:6;
hence j <= len W1;
take k;
thus j = k+len W2;
thus for n being Nat st 1 <= n & n <= len W2
holds W1.(k+n) = W2.n by A41;
let l be even Nat;
assume A43: for n being Nat st 1 <= n & n <= len W2
holds W1.(l+n) = W2.n;
per cases;
suppose l <= len W1-len W2;
hence k <= l by A42, A43;
end;
suppose l > len W1-len W2;
hence k <= l by A41, XXREAL_0:2;
end;
end;
assume not (W2 is_odd_substring_of W1, 0);
thus thesis;
end;
uniqueness
proof
let n1, n2 be odd Element of NAT;
hereby
assume that
W2 is_odd_substring_of W1, 0 & n1 <= len W1 and
A46: ex k1 being even Nat st n1 = k1+len W2 &
(for n being Nat st 1 <= n & n <= len W2 holds W1.(k1+n) = W2.n) &
for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k1 <= l and
n2 <= len W1 and
A48: ex k2 being even Nat st n2 = k2+len W2 &
(for n being Nat st 1 <= n & n <= len W2 holds W1.(k2+n) = W2.n) &
for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k2 <= l;
consider k1 being even Nat such that
A49: n1 = k1+len W2 and
A50: for n being Nat st 1 <= n & n <= len W2 holds W1.(k1+n) = W2.n and
A51: for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k1 <= l by A46;
consider k2 being even Nat such that
A52: n2 = k2+len W2 and
A53: for n being Nat st 1 <= n & n <= len W2 holds W1.(k2+n) = W2.n and
A54: for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k2 <= l by A48;
A55: k1 <= k2 by A51, A53;
k2 <= k1 by A50, A54;
hence n1 = n2 by A49, A52, A55, XXREAL_0:1;
end;
assume not (W2 is_odd_substring_of W1, 0) & n1 = len W1 & n2 = len W1;
hence thesis;
end;
consistency;
end;
theorem Th34:
for G being _Graph, W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0
holds W1.(W1.findFirstVertex(W2)) = W2.first() &
W1.(W1.findLastVertex(W2)) = W2.last()
proof
let G be _Graph;
let W1, W2 be Walk of G;
assume A1: W2 is_odd_substring_of W1, 0;
then consider k1 being even Nat such that
A2: W1.findFirstVertex(W2) = k1+1 and
A3: for n being Nat st 1 <= n & n <= len W2 holds W1.(k1+n) = W2.n and
for l being even Nat st
for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k1 <= l by Def3;
consider k2 being even Nat such that
A4: W1.findLastVertex(W2) = k2+len W2 and
A5: for n being Nat st 1 <= n & n <= len W2 holds W1.(k2+n) = W2.n and
for l being even Nat st
for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k2 <= l by A1, Def4;
A6: 1 <= len W2 by ABIAN:12;
then W1.(W1.findFirstVertex(W2)) = W2.1 by A2, A3;
hence W1.(W1.findFirstVertex(W2)) = W2.first() by GLIB_001:def 6;
W1.(W1.findLastVertex(W2)) = W2.len W2 by A4, A5, A6;
hence W1.(W1.findLastVertex(W2)) = W2.last() by GLIB_001:def 7;
end;
theorem Th35:
for G being _Graph, W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0
holds 1 <= W1.findFirstVertex(W2) & W1.findFirstVertex(W2) <= len W1 &
1 <= W1.findLastVertex(W2) & W1.findLastVertex(W2) <= len W1
by Def3, Def4, ABIAN:12;
theorem Th36:
for G being _Graph, W being Walk of G
holds 1 = W.findFirstVertex(W) & W.findLastVertex(W) = len W
proof
let G be _Graph, W be Walk of G;
A2: W is_odd_substring_of W, 0 by Th15, ABIAN:12;
set n1 = W.findFirstVertex(W);
set n2 = W.findLastVertex(W);
consider k1 being even Nat such that
A3: n1 = k1+1 and
(for n being Nat st 1 <= n & n <= len W holds W.(k1+n) = W.n) and
A5: for l being even Nat
st for n being Nat st 1 <= n & n <= len W holds W.(l+n) = W.n
holds k1 <= l by A2, Def3;
A6: for n being Nat st 1 <= n & n <= len W holds W.(0+n) = W.n;
then k1 <= 0 by A5;
then k1 = 0;
hence 1 = n1 by A3;
consider k2 being even Nat such that
A7: n2 = k2+len W and
(for n being Nat st 1 <= n & n <= len W holds W.(k2+n) = W.n) and
A9: for l being even Nat
st for n being Nat st 1 <= n & n <= len W holds W.(l+n) = W.n
holds k2 <= l by A2, Def4;
k2 <= 0 by A6, A9;
then k2 = 0;
hence n2 = len W by A7;
end;
theorem
for G being _Graph, W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0
holds W1.findFirstVertex(W2) <= W1.findLastVertex(W2)
proof
let G be _Graph;
let W1, W2 be Walk of G;
assume A1: W2 is_odd_substring_of W1, 0;
then consider k1 being even Nat such that
A2: W1.findFirstVertex(W2) = k1+1 and
A3: for n being Nat st 1 <= n & n <= len W2 holds W1.(k1+n) = W2.n and
A4: for l being even Nat st
for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k1 <= l by Def3;
consider k2 being even Nat such that
A5: W1.findLastVertex(W2) = k2+len W2 and
A6: for n being Nat st 1 <= n & n <= len W2 holds W1.(k2+n) = W2.n and
A7: for l being even Nat st
for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k2 <= l by A1, Def4;
k1 = k2
proof
A9: k2 <= k1 by A3, A7;
k1 <= k2 by A4, A6;
hence thesis by A9, XXREAL_0:1;
end;
hence thesis by A2, A5, ABIAN:12, XREAL_1:6;
end;
definition
let G be _Graph, W1, W2, W3 be Walk of G;
func W1.replaceWith(W2, W3) -> Walk of G equals
:Def5:
W1.cut(1,W1.findFirstVertex(W2)
).append(W3
).append(W1.cut(W1.findLastVertex(W2), len W1))
if W2 is_odd_substring_of W1, 0 &
W2.first() = W3.first() & W2.last() = W3.last()
otherwise W1;
correctness;
end;
definition
let G be _Graph, W1, W3 be Walk of G;
let e be object;
func W1.replaceEdgeWith(e, W3) -> Walk of G equals
:Def6:
W1.replaceWith(G.walkOf(W3.first(),e,W3.last()),W3)
if e Joins W3.first(),W3.last(),G &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0
otherwise W1;
correctness;
end;
definition
let G be _Graph, W1, W2 be Walk of G;
let e be object;
func W1.replaceWithEdge(W2, e) -> Walk of G equals
:Def7:
W1.replaceWith(W2,G.walkOf(W2.first(),e,W2.last()))
if W2 is_odd_substring_of W1, 0 &
e Joins W2.first(),W2.last(),G
otherwise W1;
correctness;
end;
theorem Th38:
for G being _Graph, W1, W2, W3 being Walk of G
st W2 is_odd_substring_of W1, 0 &
W2.first() = W3.first() & W2.last() = W3.last()
holds
W1.cut(1,W1.findFirstVertex(W2)).first() = W1.first() &
W1.cut(1,W1.findFirstVertex(W2)).last() = W3.first() &
W1.cut(1,W1.findFirstVertex(W2)).append(W3).first() =
W1.first() &
W1.cut(1,W1.findFirstVertex(W2)).append(W3).last() =
W3.last() &
W1.cut(W1.findLastVertex(W2), len W1).first() = W3.last() &
W1.cut(W1.findLastVertex(W2), len W1).last() = W1.last()
proof
let G be _Graph;
let W1, W2, W3 be Walk of G;
assume A1: W2 is_odd_substring_of W1, 0 &
W2.first() = W3.first() & W2.last() = W3.last();
reconsider n1 = 1 as odd Element of NAT by POLYFORM:4;
set n2 = W1.findFirstVertex(W2);
set n3 = W1.findLastVertex(W2);
set n4 = len W1;
set W1c = W1.cut(n1,n2);
set W1ca = W1c.append(W3);
set W1c2 = W1.cut(n3, n4);
set W1caa = W1ca.append(W1c2);
n1 <= n2 & n2 <= len W1 by A1, Th35;
then A2: W1c.first() = W1.n1 & W1c.last() = W1.n2 by GLIB_001:37;
then A3: W1c.first() = W1.first() by GLIB_001:def 6;
A4: W1c.last() = W3.first() by A1, A2, Th34;
then A5: W1ca.first() = W1.n1 & W1ca.last() = W3.last() by A2, GLIB_001:30;
then A6: W1ca.first() = W1.first() by GLIB_001:def 6;
A7: W1ca.last() = W3.last() by A5;
n3 <= n4 & n4 <= len W1 by A1, Th35;
then A8: W1c2.first() = W1.n3 & W1c2.last() = W1.n4 by GLIB_001:37;
W1.n3 = W3.last() by A1, Th34;
then A9: W1c2.first() = W3.last() by A8;
A10: W1c2.last() = W1.last() by A8, GLIB_001:def 7;
thus thesis by A3, A4, A6, A7, A9, A10;
end;
theorem Th39:
for G being _Graph, W1, W2, W3 being Walk of G holds
W1.first() = W1.replaceWith(W2, W3).first() &
W1.last() = W1.replaceWith(W2, W3).last()
proof
let G be _Graph;
let W1, W2, W3 be Walk of G;
per cases;
suppose A1: W2 is_odd_substring_of W1, 0 &
W2.first() = W3.first() & W2.last() = W3.last();
then A2: W1.replaceWith(W2, W3) =
W1.cut(1,W1.findFirstVertex(W2)
).append(W3
).append(W1.cut(W1.findLastVertex(W2), len W1)) by Def5;
reconsider n1 = 1 as odd Element of NAT by POLYFORM:4;
set n2 = W1.findFirstVertex(W2);
set n3 = W1.findLastVertex(W2);
set n4 = len W1;
set W1c = W1.cut(n1,n2);
set W1ca = W1c.append(W3);
set W1c2 = W1.cut(n3, n4);
set W1caa = W1ca.append(W1c2);
W1ca.last() = W3.last() & W1c2.first() = W3.last() by A1, Th38;
then W1caa.first() = W1ca.first() & W1caa.last() = W1c2.last()
by GLIB_001:30;
hence thesis by A1, A2, Th38;
end;
suppose not (W2 is_odd_substring_of W1, 0 &
W2.first() = W3.first() & W2.last() = W3.last());
hence thesis by Def5;
end;
end;
theorem
for G being _Graph, W1, W2, W3 being Walk of G
st W2 is_odd_substring_of W1, 0 &
W2.first() = W3.first() & W2.last() = W3.last()
holds W1.replaceWith(W2, W3).vertices() =
W1.cut(1,W1.findFirstVertex(W2)).vertices() \/ W3.vertices() \/
W1.cut(W1.findLastVertex(W2), len W1).vertices()
proof
let G be _Graph, W1,W2,W3 be Walk of G;
assume A1: W2 is_odd_substring_of W1, 0 &
W2.first() = W3.first() & W2.last() = W3.last();
reconsider n1 = 1 as odd Element of NAT by POLYFORM:4;
set n2 = W1.findFirstVertex(W2);
set n3 = W1.findLastVertex(W2);
set n4 = len W1;
set W1c = W1.cut(n1,n2);
set W1ca = W1c.append(W3);
set W1c2 = W1.cut(n3, n4);
set W1caa = W1ca.append(W1c2);
W1c.last() = W3.first() by A1, Th38;
then A2: W1ca.vertices() = W1c.vertices() \/ W3.vertices() by GLIB_001:93;
W1ca.last() = W3.last() & W1c2.first() = W3.last() by A1, Th38;
then W1caa.vertices() = W1ca.vertices() \/ W1c2.vertices()
by GLIB_001:93;
hence thesis by A1, A2, Def5;
end;
theorem Th41:
for G being _Graph, W1, W2, W3 being Walk of G
st W2 is_odd_substring_of W1, 0 &
W2.first() = W3.first() & W2.last() = W3.last()
holds W1.replaceWith(W2, W3).edges() =
W1.cut(1,W1.findFirstVertex(W2)).edges() \/ W3.edges() \/
W1.cut(W1.findLastVertex(W2), len W1).edges()
proof
let G be _Graph, W1,W2,W3 be Walk of G;
assume A1: W2 is_odd_substring_of W1, 0 &
W2.first() = W3.first() & W2.last() = W3.last();
reconsider n1 = 1 as odd Element of NAT by POLYFORM:4;
set n2 = W1.findFirstVertex(W2);
set n3 = W1.findLastVertex(W2);
set n4 = len W1;
set W1c = W1.cut(n1,n2);
set W1ca = W1c.append(W3);
set W1c2 = W1.cut(n3, n4);
set W1caa = W1ca.append(W1c2);
W1c.last() = W3.first() by A1, Th38;
then A2: W1ca.edges() = W1c.edges() \/ W3.edges() by GLIB_001:102;
W1ca.last() = W3.last() & W1c2.first() = W3.last() by A1, Th38;
then W1caa.edges() = W1ca.edges() \/ W1c2.edges() by GLIB_001:102;
hence thesis by A1, A2, Def5;
end;
theorem Th42:
for G being _Graph, W1, W3 being Walk of G, e being object
st e Joins W3.first(),W3.last(),G &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0
holds e in W1.replaceEdgeWith(e, W3).edges() iff
e in W1.cut(1,W1.findFirstVertex(G.walkOf(W3.first(),e,W3.last()))).edges()
or e in W3.edges() or e in W1.cut(W1.findLastVertex(
G.walkOf(W3.first(),e,W3.last())), len W1).edges()
proof
let G be _Graph, W1,W3 be Walk of G;
let e be object;
assume that
A1: e Joins W3.first(),W3.last(),G and
A2: G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0;
set W2 = G.walkOf(W3.first(),e,W3.last());
set W9 = W1.replaceWith(W2,W3);
A3: W9 = W1.replaceEdgeWith(e, W3) by A1, A2, Def6;
A4: W2.first() = W3.first() & W2.last() = W3.last() by A1, GLIB_001:15;
hereby
assume e in W1.replaceEdgeWith(e, W3).edges();
then e in W1.cut(1,W1.findFirstVertex(W2)).edges() \/ W3.edges() \/
W1.cut(W1.findLastVertex(W2), len W1).edges() by A2, A3, A4, Th41;
then e in W1.cut(1,W1.findFirstVertex(W2)).edges() \/ W3.edges() or
e in W1.cut(W1.findLastVertex(W2), len W1).edges() by XBOOLE_0:def 3;
hence e in W1.cut(1,W1.findFirstVertex(W2)).edges() or e in W3.edges() or
e in W1.cut(W1.findLastVertex(W2), len W1).edges() by XBOOLE_0:def 3;
end;
assume e in W1.cut(1,W1.findFirstVertex(W2)).edges() or e in W3.edges() or
e in W1.cut(W1.findLastVertex(W2), len W1).edges();
then e in W1.cut(1,W1.findFirstVertex(W2)).edges() \/ W3.edges() or
e in W1.cut(W1.findLastVertex(W2), len W1).edges() by XBOOLE_0:def 3;
then e in W1.cut(1,W1.findFirstVertex(W2)).edges() \/ W3.edges() \/
W1.cut(W1.findLastVertex(W2), len W1).edges() by XBOOLE_0:def 3;
hence thesis by A2, A3, A4, Th41;
end;
:: The Proof got surprisingly long. Maybe there's a shorter way?
theorem Th43:
for G being _Graph, W1, W3 being Walk of G, e being object
st e Joins W3.first(),W3.last(),G & not e in W3.edges() &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0 &
for n, m being even Nat st n in dom W1 & m in dom W1 & W1.n = e & W1.m = e
holds n = m
holds not e in W1.replaceEdgeWith(e, W3).edges()
proof
let G be _Graph, W1,W3 be Walk of G;
let e be object;
assume that
A1: e Joins W3.first(),W3.last(),G and
A2: not e in W3.edges() and
A3: G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0 and
A4: for n, m being even Nat
st n in dom W1 & m in dom W1 & W1.n = e & W1.m = e
holds n = m;
set W2 = G.walkOf(W3.first(),e,W3.last());
set W9 = W1.replaceWith(W2,W3);
A6: W2 is_odd_substring_of W1, 1 by A3, Th18;
A7: len W2 = 3 by A1, GLIB_001:14;
:: first step of Proof is to find first usable index of e in W1
defpred P[Nat] means $1 is odd & 1 <= $1 & $1 <= len W1
& mid(W1,$1,($1-'1)+len W2) = W2;
A9: ex i being Nat st P[i] by A6;
consider i being Nat such that
A10: P[i] and
A11: for n being Nat st P[n] holds i <= n from NAT_1:sch 5(A9);
reconsider i as odd Element of NAT by A10, ORDINAL1:def 12;
set j = i-'1+len W2;
W2 is_odd_substring_of W1, i by A10;
then W2 is_substring_of W1, i by Th12;
then A12: (1 <= j & j <= len W1 & i <= j) by Th11;
A13: mid(W1,i,(i-'1)+len W2)
= <*W3.first(),e,W3.last()*> by A1, A10, GLIB_001:def 5;
:: n1 is said index, show some properties of it
set n1 = i+1;
i-1 = i-'1 by A10, XREAL_1:233;
then A15: j = i+2 by A7;
A16: 1 <= 2 <= len mid(W1,i,j) by A7, A10;
A19: 1 <= j & j <= len W1 by A12;
A20: i <= j by A12;
then mid(W1,i,j).2 = W1.(2+i-'1) by A10, A16, A19, FINSEQ_6:118;
then <*W3.first(),e,W3.last()*>.2 = W1.(2+i-1) by A13, NAT_D:37
.= W1.n1;
:: finally, W1.n1 is proven to equal e
then A21: W1.n1 = e;
:: Now we show that i (=n1-1) is first Vertex index and
:: i+2 (=n1+1) is last Vertex index of W2 in W1
reconsider k=i-1 as even Nat by CHORD:1;
:: substring property as in the First/LastVertex definitions
A22: for n being Nat st 1 <= n & n <= len W2 holds W1.(k+n)=W2.n
proof
let n be Nat;
assume A23: 1 <= n & n <= len W2;
then 1 <= n & n <= len mid(W1,i,j) by A10;
then A24: W1.(n+i-'1) = W2.n by A10, A19, A20, FINSEQ_6:118;
n+i-'1 = n+i-1 by A23, NAT_D:37 .= k+n;
hence W1.(k+n) = W2.n by A24;
end;
:: minimal property as in the First/LastVertex definitions
A25: for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k <= l
proof
let l be even Nat;
assume A26: for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n)=W2.n;
per cases;
suppose A27: l <= len W1;
reconsider k2 = l+1 as odd Nat;
per cases;
suppose A28: k2+2 <= len W1;
P[k2]
proof
thus k2 is odd;
thus A30: 1 <= k2 by ABIAN:12;
thus A31: k2 <= len W1 by A27, Th1;
k2-1 = k2-'1 by A30, XREAL_1:233;
then A33: (k2-'1)+len W2 = k2+2 by A7;
A34: k2 in dom W1 by A30, A31, FINSEQ_3:25;
A35: 1 <= 1 & 1 <= len W2 &
1 <= 2 & 2 <= len W2 &
1 <= 3 & 3 <= len W2 by A7;
mid(W1,k2,(k2-'1)+len W2)
= <*W1.k2,W1.(k2+1),W1.(k2+2)*> by A33, A34, A28, Th10
.= <*W2.1,W1.(l+2),W1.(l+3)*> by A26, A35
.= <*W2.1,W2.2,W1.(l+3)*> by A26, A35
.= <*W2.1,W2.2,W2.3*> by A26, A35;
hence thesis by A7, FINSEQ_1:45;
end;
then i-1 <= k2-1 by A11, XREAL_1:9;
hence k <= l;
end;
suppose k2+2 > len W1;
then i+2 <= k2+2 by A15,A19,XXREAL_0:2;
then i-1 <= k2-1 by XREAL_1:6, XREAL_1:9;
hence k <= l;
end;
end;
suppose l > len W1;
then A37: len W1 <= l;
A38: k <= len W1 -1 by A10, XREAL_1:9;
len W1 -1 <= len W1 -0 by XREAL_1:13;
then k <= len W1 by A38, XXREAL_0:2;
hence k <= l by A37, XXREAL_0:2;
end;
end;
:: we conclude i as first Vertex
i <= len W1 & ex k being even Nat st i = k+1 &
(for n being Nat st 1 <= n & n <= len W2 holds W1.(k+n) = W2.n) &
for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k <= l
proof
thus i <= len W1 by A10;
take k;
thus i = k+1;
thus thesis by A22, A25;
end;
then A39: i = W1.findFirstVertex(W2) by A3, Def3;
:: we conclude i+2 as last Vertex
i+2 <= len W1 & ex k being even Nat st i+2 = k+len W2 &
(for n being Nat st 1 <= n & n <= len W2 holds W1.(k+n) = W2.n) &
for l being even Nat
st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n
holds k <= l by A7, A15, A19, A22, A25;
then A40: i+2 = W1.findLastVertex(W2) by A3, Def4;
:: show that n1 is strictly between first and last vertex index of W2;
:: this will be used to show a contradiction in the last two parts
:: of this Proof
A41: W1.findFirstVertex(W2) < n1
proof
assume W1.findFirstVertex(W2) >= n1;
then W1.findFirstVertex(W2) +1 <= W1.findFirstVertex(W2) +0 by A39;
hence contradiction by XREAL_1:6;
end;
A42: n1 < W1.findLastVertex(W2) by A40, XREAL_1:6;
n1 in dom W1
proof
i+0 <= i+1 & i+1 <= i+2 by XREAL_1:6;
then 1 <= i+1 & i+1 <= len W1 by XXREAL_0:2, A10, A15, A12;
hence thesis by FINSEQ_3:25;
end;
then A44: n1 in dom W1 & W1.findFirstVertex(W2) < n1 &
n1 < W1.findLastVertex(W2) by A41, A42;
:: Now show first part of thesis
A45: not e in W1.cut(1,W1.findFirstVertex(W2)).edges()
proof
:: we show that the negation leads to n1 <= first vertex index
:: by using the one-to-one-in e property from the initial assumption
assume e in W1.cut(1,W1.findFirstVertex(W2)).edges();
then consider n2 being even Element of NAT such that
A46: 1 <= n2 & n2 <= len W1.cut(1,W1.findFirstVertex(W2)) and
A47: W1.cut(1,W1.findFirstVertex(W2)).n2 = e by GLIB_001:99;
reconsider n9 = 1 as odd Element of NAT by POLYFORM:4;
A48: n9 <= W1.findFirstVertex(W2) & W1.findFirstVertex(W2) <= len W1
by A3, Th35;
then A49: len W1.cut(1,W1.findFirstVertex(W2)) + 1
= W1.findFirstVertex(W2) + 1 by GLIB_001:36;
then A50: n2 <= W1.findFirstVertex(W2) by A46;
n2 is non zero by A46;
then reconsider n3=n2-1 as Nat by CHORD:1;
reconsider n3 as Element of NAT by ORDINAL1:def 12;
W1.findFirstVertex(W2) <= len W1 by A3, Th35;
then n2 <= len W1 by A50, XXREAL_0:2;
then A51: n2 in dom W1 by A46, FINSEQ_3:25;
n3 < W1.findFirstVertex(W2)
proof
assume n3 >= W1.findFirstVertex(W2);
then A52: n2-1+1 >= W1.findFirstVertex(W2) + 1 by XREAL_1:6;
W1.findFirstVertex(W2) +0 < W1.findFirstVertex(W2) +1 by XREAL_1:8;
hence contradiction by A50, A52, XXREAL_0:2;
end;
then W1.cut(n9,W1.findFirstVertex(W2)).(n3+1) = W1.(n9+n3)
by A48, A49, GLIB_001:36;
:: here goes the one-to-one-in e property
hence contradiction by A50, A44, A21, A4, A47, A51;
end;
:: second part of thesis
not e in W1.cut(W1.findLastVertex(W2), len W1).edges()
proof
:: same idea as before, just a little more sophisticated
:: because the cut doesn't (necessarily) start with 1
assume e in W1.cut(W1.findLastVertex(W2), len W1).edges();
then consider n2 being even Element of NAT such that
A53: 1 <= n2 & n2 <= len W1.cut(W1.findLastVertex(W2), len W1) and
A54: W1.cut(W1.findLastVertex(W2), len W1).n2 = e by GLIB_001:99;
reconsider n9 = 1 as odd Element of NAT by POLYFORM:4;
set D = len W1 + 1 - W1.findLastVertex(W2);
A55: n9 <= W1.findLastVertex(W2) & W1.findLastVertex(W2) <= len W1
by A3, Th35;
then A56: len W1.cut(W1.findLastVertex(W2), len W1) + W1.findLastVertex(W2)
= len W1 + 1 by GLIB_001:36;
then A57: n2 <= len W1 + 1 - W1.findLastVertex(W2) by A53;
n2 is non zero by A53;
then reconsider n3=n2-1 as Nat by CHORD:1;
reconsider n3 as Element of NAT by ORDINAL1:def 12;
1 <= W1.findLastVertex(W2) by A3, Th35;
then 1+(n2-1) <= W1.findLastVertex(W2)+(n2-1) by XREAL_1:6;
then A58: 1 <= W1.findLastVertex(W2)+n3 by A53, XXREAL_0:2;
W1.findLastVertex(W2)+n3 = n2 +(W1.findLastVertex(W2)-1);
then n3 +W1.findLastVertex(W2) <=
(len W1 + 1 - W1.findLastVertex(W2)) +(W1.findLastVertex(W2)-1)
by A57, XREAL_1:6;
then A59: W1.findLastVertex(W2)+n3 in dom W1 by A58, FINSEQ_3:25;
n3 < D
proof
assume n3 >= D;
then A60: n2-1+1 >= D + 1 by XREAL_1:6;
D +0 < D +1 by XREAL_1:8;
hence contradiction by A57, A60, XXREAL_0:2;
end;
then W1.cut(W1.findLastVertex(W2), len W1).(n3+1) =
W1.(W1.findLastVertex(W2)+n3) by A55, GLIB_001:36, A56;
:: here goes the one-to-one-in e property again
then W1.findLastVertex(W2)+n2-1 = n1 by A21, A4, A54, A59, A44;
then W1.findLastVertex(W2)+1 <= n1+1 by A53, XREAL_1:7;
hence contradiction by A44, XREAL_1:6;
end;
:: the two parts together with assumption not e in W3.edges()
:: show thesis by use of last theorem
hence not e in W1.replaceEdgeWith(e, W3).edges() by A2, A45, A1, A3, Th42;
end;
:: this is the important theorem from this whole preliminary theory
:: on replacement of parts of walks that will be used in the main part
theorem Th44:
for G being _Graph, T1 being Trail of G, W3 being Walk of G, e being object
st e Joins W3.first(),W3.last(),G & not e in W3.edges() &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of T1, 0
holds not e in T1.replaceEdgeWith(e, W3).edges()
proof
let G be _Graph, T1 be Trail of G, W3 be Walk of G, e be object;
assume that
A1: e Joins W3.first(),W3.last(),G and
A2: not e in W3.edges() and
A3: G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of T1, 0;
for n, m being even Nat st n in dom T1 & m in dom T1 & T1.n = e & T1.m = e
holds n = m
proof
let n,m be even Nat;
assume A4: n in dom T1 & m in dom T1 & T1.n = e & T1.m = e;
then A5: 1 <= n & n <= len T1 & 1 <= m & m <= len T1 by FINSEQ_3:25;
reconsider n,m as even Element of NAT by ORDINAL1:def 12;
per cases by XXREAL_0:1;
suppose n < m;
hence thesis by A4, A5, GLIB_001:138;
end;
suppose n = m;
hence thesis;
end;
suppose n > m;
hence thesis by A4, A5, GLIB_001:138;
end;
end;
hence thesis by A1, A2, A3, Th43;
end;
theorem
for G being _Graph, W1, W2 being Walk of G
st W1.first() = W2.first() & W1.last() = W2.last()
holds W1.replaceWith(W1,W2) = W2
proof
let G be _Graph, W1, W2 be Walk of G;
assume A1: W1.first() = W2.first() & W1.last() = W2.last();
A2: 1 <= len W1 by ABIAN:12;
then A3: W1 is_odd_substring_of W1, 0 by Th15;
reconsider n1 = 1 as odd Element of NAT by POLYFORM:4;
set n2 = W1.findFirstVertex(W1);
set n3 = W1.findLastVertex(W1);
set n4 = len W1;
set W1c = W1.cut(n1,n2);
set W1ca = W1c.append(W2);
set W1c2 = W1.cut(n3, n4);
set W1caa = W1ca.append(W1c2);
A4: n2 = 1 & n3 = len W1 by Th36;
then A5: W1c is trivial & W1c2 is trivial by A2, GLIB_001:131;
1 <= n1 & n1 <= n2 & n2 <= len W1 by A3, Th35;
then W1c.last() = W1.n2 by GLIB_001:37;
then W1c.last() = W1.first() by A4, GLIB_001:def 6;
then W1c.last() = W2.first() by A1;
then W1ca = W2 by HELLY:16, A5;
then W1caa = W2 by A5, GLIB_001:130;
hence thesis by A1, A3, Def5;
end;
:: The following theorem has been left out
:: theorem ThExtra: for G being _Graph, W1, W2 being Walk of G
:: holds W1.replaceWith(W2,W2) = W1
:: as it needs
:: theorem for G being _Graph, W1, W2 being Walk of G
:: st W2 is_odd_substring_of W1,0 holds ex m,n being Element of NAT
:: st 1 <= m & m <= n & n <= len W2 & W1.cut(m,n) = W2
:: which in turn relies on unproven theorems about is_odd_substring_of
:: and -cut/smid.
:: the assumption in the following theorem could be dropped
:: if the theorems above would be available
theorem Th46:
for G being _Graph, W1, W3 being Walk of G, e being object
st e Joins W3.first(),W3.last(),G &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0
holds ex W2 being Walk of G
st W1.replaceEdgeWith(e,W3) = W1.replaceWith(W2,W3)
proof
let G be _Graph, W1, W3 be Walk of G, e be object;
::per cases;
::suppose A1: e Joins W3.first(),W3.last(),G &
:: G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0;
assume A1: e Joins W3.first(),W3.last(),G &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0;
take G.walkOf(W3.first(),e,W3.last());
thus thesis by A1, Def6;
::end;
::suppose not (e Joins W3.first(),W3.last(),G &
:: G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0);
:: then A2: W1.replaceEdgeWith(e, W3) = W1 by Def6;
:: take W3;
:: thus thesis by A2, ThExtra;
::end;
end;
:: same as theorem above
theorem Th47:
for G being _Graph, W1, W2 being Walk of G, e being object
st W2 is_odd_substring_of W1, 0 & e Joins W2.first(),W2.last(),G
holds ex W3 being Walk of G
st W1.replaceWithEdge(W2,e) = W1.replaceWith(W2,W3)
proof
let G be _Graph, W1, W2 be Walk of G, e be object;
::per cases;
::suppose A1: W2 is_odd_substring_of W1, 0 &
:: e Joins W2.first(),W2.last(),G;
assume A1: W2 is_odd_substring_of W1, 0 &
e Joins W2.first(),W2.last(),G;
take G.walkOf(W2.first(),e,W2.last());
thus thesis by A1, Def7;
::end;
::suppose not (W2 is_odd_substring_of W1, 0 &
:: e Joins W2.first(),W2.last(),G);
:: then A2: W1.replaceWithEdge(W2, e) = W1 by Def7;
:: take W2;
:: thus thesis by A2, Th38;
::end;
end;
theorem
for G being _Graph, W1, W3 being Walk of G, e being object holds
W1.first() = W1.replaceEdgeWith(e, W3).first() &
W1.last() = W1.replaceEdgeWith(e, W3).last()
proof
let G be _Graph;
let W1, W3 be Walk of G;
let e be object;
per cases;
suppose e Joins W3.first(),W3.last(),G &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0;
then consider W2 being Walk of G such that
A1: W1.replaceEdgeWith(e,W3) = W1.replaceWith(W2,W3) by Th46;
thus thesis by A1, Th39;
end;
suppose not (e Joins W3.first(),W3.last(),G &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0);
hence thesis by Def6;
end;
end;
theorem
for G being _Graph, W1, W2 being Walk of G, e being object holds
W1.first() = W1.replaceWithEdge(W2, e).first() &
W1.last() = W1.replaceWithEdge(W2, e).last()
proof
let G be _Graph;
let W1, W2 be Walk of G;
let e be object;
per cases;
suppose W2 is_odd_substring_of W1, 0 & e Joins W2.first(),W2.last(),G;
then consider W3 being Walk of G such that
A1: W1.replaceWithEdge(W2, e) = W1.replaceWith(W2,W3) by Th47;
thus thesis by A1, Th39;
end;
suppose not (W2 is_odd_substring_of W1, 0 & e Joins W2.first(),W2.last(),G);
hence thesis by Def7;
end;
end;
theorem Th50:
for G being _Graph, W1, W2, W3 being Walk of G, u,v being object holds
W1 is_Walk_from u,v iff W1.replaceWith(W2, W3) is_Walk_from u,v
proof
let G be _Graph;
let W1, W2, W3 be Walk of G;
let u,v be object;
W1 is_Walk_from u,v iff W1.first() = u & W1.last() = v by GLIB_001:def 23;
then W1 is_Walk_from u,v iff
u = W1.replaceWith(W2, W3).first() &
v = W1.replaceWith(W2, W3).last() by Th39;
hence thesis by GLIB_001:def 23;
end;
theorem Th51:
for G being _Graph, W1, W3 being Walk of G, e,u,v being object holds
W1 is_Walk_from u,v iff W1.replaceEdgeWith(e, W3) is_Walk_from u,v
proof
let G be _Graph;
let W1, W3 be Walk of G;
let e,u,v be object;
per cases;
suppose e Joins W3.first(),W3.last(),G &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0;
then consider W2 being Walk of G such that
A1: W1.replaceEdgeWith(e,W3) = W1.replaceWith(W2,W3) by Th46;
thus thesis by A1, Th50;
end;
suppose not (e Joins W3.first(),W3.last(),G &
G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0);
hence thesis by Def6;
end;
end;
theorem
for G being _Graph, W1, W2 being Walk of G, e,u,v being object holds
W1 is_Walk_from u,v iff W1.replaceWithEdge(W2, e) is_Walk_from u,v
proof
let G be _Graph;
let W1, W2 be Walk of G;
let e,u,v be object;
per cases;
suppose W2 is_odd_substring_of W1, 0 & e Joins W2.first(),W2.last(),G;
then consider W3 being Walk of G such that
A1: W1.replaceWithEdge(W2,e) = W1.replaceWith(W2,W3) by Th47;
thus thesis by A1, Th50;
end;
suppose not (W2 is_odd_substring_of W1, 0 & e Joins W2.first(),W2.last(),G);
hence thesis by Def7;
end;
end;
:: END into GLIB_001 ?
:: into GLIB_002 ?
theorem Th53:
for G being _Graph, v1, v2 being Vertex of G st v1 is isolated & v1 <> v2
holds not v2 in G.reachableFrom v1
proof
let G be _Graph, v1,v2 be Vertex of G;
assume A1: v1 is isolated & v1 <> v2;
assume v2 in G.reachableFrom v1;
then consider W being Walk of G such that
A2: W is_Walk_from v1,v2 by GLIB_002:def 5;
A3: W.first() = v1 & W.last() = v2 by A2, GLIB_001:def 23;
then v1 in W.vertices() by GLIB_001:88;
hence contradiction by A1, A3, GLIB_001:127, GLIB_001:135;
end;
:: into GLIB_002 ?
theorem Th54:
for G being _Graph, v1, v2 being Vertex of G
holds v1 in G.reachableFrom v2 implies v2 in G.reachableFrom v1
proof
let G be _Graph, v1, v2 be Vertex of G;
assume v1 in G.reachableFrom v2;
then G.reachableFrom v2 = G.reachableFrom v1 by GLIB_002:12;
hence thesis by GLIB_002:9;
end;
:: into GLIB_002 ?
theorem Th55:
for G being _Graph, v being Vertex of G
st v is isolated holds {v} = G.reachableFrom(v)
proof
let G be _Graph, v be Vertex of G;
assume A1: v is isolated;
for x being object holds x in {v} iff x in G.reachableFrom(v)
proof
let x be object;
hereby
assume x in {v};
then x = v by TARSKI:def 1;
hence x in G.reachableFrom(v) by GLIB_002:9;
end;
assume A2: x in G.reachableFrom(v);
then reconsider v2 = x as Vertex of G;
v = v2 by A1, A2, Th53;
hence x in {v} by TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
:: into GLIB_002 ?
theorem
for G being _Graph, v being Vertex of G, C being inducedSubgraph of G, {v}
st v is isolated holds C is Component of G
proof
let G be _Graph, v be Vertex of G, C be inducedSubgraph of G, {v};
assume v is isolated;
then {v} = G.reachableFrom(v) by Th55;
hence thesis;
end;
:: into GLIB_002 ?
theorem Th57:
for G1 being non _trivial _Graph, v being Vertex of G1,
G2 being removeVertex of G1, v
st v is isolated holds G1.componentSet() = G2.componentSet() \/ {{v}} &
G1.numComponents() = G2.numComponents() +` 1
proof
let G1 be non _trivial _Graph, v be Vertex of G1, G2 be removeVertex of G1,v;
assume A1: v is isolated;
for V being object holds
V in G1.componentSet() iff V in G2.componentSet() \/ {{v}}
proof
let V be object;
hereby
assume V in G1.componentSet();
then consider v1 being Vertex of G1 such that
A2: V = G1.reachableFrom(v1) by GLIB_002:def 8;
per cases;
suppose v = v1;
then V = {v} by A1, A2, Th55;
then V in {{v}} by TARSKI:def 1;
hence V in G2.componentSet() \/ {{v}} by XBOOLE_0:def 3;
end;
suppose v <> v1;
then not v1 in {v} by TARSKI:def 1;
then v1 in the_Vertices_of G1 \ {v} by XBOOLE_0:def 5;
then reconsider v2 = v1 as Vertex of G2 by GLIB_000:def 37;
for v3 being object holds
v3 in G1.reachableFrom(v1) implies v3 in G2.reachableFrom(v2)
proof
let v3 be object;
assume A3: v3 in G1.reachableFrom(v1);
per cases;
suppose A4: v2 <> v3;
ex W2 being Walk of G2 st W2 is_Walk_from v2,v3
proof
consider W being Walk of G1 such that
A5: W is_Walk_from v1,v3 by A3, GLIB_002:def 5;
W.first() = v1 & W.last() = v3 by A5, GLIB_001:def 23;
then W is non trivial by A4, GLIB_001:127;
then not v in W.vertices() by A1, GLIB_001:135;
then reconsider W2 = W as Walk of G2 by GLIB_001:171;
take W2;
thus thesis by A5, GLIB_001:19;
end;
hence thesis by GLIB_002:def 5;
end;
suppose v2 = v3;
hence v3 in G2.reachableFrom(v2) by GLIB_002:9;
end;
end;
then A6: G1.reachableFrom(v1) c= G2.reachableFrom(v2) by TARSKI:def 3;
G2.reachableFrom(v2) c= G1.reachableFrom(v1) by GLIB_002:14;
then G1.reachableFrom(v1) = G2.reachableFrom(v2)
by A6, XBOOLE_0:def 10;
then V in G2.componentSet() by A2, GLIB_002:def 8;
hence V in G2.componentSet() \/ {{v}} by XBOOLE_0:def 3;
end;
end;
assume V in G2.componentSet() \/ {{v}};
then per cases by XBOOLE_0:def 3;
suppose V in G2.componentSet();
then consider v2 being Vertex of G2 such that
A7: V = G2.reachableFrom(v2) by GLIB_002:def 8;
reconsider v1 = v2 as Vertex of G1 by GLIB_000:42;
for v3 being object holds
v3 in G1.reachableFrom(v1) implies v3 in G2.reachableFrom(v2)
proof
let v3 be object;
assume A8: v3 in G1.reachableFrom(v1);
per cases;
suppose A9: v2 <> v3;
ex W2 being Walk of G2 st W2 is_Walk_from v2,v3
proof
consider W being Walk of G1 such that
A10: W is_Walk_from v1,v3 by A8, GLIB_002:def 5;
W.first() = v1 & W.last() = v3 by A10, GLIB_001:def 23;
then W is non trivial by A9, GLIB_001:127;
then not v in W.vertices() by A1, GLIB_001:135;
then reconsider W2 = W as Walk of G2 by GLIB_001:171;
take W2;
thus thesis by A10, GLIB_001:19;
end;
hence thesis by GLIB_002:def 5;
end;
suppose v2 = v3;
hence v3 in G2.reachableFrom(v2) by GLIB_002:9;
end;
end;
then A11: G1.reachableFrom(v1) c= G2.reachableFrom(v2) by TARSKI:def 3;
G2.reachableFrom(v2) c= G1.reachableFrom(v1) by GLIB_002:14;
then G1.reachableFrom(v1) = G2.reachableFrom(v2) by A11, XBOOLE_0:def 10;
hence V in G1.componentSet() by A7, GLIB_002:def 8;
end;
suppose V in {{v}};
then V = {v} by TARSKI:def 1;
then V = G1.reachableFrom(v) by A1, Th55;
hence V in G1.componentSet() by GLIB_002:def 8;
end;
end;
hence A12: G1.componentSet() = G2.componentSet() \/ {{v}} by TARSKI:2;
not {v} in G2.componentSet()
proof
assume {v} in G2.componentSet();
then consider v2 being Vertex of G2 such that
A13: {v} = G2.reachableFrom(v2) by GLIB_002:def 8;
v in G2.reachableFrom(v2) by A13, TARSKI:def 1;
then A14: v in the_Vertices_of G2;
v in {v} by TARSKI:def 1;
then not v in the_Vertices_of G1 \ {v} by XBOOLE_0:def 5;
hence contradiction by A14, GLIB_000:47;
end;
then A15: G2.componentSet() misses {{v}} by ZFMISC_1:50;
thus G1.numComponents() = card G1.componentSet() by GLIB_002:def 9
.= card G2.componentSet() +` card {{v}} by A12, A15, CARD_2:35
.= G2.numComponents() +` card {{v}} by GLIB_002:def 9
.= G2.numComponents() +` 1 by CARD_2:42;
end;
:: into GLIB_002 ?
registration
let G be _Graph;
cluster isolated -> non cut-vertex for Vertex of G;
coherence
proof
let v be Vertex of G;
assume A1: v is isolated;
ex G2 being removeVertex of G,v st
not G.numComponents() in G2.numComponents()
proof
set G2 = the removeVertex of G,v;
take G2;
per cases;
suppose G is non _trivial;
then G.numComponents() = G2.numComponents() +` 1 by A1, Th57;
hence thesis by ORDINAL1:5, CARD_2:94;
end;
suppose G is _trivial;
then consider v1 being Vertex of G such that
A2: the_Vertices_of G = {v1} by GLIB_000:22;
v = v1 by A2, TARSKI:def 1;
then the_Vertices_of G \ {v} is empty by A2, XBOOLE_1:37;
then G == G2 by GLIB_000:def 37;
then G.numComponents() = G2.numComponents() by GLIB_002:29;
hence thesis;
end;
end;
hence thesis by GLIB_002:def 10;
end;
end;
:: into GLIB_002 ?
theorem Th58:
for G1 being _Graph, G2 being Subgraph of G1,
W1 being Walk of G1, W2 being Walk of G2 st W1 = W2
holds W1 is Cycle-like iff W2 is Cycle-like
proof
let G1 be _Graph, G2 be Subgraph of G1;
let W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1 = W2;
hereby
assume W1 is Cycle-like;
then W2 is closed & W2 is Path-like & W2 is non trivial
by A1, GLIB_001:176;
hence W2 is Cycle-like;
end;
assume W2 is Cycle-like;
then W1 is closed & W1 is Path-like & W1 is non trivial by A1, GLIB_001:176;
hence W1 is Cycle-like;
end;
:: into GLIB_002 ?
theorem
for G1 being connected _Graph, G2 being Component of G1 holds G1 == G2
proof
let G1 be connected _Graph;
let G2 be Component of G1;
reconsider G3 = G1 as Component of G1 by GLIB_002:30;
set v = the Vertex of G2;
reconsider w=v as Vertex of G1 by GLIB_000:42;
the_Vertices_of G2 = G1.reachableFrom(w) by GLIB_002:33
.= the_Vertices_of G3 by GLIB_002:16;
hence thesis by GLIB_002:32;
end;
:: into CHORD ?
registration
cluster complete -> connected for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is complete;
for u,v being Vertex of G holds ex W being Walk of G st W is_Walk_from u,v
proof
let u,v be Vertex of G;
per cases;
suppose A2: u = v;
take G.walkOf(v);
thus thesis by A2, GLIB_001:13;
end;
suppose u <> v;
then consider e being object such that
A3: e Joins u,v,G by A1, CHORD:def 6, CHORD:def 3;
take G.walkOf(u,e,v);
thus thesis by A3, GLIB_001:15;
end;
end;
hence thesis by GLIB_002:def 1;
end;
end;
registration
cluster non non-Dmulti non non-multi non loopless non Dsimple non simple
non acyclic non _finite for _Graph;
existence
proof
0 in {0} by TARSKI:def 1;
then reconsider f0 = NAT --> 0 as Function of NAT, {0} by FUNCOP_1:45;
set G = createGraph({0}, NAT, f0, f0);
A1: for n being Nat holds n DJoins 0,0,G
proof
let n be Nat;
A2: n in NAT by ORDINAL1:def 12;
then A3: n in the_Edges_of G;
A4: (the_Source_of G).n = f0.n
.= 0 by A2, FUNCOP_1:7;
(the_Target_of G).n = f0.n
.= 0 by A2, FUNCOP_1:7;
hence thesis by A3, A4, GLIB_000:def 14;
end;
take G;
ex e1,e2,v1,v2 being object st
e1 DJoins v1,v2,G & e2 DJoins v1,v2,G & e1 <> e2
proof
take 0,1,0,0;
thus thesis by A1;
end;
hence G is non non-Dmulti non non-multi by GLIB_000:def 21;
::hence G is non non-multi;
ex e being object st e in the_Edges_of G &
(the_Source_of G).e = (the_Target_of G).e
proof
take 0;
thus thesis;
end;
hence G is non loopless non Dsimple non simple;
::hence G is non Dsimple & G is non simple;
set W = G.walkOf(0,0,0);
0 DJoins 0,0,G by A1;
then 0 Joins 0,0,G by GLIB_000:16;
then W is Cycle-like by GLIB_001:156;
hence G is non acyclic;
not the_Edges_of G is finite;
hence thesis;
end;
end;
reserve G for _Graph;
definition
let G;
func Endvertices(G) -> Subset of the_Vertices_of G means
:Def8:
for v being object holds v in it iff
ex w being Vertex of G st v = w & w is endvertex;
existence
proof
defpred P[object] means ex w being Vertex of G st $1 = w & w is endvertex;
consider M being Subset of the_Vertices_of G such that
A1: for v being set holds v in M iff
v in the_Vertices_of G & P[v] from SUBSET_1:sch 1;
take M;
thus thesis by A1;
end;
uniqueness
proof
let E1, E2 be Subset of the_Vertices_of G;
assume that
A2: for v being object holds v in E1 iff
ex w being Vertex of G st v = w & w is endvertex and
A3: for v being object holds v in E2 iff
ex w being Vertex of G st v = w & w is endvertex;
now
let v be object;
hereby
assume v in E1;
then ex w being Vertex of G st v = w & w is endvertex by A2;
hence v in E2 by A3;
end;
assume v in E2;
then ex w being Vertex of G st v = w & w is endvertex by A3;
hence v in E1 by A2;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
for v being Vertex of G holds v in Endvertices(G) iff v is endvertex
proof
let v be Vertex of G;
hereby
assume v in Endvertices(G);
then consider w being Vertex of G such that
A1: v = w & w is endvertex by Def8;
thus v is endvertex by A1;
end;
thus thesis by Def8;
end;
begin :: Supergraphs
:: analogue to GLIB_000:def 32
definition
let G;
mode Supergraph of G -> _Graph means
:Def9:
the_Vertices_of G c= the_Vertices_of it &
the_Edges_of G c= the_Edges_of it &
for e being set st e in the_Edges_of G holds
(the_Source_of G).e = (the_Source_of it).e &
(the_Target_of G).e = (the_Target_of it).e;
existence
proof
take G;
thus thesis;
end;
end;
:: Now we show some handy trivialities. Most of them have a
:: Subgraph equivalent in e.g. GLIB_000 and are shown through it and
:: the following theorem
:: Hence not all Subgraph theorems are reproduced here as they can be easily
:: shown.
theorem Th61:
for G1, G2 being _Graph
holds G2 is Subgraph of G1 iff G1 is Supergraph of G2
proof
let G1, G2 be _Graph;
thus G2 is Subgraph of G1 implies G1 is Supergraph of G2
proof
assume G2 is Subgraph of G1;
then
the_Vertices_of G2 c= the_Vertices_of G1 &
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 Def9;
end;
assume G1 is Supergraph of G2;
then
the_Vertices_of G2 c= the_Vertices_of G1 &
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 Def9;
hence thesis by GLIB_000:def 32;
end;
theorem Th62:
for G1, G2 being _Graph
holds G2 is Subgraph of G1 & G2 is Supergraph of G1 iff G1 == G2
proof
let G1, G2 be _Graph;
G1 == G2 iff G2 is Subgraph of G1 & G1 is Subgraph of G2 by GLIB_000:87;
hence thesis by Th61;
end;
theorem Th63:
for G1, G2 being _Graph
holds G1 is Supergraph of G2 & G2 is Supergraph of G1 iff G1 == G2
proof
let G1, G2 be _Graph;
G1 == G2 iff G2 is Subgraph of G1 & G1 is Subgraph of G2 by GLIB_000:87;
hence thesis by Th61;
end;
theorem Th64:
for G1, G2 being _Graph holds G1 is Supergraph of G2 iff G2 c= G1
proof
let G1, G2 be _Graph;
G1 is Supergraph of G2 iff G2 is Subgraph of G1 by Th61;
hence thesis by GLIB_000:def 35;
end;
theorem Th65:
G is Supergraph of G by Th64;
theorem Th66:
for G3 being _Graph, G2 being Supergraph of G3, G1 being Supergraph of G2
holds G1 is Supergraph of G3
proof
let G3 be _Graph, G2 be Supergraph of G3, G1 be Supergraph of G2;
G3 is Subgraph of G2 & G2 is Subgraph of G1 by Th61;
then G3 is Subgraph of G1 by GLIB_000:43;
hence thesis by Th61;
end;
reserve G2 for _Graph, G1 for Supergraph of G2;
:: the following 4 Supergraph theorems have no Subgraph analogon in the MML yet
theorem Th67:
for G1, G2 being _Graph st the_Vertices_of G2 c= the_Vertices_of G1 &
the_Source_of G2 c= the_Source_of G1 &
the_Target_of G2 c= the_Target_of G1
holds G1 is Supergraph of G2
proof
let G1, G2 be _Graph;
assume that
A1: the_Vertices_of G2 c= the_Vertices_of G1 and
A2: the_Source_of G2 c= the_Source_of G1 and
A3: the_Target_of G2 c= the_Target_of G1;
A4: dom the_Source_of G2 = the_Edges_of G2 &
dom the_Target_of G2 = the_Edges_of G2 &
dom the_Source_of G1 = the_Edges_of G1 &
dom the_Target_of G1 = the_Edges_of G1 by GLIB_000:4;
A6: the_Edges_of G2 c= the_Edges_of G1 by A3, A4, RELAT_1:11;
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 A2, A3, A4, GRFUNC_1:2;
hence thesis by A1, A6, Def9;
end;
theorem Th68:
for G2, G1 holds the_Source_of G2 c= the_Source_of G1 &
the_Target_of G2 c= the_Target_of G1
proof
let G2, G1;
A1: dom the_Source_of G2 = the_Edges_of G2 &
dom the_Target_of G2 = the_Edges_of G2 &
dom the_Source_of G1 = the_Edges_of G1 &
dom the_Target_of G1 = the_Edges_of G1 by GLIB_000:4;
A2: dom the_Source_of G2 c= dom the_Source_of G1 &
dom the_Target_of G2 c= dom the_Target_of G1 by A1, Def9;
for e being object holds e in dom the_Source_of G2 implies
(the_Source_of G2).e = (the_Source_of G1).e by Def9;
hence the_Source_of G2 c= the_Source_of G1 by A2, GRFUNC_1:2;
for e being object holds e in dom the_Target_of G2 implies
(the_Target_of G2).e = (the_Target_of G1).e by Def9;
hence the_Target_of G2 c= the_Target_of G1 by A2, GRFUNC_1:2;
end;
theorem Th69:
for G2, G1 st the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 holds G1 == G2
proof
let G2, G1;
assume that
A1: the_Vertices_of G2 = the_Vertices_of G1 and
A2: the_Edges_of G2 = the_Edges_of G1;
dom the_Source_of G2 = the_Edges_of G2 &
dom the_Target_of G2 = the_Edges_of G2 &
dom the_Source_of G1 = the_Edges_of G1 &
dom the_Target_of G1 = the_Edges_of G1 by GLIB_000:4;
then the_Source_of G2 = the_Source_of G1 &
the_Target_of G2 = the_Target_of G1 by A2, Th68, GRFUNC_1:3;
hence thesis by A1, A2, GLIB_000:def 34;
end;
theorem
for G1, G2 being _Graph st the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 &
the_Source_of G2 c= the_Source_of G1 &
the_Target_of G2 c= the_Target_of G1
holds G1 == G2
proof
let G1, G2 be _Graph;
assume that
A1: the_Vertices_of G2 = the_Vertices_of G1 and
A2: the_Edges_of G2 = the_Edges_of G1 and
A3: the_Source_of G2 c= the_Source_of G1 and
A4: the_Target_of G2 c= the_Target_of G1;
G1 is Supergraph of G2 by A1, A3, A4, Th67;
hence thesis by A1, A2, Th69;
end;
theorem Th71:
for G2, G1 for x being set holds
(x in the_Vertices_of G2 implies x in the_Vertices_of G1) &
(x in the_Edges_of G2 implies x in the_Edges_of G1)
proof
let G2, G1;
let x be set;
G2 is Subgraph of G1 by Th61;
hence thesis by GLIB_000:42;
end;
theorem Th72:
for G2, G1 for v being Vertex of G2 holds v is Vertex of G1 by Th71;
theorem
for G2, G1 holds
the_Source_of G2 = (the_Source_of G1) | the_Edges_of G2 &
the_Target_of G2 = (the_Target_of G1) | the_Edges_of G2
proof
let G2, G1;
G2 is Subgraph of G1 by Th61;
hence thesis by GLIB_000:45;
end;
theorem Th74:
for G2, G1 for x,y being set, e being object holds
(e Joins x,y,G2 implies e Joins x,y,G1) &
(e DJoins x,y,G2 implies e DJoins x,y,G1) &
(e SJoins x,y,G2 implies e SJoins x,y,G1) &
(e DSJoins x,y,G2 implies e DSJoins x,y,G1)
proof
let G2, G1;
let x,y be set;
let e be object;
G2 is Subgraph of G1 by Th61;
hence thesis by GLIB_000:72;
end;
theorem Th75:
for G2, G1 for e,v1,v2 being object st e DJoins v1,v2,G1
holds e DJoins v1,v2,G2 or not e in the_Edges_of G2
proof
let G2, G1;
let e,v1,v2 be object;
assume A1: e DJoins v1,v2,G1;
per cases;
suppose not e in the_Edges_of G2;
hence thesis;
end;
suppose A2: e in the_Edges_of G2;
A3: e in the_Edges_of G1 &
(the_Source_of G1).e = v1 &
(the_Target_of G1).e = v2 by A1, GLIB_000:def 14;
reconsider e1=e as set by TARSKI:1;
(the_Source_of G2).e = v1 & (the_Target_of G2).e = v2 by A2, A3, Def9;
hence thesis by GLIB_000:def 14;
end;
end;
theorem Th76:
for G2, G1 for e,v1,v2 being object st e Joins v1,v2,G1
holds e Joins v1,v2,G2 or not e in the_Edges_of G2
proof
let G2, G1;
let e,v1,v2 be object;
assume e Joins v1,v2,G1;
then per cases by GLIB_000:16;
suppose e DJoins v1,v2,G1;
then per cases by Th75;
suppose e DJoins v1,v2,G2;
hence thesis by GLIB_000:16;
end;
suppose not e in the_Edges_of G2;
hence thesis;
end;
end;
suppose e DJoins v2,v1,G1;
then per cases by Th75;
suppose e DJoins v2,v1,G2;
hence thesis by GLIB_000:16;
end;
suppose not e in the_Edges_of G2;
hence thesis;
end;
end;
end;
registration
let G be _finite _Graph;
cluster _finite for Supergraph of G;
existence
proof
reconsider G1 = G as Supergraph of G by Th62;
take G1;
thus thesis;
end;
end;
:: no equivalent in GLIB_000
theorem
for G2, G1 holds G2.order() c= G1.order() & G2.size() c= G1.size()
proof
let G2, G1;
the_Vertices_of G2 c= the_Vertices_of G1 &
the_Edges_of G2 c= the_Edges_of G1 by Def9;
then card the_Vertices_of G2 c= card the_Vertices_of G1 &
card the_Edges_of G2 c= card the_Edges_of G1 by CARD_1:11;
then G2.order() c= card the_Vertices_of G1 &
G2.size() c= card the_Edges_of G1 by GLIB_000:def 24, GLIB_000:def 25;
hence thesis by GLIB_000:def 24, GLIB_000:def 25;
end;
theorem
for G2 being _finite _Graph, G1 being _finite Supergraph of G2 holds
G2.order() <= G1.order() & G2.size() <= G1.size()
proof
let G2 be _finite _Graph, G1 be _finite Supergraph of G2;
G2 is Subgraph of G1 by Th61;
hence thesis by GLIB_000:75;
end;
theorem Th79:
for G2, G1 for W being Walk of G2 holds W is Walk of G1
proof
let G2, G1;
A1: G2 is Subgraph of G1 by Th61;
let W be Walk of G2;
thus thesis by A1, GLIB_001:167;
end;
theorem Th80:
for G2, G1 for W2 being Walk of G2, W1 being Walk of G1 st W1 = W2 holds
(W1 is closed iff W2 is closed) &
(W1 is directed iff W2 is directed) &
(W1 is trivial iff W2 is trivial) &
(W1 is Trail-like iff W2 is Trail-like) &
(W1 is Path-like iff W2 is Path-like) &
(W1 is vertex-distinct iff W2 is vertex-distinct) &
(W1 is Cycle-like iff W2 is Cycle-like)
proof
let G2, G1;
A1: G2 is Subgraph of G1 by Th61;
let W2 being Walk of G2;
let W1 being Walk of G1;
assume W1 = W2;
hence thesis by A1, Th58, GLIB_001:176;
end;
registration
let G be non _trivial _Graph;
cluster -> non _trivial for Supergraph of G;
coherence
proof
let G2 be Supergraph of G;
A1: G is Subgraph of G2 by Th61;
assume G2 is _trivial;
hence contradiction by A1;
end;
end;
registration
let G be non non-Dmulti _Graph;
cluster -> non non-Dmulti for Supergraph of G;
coherence
proof
let G2 be Supergraph of G;
A1: G is Subgraph of G2 by Th61;
assume G2 is non-Dmulti;
hence contradiction by A1;
end;
end;
registration
let G be non non-multi _Graph;
cluster -> non non-multi for Supergraph of G;
coherence
proof
let G2 be Supergraph of G;
A1: G is Subgraph of G2 by Th61;
assume G2 is non-multi;
hence contradiction by A1;
end;
end;
registration
let G be non loopless _Graph;
cluster -> non loopless for Supergraph of G;
coherence
proof
let G2 be Supergraph of G;
A1: G is Subgraph of G2 by Th61;
assume G2 is loopless;
hence contradiction by A1;
end;
end;
registration
let G be non Dsimple _Graph;
cluster -> non Dsimple for Supergraph of G;
coherence
proof
let G1 be Supergraph of G;
per cases;
suppose G is non non-Dmulti;
hence thesis;
end;
suppose G is non loopless;
hence thesis;
end;
end;
end;
registration
let G be non simple _Graph;
cluster -> non simple for Supergraph of G;
coherence
proof
let G1 be Supergraph of G;
per cases;
suppose G is non non-multi;
hence thesis;
end;
suppose G is non loopless;
hence thesis;
end;
end;
end;
registration
let G be non acyclic _Graph;
cluster -> non acyclic for Supergraph of G;
coherence
proof
let G2 be Supergraph of G;
A1: G is Subgraph of G2 by Th61;
assume G2 is acyclic;
hence contradiction by A1;
end;
end;
registration
let G be non _finite _Graph;
cluster -> non _finite for Supergraph of G;
coherence
proof
let G2 be Supergraph of G;
A1: G is Subgraph of G2 by Th61;
assume G2 is _finite;
hence contradiction by A1;
end;
end;
reserve V for set;
definition
let G, V;
mode addVertices of G, V -> Supergraph of G means
:Def10:
the_Vertices_of it = the_Vertices_of G \/ V &
the_Edges_of it = the_Edges_of G &
the_Source_of it = the_Source_of G &
the_Target_of it = the_Target_of G;
existence
proof
reconsider V1 = the_Vertices_of G \/ V as non empty set;
A1: the_Vertices_of G c= V1 by XBOOLE_1:7;
set E = the_Edges_of G;
reconsider S1 = the_Source_of G as Function of E, V1 by A1, FUNCT_2:7;
reconsider T1 = the_Target_of G as Function of E, V1 by A1, FUNCT_2:7;
set G1 = createGraph(V1,E,S1,T1);
for e being set st e in the_Edges_of G holds
(the_Source_of G).e = (the_Source_of G1).e &
(the_Target_of G).e = (the_Target_of G1).e;
then reconsider G1 as Supergraph of G by Def9, XBOOLE_1:7;
take G1;
thus thesis;
end;
end;
theorem
for G, V for G1, G2 being addVertices of G, V holds G1 == G2
proof
let G, V;
let G1, G2 be addVertices of G, V;
the_Vertices_of G1 = the_Vertices_of G \/ V &
the_Edges_of G1 = the_Edges_of G &
the_Source_of G1 = the_Source_of G &
the_Target_of G1 = the_Target_of G &
the_Vertices_of G2 = the_Vertices_of G \/ V &
the_Edges_of G2 = the_Edges_of G &
the_Source_of G2 = the_Source_of G &
the_Target_of G2 = the_Target_of G by Def10;
hence thesis by GLIB_000:def 34;
end;
theorem Th82:
for G2, V for G1 being addVertices of G2, V
holds G1 == G2 iff V c= the_Vertices_of G2
proof
let G2, V;
let G1 be addVertices of G2, V;
hereby
assume G1 == G2;
then the_Vertices_of G2 = the_Vertices_of G1 by GLIB_000:def 34
.= the_Vertices_of G2 \/ V by Def10;
hence V c= the_Vertices_of G2 by XBOOLE_1:11;
end;
assume V c= the_Vertices_of G2;
then A1: V \/ the_Vertices_of G2 c=
the_Vertices_of G2 \/ the_Vertices_of G2 by XBOOLE_1:9;
the_Vertices_of G2 c= V \/ the_Vertices_of G2 by XBOOLE_1:7;
then A2: the_Vertices_of G2 = V \/ the_Vertices_of G2 by A1, XBOOLE_0:def 10
.= the_Vertices_of G1 by Def10;
the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 &
the_Target_of G1 = the_Target_of G2 by Def10;
hence thesis by A2, GLIB_000:def 34;
end;
theorem
for G1, G2 being _Graph, V being set st G1 == G2 & V c= the_Vertices_of G2
holds G1 is addVertices of G2, V
proof
let G1, G2 be _Graph, V be set;
assume A1: G1 == G2 & V c= the_Vertices_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 &
the_Target_of G1 = the_Target_of G2 by GLIB_000:def 34;
then A3: the_Vertices_of G1 = the_Vertices_of G2 \/ V &
the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 &
the_Target_of G1 = the_Target_of G2 by A1, XBOOLE_1:12;
G1 is Supergraph of G2 by A1, Th63;
hence thesis by A3, Def10;
end;
theorem
for G, G2, V for G1 being addVertices of G, V st G1 == G2
holds G2 is addVertices of G, V
proof
let G, G2, V;
let G1 be addVertices of G, V;
assume A1: G1 == G2;
then the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 &
the_Target_of G1 = the_Target_of G2 &
the_Source_of G1 = the_Source_of G2 by GLIB_000:def 34;
then A2: the_Vertices_of G2 = the_Vertices_of G \/ V &
the_Edges_of G2 = the_Edges_of G &
the_Source_of G2 = the_Source_of G &
the_Target_of G2 = the_Target_of G by Def10;
G2 is Supergraph of G1 by A1, Th62;
then G2 is Supergraph of G by Th66;
hence thesis by A2, Def10;
end;
theorem Th85:
for G2, V for G1 being addVertices of G2, V
holds G1.edgesBetween(the_Vertices_of G2) = the_Edges_of G1
proof
let G2, V;
let G1 be addVertices of G2, V;
set E1 = the_Edges_of G1;
set V2 = the_Vertices_of G2;
for e being object holds e in E1 iff
e in G1.edgesInto(V2) /\ G1.edgesOutOf(V2)
proof
let e be object;
hereby
assume A1: e in the_Edges_of G1;
then A2: e in the_Edges_of G2 by Def10;
then A3: (the_Source_of G2).e in V2 & (the_Target_of G2).e in V2
by FUNCT_2:5;
reconsider e1=e as set by TARSKI:1;
(the_Source_of G1).e1 in V2 & (the_Target_of G1).e1 in V2
by A2, A3, Def9;
then e1 in G1.edgesInto(V2) & e1 in G1.edgesOutOf(V2)
by A1, GLIB_000:def 26, GLIB_000:def 27;
hence e in G1.edgesInto(V2) /\ G1.edgesOutOf(V2) by XBOOLE_0:def 4;
end;
thus thesis;
end;
then E1 = G1.edgesInto(V2) /\ G1.edgesOutOf(V2) by TARSKI:2;
hence thesis by GLIB_000:def 29;
end;
theorem
for G3 being _Graph, V1, V2 being set, G2 being addVertices of G3, V2,
G1 being addVertices of G2, V1
holds G1 is addVertices of G3, V1 \/ V2
proof
let G3 be _Graph, V1, V2 be set;
let G2 be addVertices of G3, V2;
let G1 be addVertices of G2, V1;
A1: the_Vertices_of G1 = (the_Vertices_of G2) \/ V1 &
the_Edges_of G1 = the_Edges_of G2 &
the_Source_of G1 = the_Source_of G2 &
the_Target_of G1 = the_Target_of G2 by Def10;
the_Vertices_of G2 = (the_Vertices_of G3) \/ V2 &
the_Edges_of G2 = the_Edges_of G3 &
the_Source_of G2 = the_Source_of G3 &
the_Target_of G2 = the_Target_of G3 by Def10;
then A3: the_Vertices_of G1 = the_Vertices_of G3 \/ (V1 \/ V2)
by A1, XBOOLE_1:4;
A4: the_Edges_of G1 = the_Edges_of G3 by A1, Def10;
A5: the_Source_of G1 = the_Source_of G3 by A1, Def10;
A6: the_Target_of G1 = the_Target_of G3 by A1, Def10;
G1 is Supergraph of G3 by Th66;
hence thesis by A3, A4, A5, A6, Def10;
end;
theorem
for G3 being _Graph, V1, V2 being set, G1 being addVertices of G3, V1 \/ V2
holds ex G2 being addVertices of G3, V2 st G1 is addVertices of G2, V1
proof
let G3 be _Graph, V1, V2 be set;
let G1 be addVertices of G3, V1 \/ V2;
set G2 = the addVertices of G3, V2;
take G2;
A1: the_Vertices_of G2 = (the_Vertices_of G3) \/ V2 &
the_Edges_of G2 = the_Edges_of G3 &
the_Source_of G2 = the_Source_of G3 &
the_Target_of G2 = the_Target_of G3 by Def10;
A2: the_Vertices_of G1 = (the_Vertices_of G3) \/ (V1 \/ V2) &
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 Def10;
(the_Vertices_of G3) \/ V2 c= (the_Vertices_of G3) \/ (V1 \/ V2)
by XBOOLE_1:7, XBOOLE_1:9;
then A4: the_Vertices_of G2 c= the_Vertices_of G1 by A1, Def10;
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 A1, A2;
then A5: G1 is Supergraph of G2 by A1, A2, A4, Def9;
the_Vertices_of G1 = (the_Vertices_of G3 \/ V2) \/ V1 by A2, XBOOLE_1:4
.= the_Vertices_of G2 \/ V1 by Def10;
hence thesis by A1, A2, A5, Def10;
end;
theorem Th88:
for G2, V for G1 being addVertices of G2, V
holds G2 is inducedSubgraph of G1, the_Vertices_of G2
proof
let G2, V;
let G1 be addVertices of G2, V;
set V2 = the_Vertices_of G2;
reconsider G3=G2 as Subgraph of G1 by Th61;
A2: the_Vertices_of G3 = V2;
A3: the_Edges_of G3 = the_Edges_of G1 by Def10
.= G1.edgesBetween(V2) by Th85;
thus G2 is inducedSubgraph of G1, V2 by A2, A3, GLIB_000:def 37;
end;
theorem Th89:
for G2, V for G1 being addVertices of G2, V
for x,y,e being object holds e DJoins x,y,G1 iff e DJoins x,y,G2
proof
let G2, V;
let G1 be addVertices of G2, V;
let x,y,e be object;
hereby
assume e DJoins x,y,G1;
then e in the_Edges_of G1 &
(the_Source_of G1).e = x & (the_Target_of G1).e = y by GLIB_000:def 14;
then e in the_Edges_of G2 &
(the_Source_of G2).e = x & (the_Target_of G2).e = y by Def10;
hence e DJoins x,y,G2 by GLIB_000:def 14;
end;
assume e DJoins x,y,G2;
then e in the_Edges_of G2 &
(the_Source_of G2).e = x & (the_Target_of G2).e = y by GLIB_000:def 14;
then e in the_Edges_of G1 &
(the_Source_of G1).e = x & (the_Target_of G1).e = y by Def10;
hence e DJoins x,y,G1 by GLIB_000:def 14;
end;
theorem Th90:
for G2, V for G1 being addVertices of G2, V, v being object
st v in V holds v is Vertex of G1
proof
let G2, V;
let G1 be addVertices of G2, V;
let v be object;
assume v in V;
then v in V \/ the_Vertices_of G2 by XBOOLE_0:def 3;
hence thesis by Def10;
end;
theorem Th91:
for G2, V for G1 being addVertices of G2, V
for x,y,e being object holds e Joins x,y,G1 iff e Joins x,y,G2
proof
let G2, V;
let G1 be addVertices of G2, V;
let x,y,e be object;
e Joins x,y,G1 iff (e DJoins x,y,G1 or e DJoins y,x,G1) by GLIB_000:16;
then e Joins x,y,G1 iff (e DJoins x,y,G2 or e DJoins y,x,G2) by Th89;
hence thesis by GLIB_000:16;
end;
theorem Th92:
for G2, V for G1 being addVertices of G2, V, v being Vertex of G1
st v in V \ the_Vertices_of G2 holds v is isolated non cut-vertex
proof
let G2, V;
let G1 be addVertices of G2, V;
let v be Vertex of G1;
assume A1: v in V \ the_Vertices_of G2;
v.edgesInOut() = {}
proof
assume v.edgesInOut() <> {};
then consider e being object such that
A2: e in v.edgesInOut() by XBOOLE_0:def 1;
e in the_Edges_of G1 by A2;
then A3: e in the_Edges_of G2 by Def10;
per cases by A2, GLIB_000:61;
suppose (the_Source_of G1).e = v;
then (the_Source_of G2).e = v by Def10;
then v in the_Vertices_of G2 by A3, FUNCT_2:5;
hence contradiction by A1, XBOOLE_0:def 5;
end;
suppose (the_Target_of G1).e = v;
then (the_Target_of G2).e = v by Def10;
then v in the_Vertices_of G2 by A3, FUNCT_2:5;
hence contradiction by A1, XBOOLE_0:def 5;
end;
end;
hence v is isolated by GLIB_000:def 49;
hence v is non cut-vertex;
end;
theorem Th93:
for G2, V for G1 being addVertices of G2, V
st V \ the_Vertices_of G2 <> {}
holds G1 is non _trivial non connected non Tree-like non complete
proof
let G2, V;
let G1 be addVertices of G2, V;
assume V \ the_Vertices_of G2 <> {};
then consider v1 being object such that
A2: v1 in V \ the_Vertices_of G2 by XBOOLE_0:def 1;
A3: v1 in V & not v1 in the_Vertices_of G2 by A2, XBOOLE_0:def 5;
then v1 in the_Vertices_of G2 \/ V by XBOOLE_0:def 3;
then reconsider v1 as Vertex of G1 by Def10;
set v2 = the Vertex of G2;
v1 <> v2 by A3;
then A5: card {v1, v2} = 2 by CARD_2:57;
v2 in the_Vertices_of G2 \/ V by XBOOLE_0:def 3;
then v2 in the_Vertices_of G1 by Def10;
then A6: 2 c= card the_Vertices_of G1 by A5, CARD_1:11, ZFMISC_1:32;
card the_Vertices_of G1 <> 1
proof
assume card the_Vertices_of G1 = 1;
then 1 in 1 by A6, CARD_2:69;
hence contradiction;
end;
hence A7: G1 is non _trivial by GLIB_000:def 19;
v1 is isolated by A2, Th92;
hence G1 is non connected non Tree-like non complete by A7, GLIB_002:2;
end;
registration
let G be non-Dmulti _Graph;
let V be set;
cluster -> non-Dmulti for addVertices of G, V;
coherence
proof
let G2 be addVertices of G, V;
for e1,e2,v1,v2 being object holds
e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 implies e1 = e2
proof
let e1,e2,v1,v2 be object;
assume e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2;
then e1 DJoins v1,v2,G & e2 DJoins v1,v2,G by Th89;
hence thesis by GLIB_000:def 21;
end;
hence thesis by GLIB_000:def 21;
end;
end;
registration
let G be non-multi _Graph;
let V be set;
cluster -> non-multi for addVertices of G, V;
coherence
proof
let G2 be addVertices of G, V;
for e1,e2,v1,v2 being object holds
e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 implies e1 = e2
proof
let e1,e2,v1,v2 be object;
assume e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2;
then e1 Joins v1,v2,G & e2 Joins v1,v2,G by Th91;
hence thesis by GLIB_000:def 20;
end;
hence thesis by GLIB_000:def 20;
end;
end;
registration
let G be loopless _Graph;
let V be set;
cluster -> loopless for addVertices of G, V;
coherence
proof
let G2 be addVertices of G, V;
for v being object holds not ex e being object st e Joins v,v,G2
proof
let v be object;
given e being object such that
A2: e Joins v,v,G2;
e DJoins v,v,G2 by A2, GLIB_000:16;
then e DJoins v,v,G by Th89;
then e Joins v,v,G by GLIB_000:16;
hence contradiction by GLIB_000:18;
end;
hence thesis by GLIB_000:18;
end;
end;
registration
let G be Dsimple _Graph;
let V be set;
cluster -> Dsimple for addVertices of G, V;
coherence;
end;
registration
let G be Dsimple _Graph;
let V be set;
cluster -> Dsimple for addVertices of G, V;
coherence;
end;
theorem Th94:
for G2, V for G1 being addVertices of G2, V, W being Walk of G1
holds W.vertices() misses V \ the_Vertices_of G2 or W is trivial
proof
let G2, V;
let G1 be addVertices of G2, V, W be Walk of G1;
assume not W.vertices() misses V \ the_Vertices_of G2;
then W.vertices() /\ (V \ the_Vertices_of G2) <> {} by XBOOLE_0:def 7;
then consider v being object such that
A1: v in W.vertices() /\ (V \ the_Vertices_of G2) by XBOOLE_0:def 1;
v in W.vertices() & v in V \ the_Vertices_of G2 by A1, XBOOLE_0:def 4;
then A2: v in W.vertices() & v in V & not v in the_Vertices_of G2
by XBOOLE_0:def 5;
then consider n being odd Element of NAT such that
A3: n <= len W & W.n = v by GLIB_001:87;
per cases by A3, XXREAL_0:1;
suppose n < len W;
then per cases by GLIB_001:def 3, GLIB_000:16;
suppose W.(n+1) DJoins W.n,W.(n+2),G1;
then W.(n+1) DJoins W.n,W.(n+2),G2 by Th89;
then W.(n+1) in the_Edges_of G2 &
(the_Source_of G2).(W.(n+1)) = W.n by GLIB_000:def 14;
hence thesis by A2, A3, FUNCT_2:5;
end;
suppose W.(n+1) DJoins W.(n+2),W.n,G1;
then W.(n+1) DJoins W.(n+2),W.n,G2 by Th89;
then W.(n+1) in the_Edges_of G2 &
(the_Target_of G2).(W.(n+1)) = W.n by GLIB_000:def 14;
hence thesis by A2, A3, FUNCT_2:5;
end;
end;
suppose A4: n = len W;
per cases;
suppose n = 1;
hence thesis by A4, GLIB_001:126;
end;
suppose n <> 1;
then consider m being odd Nat such that
A5: m+2 = n by CHORD:5;
reconsider m as odd Element of NAT by ORDINAL1:def 12;
m < len W by A4, A5, NAT_D:47;
then per cases by GLIB_000:16, GLIB_001:def 3;
suppose W.(m+1) DJoins W.m,W.(m+2),G1;
then W.(m+1) DJoins W.m,W.(m+2),G2 by Th89;
then W.(m+1) in the_Edges_of G2 &
(the_Target_of G2).(W.(m+1)) = W.(m+2) by GLIB_000:def 14;
hence thesis by A2, A3, A5, FUNCT_2:5;
end;
suppose W.(m+1) DJoins W.(m+2),W.m,G1;
then W.(m+1) DJoins W.(m+2),W.m,G2 by Th89;
then W.(m+1) in the_Edges_of G2 &
(the_Source_of G2).(W.(m+1)) = W.(m+2) by GLIB_000:def 14;
hence thesis by A2, A3, A5, FUNCT_2:5;
end;
end;
end;
end;
theorem Th95:
for G2, V for G1 being addVertices of G2, V, W being Walk of G1
st W.vertices() misses V \ the_Vertices_of G2 holds W is Walk of G2
proof
let G2, V;
let G1 be addVertices of G2, V, W be Walk of G1;
A1: G2 is Subgraph of G1 by Th61;
assume A2: W.vertices() misses V \ the_Vertices_of G2;
the_Vertices_of G1 = the_Vertices_of G2 \/ V by Def10;
then A3: the_Vertices_of G1 = the_Vertices_of G2 \/ (V \ the_Vertices_of G2)
by XBOOLE_1:39;
A4: W.vertices() c= the_Vertices_of G2 by A2, A3, XBOOLE_1:73;
W.edges() c= the_Edges_of G1;
then W.edges() c= the_Edges_of G2 by Def10;
hence thesis by A1, A4, GLIB_001:170;
end;
registration
let G be acyclic _Graph;
let V be set;
cluster -> acyclic for addVertices of G, V;
coherence
proof
let G1 be addVertices of G, V;
not ex W1 being Walk of G1 st W1 is Cycle-like
proof
given W1 being Walk of G1 such that
A1: W1 is Cycle-like;
per cases by Th94;
suppose W1.vertices() misses V \ the_Vertices_of G;
then reconsider P = W1 as Walk of G by Th95;
P is Cycle-like by A1, Th80;
hence contradiction by GLIB_002:def 2;
end;
suppose W1 is trivial;
hence contradiction by A1;
end;
end;
hence thesis by GLIB_002:def 2;
end;
end;
theorem Th96:
for G2, V for G1 being addVertices of G2, V
holds G2 is chordal iff G1 is chordal
proof
let G2 be _Graph, V be set, G1 be addVertices of G2, V;
thus G2 is chordal implies G1 is chordal
proof
assume A1: G2 is chordal;
for P being Walk of G1 st
P.length() > 3 & P is Cycle-like holds P is chordal
proof
let P be Walk of G1;
assume A2: P.length() > 3 & P is Cycle-like;
per cases by Th94;
suppose P.vertices() misses V \ the_Vertices_of G2;
then reconsider W = P as Walk of G2 by Th95;
A3: W is Cycle-like by A2, Th80;
P.length() = W.length() by GLIB_001:114;
then W is chordal by A1, A2, A3, CHORD:def 11;
then consider m,n being odd Nat such that
A4: m+2 < n & n <= len W & W.m <> W.n and
A5: ex e being object st e Joins W.m,W.n,G2 and
A6: for f being object st f in W.edges() holds not f Joins W.m,W.n,G2
by CHORD:def 10;
now
take m, n;
thus m+2 < n & n <= len P & P.m <> P.n by A4;
thus ex e being object st e Joins P.m,P.n,G1 by A5, Th74;
thus for f being object st f in P.edges() holds
not f Joins P.m,P.n,G1
proof
given f being object such that
A7: f in P.edges() and
A8: f Joins P.m,P.n,G1;
A9: f in W.edges() by A7, GLIB_001:110;
per cases by A8, GLIB_000:16;
suppose f DJoins P.m,P.n,G1;
then per cases by Th75;
suppose f DJoins P.m,P.n,G2;
then f Joins W.m,W.n,G2 by GLIB_000:16;
hence contradiction by A6, A9;
end;
suppose not f in the_Edges_of G2;
hence contradiction by A9;
end;
end;
suppose f DJoins P.n,P.m,G1;
then per cases by Th75;
suppose f DJoins P.n,P.m,G2;
then f Joins W.m,W.n,G2 by GLIB_000:16;
hence contradiction by A6, A9;
end;
suppose not f in the_Edges_of G2;
hence contradiction by A9;
end;
end;
end;
end;
hence P is chordal by CHORD:def 10;
end;
suppose P is trivial;
hence thesis by A2;
end;
end;
hence thesis by CHORD:def 11;
end;
assume A10: G1 is chordal;
G2 is inducedSubgraph of G1, the_Vertices_of G2 by Th88;
hence thesis by A10;
end;
:: "non"-version of this cluster has to wait
:: because non chordal existence will be proven with cycle graphs
registration
let G be chordal _Graph;
let V be set;
cluster -> chordal for addVertices of G, V;
coherence by Th96;
end;
reserve v for object;
definition
let G, v;
mode addVertex of G, v is addVertices of G, {v};
end;
theorem
for G2, v for G1 being addVertex of G2, v
holds G1 == G2 iff v in the_Vertices_of G2 by Th82, ZFMISC_1:31;
theorem Th98:
for G2, v for G1 being addVertex of G2, v holds v is Vertex of G1
proof
let G2, v;
let G1 be addVertex of G2, v;
v in {v} by TARSKI:def 1;
hence thesis by Th90;
end;
Lm1:
for X being set holds {X} \ X <> {}
proof
let X be set;
assume {X} \ X = {};
then X in X by ZFMISC_1:60;
hence contradiction;
end;
registration
let G;
cluster -> non _trivial non connected non complete
for addVertex of G, the_Vertices_of G;
coherence
proof
let G1 be addVertex of G, the_Vertices_of G;
{the_Vertices_of G} \ the_Vertices_of G <> {} by Lm1;
hence thesis by Th93;
end;
end;
:: the prime example of how to use the new modes to show existences
:: of certain graphs
registration
cluster non _trivial non connected non complete for _Graph;
existence
proof
set G0 = the _Graph;
set G = the addVertex of G0, the_Vertices_of G0;
take G;
thus thesis;
end;
end;
registration
let G be non connected _Graph, V be set;
cluster -> non connected for addVertices of G, V;
coherence
proof
let G1 be addVertices of G, V;
ex u1,v1 being Vertex of G1 st for W being Walk of G1 holds
not W is_Walk_from u1,v1
proof
consider u,v being Vertex of G such that
A1: for W being Walk of G holds not W is_Walk_from u,v
by GLIB_002:def 1;
reconsider u1=u,v1=v as Vertex of G1 by Th72;
take u1,v1;
let W be Walk of G1;
assume A2: W is_Walk_from u1,v1;
per cases by Th94;
suppose W.vertices() misses V \ the_Vertices_of G;
then reconsider W2 = W as Walk of G by Th95;
W2 is_Walk_from u,v by A2, GLIB_001:19;
hence contradiction by A1;
end;
suppose W is trivial;
then consider w being Vertex of G1 such that
A4: W = G1.walkOf(w) by GLIB_001:128;
W.first() = u1 & W.last() = v1 by A2, GLIB_001:def 23;
then u1 = w & v1 = w by A4, GLIB_001:13;
then G.walkOf(v) is_Walk_from u,v by GLIB_001:13;
hence contradiction by A1;
end;
end;
hence thesis by GLIB_002:def 1;
end;
end;
:: In general, non finite versions of cardinalities are missing in the
:: graph construction modes of GLIB_000 (e.g. removeVertex) and should
:: be added.
theorem Th99:
for G2, V for G1 being addVertices of G2, V
holds G1.size() = G2.size() &
G1.order() = G2.order() +` card (V \ the_Vertices_of G2)
proof
let G2, V;
let G1 be addVertices of G2, V;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= card the_Edges_of G2 by Def10
.= G2.size() by GLIB_000:def 25;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= card (the_Vertices_of G2 \/ V) by Def10
.= card (the_Vertices_of G2 \/ (V \ the_Vertices_of G2)) by XBOOLE_1:39
.= card the_Vertices_of G2 +` card (V \ the_Vertices_of G2)
by XBOOLE_1:79, CARD_2:35
.= G2.order() +` card (V \ the_Vertices_of G2) by GLIB_000:def 24;
end;
theorem Th100:
for G2 being _finite _Graph, V being finite set, G1 being addVertices of G2,V
holds G1.order() = G2.order() + card (V \ the_Vertices_of G2)
proof
let G2 be _finite _Graph, V be finite set, G1 be addVertices of G2,V;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= card (the_Vertices_of G2 \/ V) by Def10
.= card (the_Vertices_of G2 \/ (V \ the_Vertices_of G2)) by XBOOLE_1:39
.= card the_Vertices_of G2 + card (V \ the_Vertices_of G2)
by XBOOLE_1:79, CARD_2:40
.= G2.order() + card (V \ the_Vertices_of G2) by GLIB_000:def 24;
end;
theorem
for G2 being _Graph, v being object, G1 being addVertex of G2,v
st not v in the_Vertices_of G2 holds G1.order() = G2.order() +` 1
proof
let G2 be _Graph, v be object, G1 be addVertex of G2,v;
assume not v in the_Vertices_of G2;
then card ({v} \ the_Vertices_of G2) = 1 by ZFMISC_1:59, CARD_2:42;
hence thesis by Th99;
end;
theorem
for G2 being _finite _Graph, v being object, G1 being addVertex of G2,v
st not v in the_Vertices_of G2 holds G1.order() = G2.order() + 1
proof
let G2 be _finite _Graph, v be object, G1 be addVertex of G2,v;
assume not v in the_Vertices_of G2;
then card ({v} \ the_Vertices_of G2) = 1 by ZFMISC_1:59, CARD_2:42;
hence thesis by Th100;
end;
registration
let G be _finite _Graph, V be finite set;
cluster -> _finite for addVertices of G, V;
coherence
proof
let G1 be addVertices of G, V;
the_Vertices_of G1 = the_Vertices_of G \/ V &
the_Edges_of G1 = the_Edges_of G by Def10;
hence thesis by GLIB_000:def 17;
end;
end;
registration
let G be _finite _Graph, v be object;
cluster -> _finite for addVertex of G, v;
coherence;
end;
registration
let G be _Graph, V be non finite set;
cluster -> non _finite for addVertices of G,V;
coherence
proof
let G1 be addVertices of G,V;
the_Vertices_of G1 = the_Vertices_of G \/ V by Def10;
hence thesis;
end;
end;
:: we explicitly add an edge only if it is not used already
:: to ensure getting a Supergraph
definition
let G;
let v1,e,v2 be object;
mode addEdge of G,v1,e,v2 -> Supergraph of G means
:Def11:
the_Vertices_of it = the_Vertices_of G &
the_Edges_of it = the_Edges_of G \/ {e} &
the_Source_of it = the_Source_of G +* (e .--> v1) &
the_Target_of it = the_Target_of G +* (e .--> v2)
if v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G
otherwise it == G;
existence
proof
hereby
assume A1: v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
set V1 = the_Vertices_of G;
set E1 = the_Edges_of G \/ {e};
A2: rng (e .--> v1) = rng ({e} --> v1) by FUNCOP_1:def 9
.= {v1} by FUNCOP_1:8;
A3: rng (e .--> v2) = rng ({e} --> v2) by FUNCOP_1:def 9
.= {v2} by FUNCOP_1:8;
A4: dom (e .--> v1) = dom ({e} --> v1) by FUNCOP_1:def 9
.= {e};
A5: dom (e .--> v2) = dom ({e} --> v2) by FUNCOP_1:def 9
.= {e};
set S1 = the_Source_of G +* (e .--> v1);
A6: dom S1 = (dom the_Source_of G) \/ dom (e .--> v1) by FUNCT_4:def 1
.= E1 by FUNCT_2:def 1, A4;
(rng the_Source_of G) \/ {v1} c= the_Vertices_of G \/ {v1}
by XBOOLE_1:9;
then A7: (rng the_Source_of G) \/ rng (e .--> v1) c= V1
by A1, A2, ZFMISC_1:40;
rng S1 c= (rng the_Source_of G) \/ rng (e .--> v1) by FUNCT_4:17;
then reconsider S1 as Function of E1, V1
by A6, A7, FUNCT_2:2, XBOOLE_1:1;
set T1 = the_Target_of G +* (e .--> v2);
A8: dom T1 = (dom the_Target_of G) \/ dom (e .--> v2) by FUNCT_4:def 1
.= E1 by FUNCT_2:def 1, A5;
(rng the_Target_of G) \/ {v2} c= the_Vertices_of G \/ {v2}
by XBOOLE_1:9;
then A9: (rng the_Target_of G) \/ rng (e .--> v2) c= V1
by A1, A3, ZFMISC_1:40;
rng T1 c= (rng the_Target_of G) \/ rng (e .--> v2) by FUNCT_4:17;
then reconsider T1 as Function of E1, V1
by A8, A9, FUNCT_2:2, XBOOLE_1:1;
set G1 = createGraph(V1,E1,S1,T1);
for e1 being set st e1 in the_Edges_of G holds
(the_Source_of G).e1 = (the_Source_of G1).e1 &
(the_Target_of G).e1 = (the_Target_of G1).e1
proof
let e1 be set;
assume e1 in the_Edges_of G;
then A12: not e1 in dom (e .--> v1) &
not e1 in dom (e .--> v2) by A1, TARSKI:def 1;
thus (the_Source_of G1).e1
= (the_Source_of G +* (e .--> v1)).e1
.= (the_Source_of G).e1 by A12, FUNCT_4:11;
thus (the_Target_of G1).e1
= (the_Target_of G +* (e .--> v2)).e1
.= (the_Target_of G).e1 by A12, FUNCT_4:11;
thus thesis;
end;
then reconsider G1 as Supergraph of G by Def9, XBOOLE_1:7;
take G1;
thus the_Vertices_of G1 = the_Vertices_of G &
the_Edges_of G1 = the_Edges_of G \/ {e} &
the_Source_of G1 = the_Source_of G +* (e .--> v1) &
the_Target_of G1 = the_Target_of G +* (e .--> v2);
end;
assume not (v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
reconsider G1 = G as Supergraph of G by Th65;
take G1;
thus thesis;
end;
consistency;
end;
theorem
for G for v1,e,v2 being object, G1, G2 being addEdge of G,v1,e,v2
holds G1 == G2
proof
let G;
let v1,e,v2 be object;
let G1, G2 be addEdge of G,v1,e,v2;
per cases;
suppose v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
then
the_Vertices_of G1 = the_Vertices_of G &
the_Edges_of G1 = the_Edges_of G \/ {e} &
the_Source_of G1 = the_Source_of G +* (e .--> v1) &
the_Target_of G1 = the_Target_of G +* (e .--> v2) &
the_Vertices_of G2 = the_Vertices_of G &
the_Edges_of G2 = the_Edges_of G \/ {e} &
the_Source_of G2 = the_Source_of G +* (e .--> v1) &
the_Target_of G2 = the_Target_of G +* (e .--> v2) by Def11;
hence thesis by GLIB_000:def 34;
end;
suppose not (v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G == G1 & G == G2 by Def11;
hence thesis by GLIB_000:85;
end;
end;
theorem
for G2 for v1, v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
holds G1 == G2 iff e in the_Edges_of G2
proof
let G2;
let v1, v2 be Vertex of G2;
let e be object;
let G1 be addEdge of G2,v1,e,v2;
hereby
assume G1 == G2;
then A1: the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
per cases;
suppose e in the_Edges_of G2;
hence e in the_Edges_of G2;
end;
suppose not e in the_Edges_of G2;
then the_Edges_of G2 \/ {e} c= the_Edges_of G2 by A1, Def11;
hence e in the_Edges_of G2 by ZFMISC_1:39;
end;
end;
thus thesis by Def11;
end;
theorem
for G, G2 for v1,e,v2 being object, G1 being addEdge of G,v1,e,v2
st G1 == G2 holds G2 is addEdge of G,v1,e,v2
proof
let G, G2;
let v1,e,v2 be object;
let G1 be addEdge of G,v1,e,v2;
assume A1: G1 == G2;
per cases;
suppose A2: v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
then the_Vertices_of G1 = the_Vertices_of G &
the_Edges_of G1 = the_Edges_of G \/ {e} &
the_Source_of G1 = the_Source_of G +* (e .--> v1) &
the_Target_of G1 = the_Target_of G +* (e .--> v2) by Def11;
then A3: the_Vertices_of G2 = the_Vertices_of G &
the_Edges_of G2 = the_Edges_of G \/ {e} &
the_Source_of G2 = the_Source_of G +* (e .--> v1) &
the_Target_of G2 = the_Target_of G +* (e .--> v2) by A1, GLIB_000:def 34;
G2 is Supergraph of G1 by A1, Th62;
then G2 is Supergraph of G by Th66;
hence thesis by A2, A3, Def11;
end;
suppose A4: not (v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G == G1 by Def11;
then A5: G == G2 by A1, GLIB_000:85;
then G2 is Supergraph of G by Th62;
hence thesis by A4, A5, Def11;
end;
end;
theorem Th106:
for G2 for v1, v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
holds the_Vertices_of G1 = the_Vertices_of G2
proof
let G2;
let v1, v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
per cases;
suppose not e in the_Edges_of G2;
hence thesis by Def11;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by Def11;
hence thesis by GLIB_000:def 34;
end;
end;
theorem
for G2 for v1, v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
holds G1.edgesBetween(the_Vertices_of G2) = the_Edges_of G1
proof
let G2;
let v1, v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
thus G1.edgesBetween(the_Vertices_of G2)
= G1.edgesBetween(the_Vertices_of G1) by Th106
.= the_Edges_of G1 by GLIB_000:34;
end;
theorem Th108:
for G2 for v1, v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
for v being Vertex of G1 holds v is Vertex of G2
proof
let G2;
let v1, v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
let v be Vertex of G1;
per cases;
suppose not e in the_Edges_of G2;
hence thesis by Def11;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by Def11;
hence thesis by GLIB_000:def 34;
end;
end;
theorem Th109:
for G2 for v1, v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
holds not e in the_Edges_of G2 implies e DJoins v1,v2,G1
proof
let G2;
let v1, v2 be Vertex of G2;
let e be object;
let G1 be addEdge of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2;
e in {e} by TARSKI:def 1;
then e in the_Edges_of G2 \/ {e} by XBOOLE_0:def 3;
then A2: e in the_Edges_of G1 by A1, Def11;
A3: e in dom (e .--> v1) by FUNCOP_1:74;
A4: (the_Source_of G1).e
= (the_Source_of G2 +* (e .--> v1)).e by A1, Def11
.= (e .--> v1).e by A3, FUNCT_4:13
.= v1 by FUNCOP_1:72;
A5: e in dom (e .--> v2) by FUNCOP_1:74;
(the_Target_of G1).e
= (the_Target_of G2 +* (e .--> v2)).e by A1, Def11
.= (e .--> v2).e by A5, FUNCT_4:13
.= v2 by FUNCOP_1:72;
hence thesis by A2, A4, GLIB_000:def 14;
end;
theorem Th110:
for G2 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
for e1,w1,w2 being object
holds e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 implies e1 = e
proof
let G2;
let v1,v2 be Vertex of G2, e be object, G1 be addEdge of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2;
let e1,w1,w2 be object;
assume A2: e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2;
then A3: e1 in the_Edges_of G1 by GLIB_000:def 13;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, Def11;
then e1 in {e} by A3, A2, XBOOLE_0:def 3;
hence e1 = e by TARSKI:def 1;
end;
theorem
for G2 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
for e1,w1,w2 being object
holds e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2
implies (w1 = v1 & w2 = v2) or (w1 = v2 & w2 = v1)
proof
let G2;
let v1,v2 be Vertex of G2, e be object, G1 be addEdge of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2;
let e1,w1,w2 be object;
assume A2: e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2;
then A3: e = e1 by A1, Th110;
e DJoins v1,v2,G1 by A1, Th109;
then e1 Joins v1,v2,G1 by A3, GLIB_000:16;
hence thesis by A2, GLIB_000:15;
end;
theorem Th112:
for G2 for v1, v2 being Vertex of G2, e being set
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2
holds G2 is removeEdge of G1,e
proof
let G2;
let v1, v2 be Vertex of G2, e be set;
let G1 be addEdge of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ {e} &
the_Source_of G1 = the_Source_of G2 +* (e .--> v1) &
the_Target_of G1 = the_Target_of G2 +* (e .--> v2) by Def11;
then A3: the_Edges_of G1 \ {e}
= the_Edges_of G2 by A1, ZFMISC_1:117;
the_Vertices_of G1 is non empty & the_Vertices_of G1 c= the_Vertices_of G1;
then reconsider V = the_Vertices_of G1
as non empty Subset of the_Vertices_of G1;
A4: G2 is Subgraph of G1 by Th61;
the_Edges_of G1 \ {e} c= the_Edges_of G1;
then the_Edges_of G1 \ {e} c= G1.edgesBetween(V)
by GLIB_000:34;
hence thesis by A2, A3, A4, GLIB_000:def 37;
end;
theorem Th113:
for G2 for v1, v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2, W being Walk of G1
st (e in W.edges() implies e in the_Edges_of G2)
holds W is Walk of G2
proof
let G2;
let v1, v2 be Vertex of G2;
let e be object;
let G1 be addEdge of G2,v1,e,v2;
let W be Walk of G1;
assume e in W.edges() implies e in the_Edges_of G2;
then per cases;
suppose not e in W.edges();
then A1: W.edges() misses {e} by ZFMISC_1:50;
A2: G2 is Subgraph of G1 by Th61;
per cases;
suppose A3: not e in the_Edges_of G2;
W.edges() c= the_Edges_of G1;
then W.edges() c= the_Edges_of G2 \/ {e} by A3, Def11;
then A4: W.edges() c= the_Edges_of G2 by A1, XBOOLE_1:73;
W.vertices() c= the_Vertices_of G1;
then W.vertices() c= the_Vertices_of G2 by A3, Def11;
hence thesis by A2, A4, GLIB_001:170;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by Def11;
hence thesis by GLIB_001:179;
end;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by Def11;
hence thesis by GLIB_001:179;
end;
end;
registration
let G be _trivial _Graph;
let v1,e,v2 be object;
cluster -> _trivial for addEdge of G,v1,e,v2;
coherence
proof
let G1 be addEdge of G,v1,e,v2;
per cases;
suppose v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
then A1: the_Vertices_of G = the_Vertices_of G1 by Def11;
card the_Vertices_of G = 1 by GLIB_000:def 19;
hence thesis by A1, GLIB_000:def 19;
end;
suppose not (v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def11;
hence thesis by GLIB_000:89;
end;
end;
end;
registration
let G be connected _Graph;
let v1,e,v2 be object;
cluster -> connected for addEdge of G,v1,e,v2;
coherence
proof
let G1 be addEdge of G,v1,e,v2;
per cases;
suppose A1: v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
for u,v being Vertex of G1 holds
ex W being Walk of G1 st W is_Walk_from u,v
proof
let u,v be Vertex of G1;
reconsider u1=u, v1=v as Vertex of G by A1, Def11;
consider W1 being Walk of G such that
A2: W1 is_Walk_from u1, v1 by GLIB_002:def 1;
G is Subgraph of G1 by Th61;
then reconsider W=W1 as Walk of G1 by GLIB_001:167;
W1.first() = u1 & W1.last() = v1 by A2, GLIB_001:def 23;
then W.first() = u & W.last() = v by GLIB_001:16;
hence thesis by GLIB_001:def 23;
end;
hence thesis by GLIB_002:def 1;
end;
suppose not (v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def11;
hence thesis by GLIB_002:8;
end;
end;
end;
registration
let G be complete _Graph;
let v1,e,v2 be object;
cluster -> complete for addEdge of G,v1,e,v2;
coherence
proof
let G1 be addEdge of G,v1,e,v2;
per cases;
suppose A1: v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
for u,v being Vertex of G1 st u <> v holds u, v are_adjacent
proof
let u,v be Vertex of G1;
assume A2: u <> v;
reconsider u1=u, v1=v as Vertex of G by A1, Def11;
consider e1 being object such that
A3: e1 Joins u1,v1,G by A2, CHORD:def 6, CHORD:def 3;
reconsider u1, v1 as set;
thus u,v are_adjacent by A3, Th74, CHORD:def 3;
end;
hence thesis by CHORD:def 6;
end;
suppose not (v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def11;
hence thesis by CHORD:62;
end;
end;
end;
theorem
for G2 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
holds G1.order() = G2.order() & G1.size() = G2.size() +` 1
proof
let G2;
let v1,v2 be Vertex of G2, e being object;
let G1 be addEdge of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by Def11;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= G2.order() by A2, GLIB_000:def 24;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= card the_Edges_of G2 +` card {e} by A1, A2, CARD_2:35, ZFMISC_1:50
.= G2.size() +` card {e} by GLIB_000:def 25
.= G2.size() +` 1 by CARD_2:42;
end;
theorem
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
holds G1.size() = G2.size() + 1
proof
let G2 be _finite _Graph;
let v1,v2 be Vertex of G2, e being object;
let G1 be addEdge of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2;
then A2: the_Edges_of G1 = the_Edges_of G2 \/ {e} by Def11;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= card the_Edges_of G2 + card {e} by A1, A2, CARD_2:40, ZFMISC_1:50
.= G2.size() + card {e} by GLIB_000:def 25
.= G2.size() + 1 by CARD_2:42;
end;
registration
let G be _finite _Graph;
let v1,e,v2 be object;
cluster -> _finite for addEdge of G,v1,e,v2;
coherence
proof
let G1 be addEdge of G,v1,e,v2;
per cases;
suppose v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
then the_Vertices_of G1 = the_Vertices_of G &
the_Edges_of G1 = the_Edges_of G \/ {e} by Def11;
hence thesis by GLIB_000:def 17;
end;
suppose not (v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def11;
hence thesis by GLIB_000:89;
end;
end;
end;
theorem Th116:
for G2 for v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is loopless & v1 <> v2
holds G1 is loopless
proof
let G2;
let v1, v2 be Vertex of G2;
let e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: G2 is loopless and
A2: v1 <> v2;
per cases;
suppose e in the_Edges_of G2;
then G1 == G2 by Def11;
hence thesis by A1, GLIB_000:89;
end;
suppose A3: not e in the_Edges_of G2;
not ex e1 being object st e1 in the_Edges_of G1 &
(the_Source_of G1).e1 = (the_Target_of G1).e1
proof
given e1 being object such that
A4: e1 in the_Edges_of G1 and
A5: (the_Source_of G1).e1 = (the_Target_of G1).e1;
per cases;
suppose A6: e1 in the_Edges_of G2;
reconsider e1 as set by TARSKI:1;
(the_Source_of G1).e1 = (the_Source_of G2).e1 &
(the_Target_of G1).e1 = (the_Target_of G2).e1 by A6, Def9;
hence contradiction by A1, A5, A6, GLIB_000:def 18;
end;
suppose A7: not e1 in the_Edges_of G2;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A3, Def11;
then e1 in {e} by A4, A7, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 DJoins v1,v2,G1 by A7, Th109;
then (the_Source_of G1).e1 = v1 & (the_Target_of G1).e1 = v2
by GLIB_000:def 14;
hence contradiction by A2, A5;
end;
end;
hence thesis by GLIB_000:def 18;
end;
end;
theorem Th117:
for G2 for v being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,v
st G2 is non loopless or not e in the_Edges_of G2
holds G1 is non loopless
proof
let G2;
let v be Vertex of G2,e be object;
let G1 be addEdge of G2,v,e,v;
assume G2 is non loopless or not e in the_Edges_of G2;
then per cases;
suppose G2 is non loopless;
hence G1 is non loopless;
end;
suppose not e in the_Edges_of G2;
then e DJoins v,v,G1 by Th109;
then e in the_Edges_of G1 & (the_Source_of G1).e = v &
(the_Target_of G1).e = v by GLIB_000:def 14;
hence thesis by GLIB_000:def 18;
end;
end;
registration
let G;
let v be Vertex of G;
cluster -> non loopless for addEdge of G,v,the_Edges_of G,v;
coherence
proof
let G1 be addEdge of G,v,the_Edges_of G,v;
not the_Edges_of G in the_Edges_of G;
hence thesis by Th117;
end;
end;
theorem Th118:
for G2 for v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
st G2 is non-Dmulti & not ex e3 being object st e3 DJoins v1,v2,G2
holds G1 is non-Dmulti
proof
let G2;
let v1,v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: G2 is non-Dmulti and
A2: not ex e3 being object st e3 DJoins v1,v2,G2;
per cases;
suppose A3: v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
for e1,e2,w1,w2 being object holds e1 DJoins
w1,w2,G1 & e2 DJoins w1,w2,G1 implies e1 = e2
proof
let e1,e2,w1,w2 be object;
assume that
A4: e1 DJoins w1,w2,G1 and
A5: e2 DJoins w1,w2,G1;
A6: the_Edges_of G1 = the_Edges_of G2 \/ {e} by A3, Def11;
per cases by A4, Th75;
suppose A7: e1 DJoins w1,w2,G2;
per cases by A5, Th75;
suppose e2 DJoins w1,w2,G2;
hence thesis by A7, A1, GLIB_000:def 21;
end;
suppose A8: not e2 in the_Edges_of G2;
e2 in the_Edges_of G1 by A5, GLIB_000:def 14;
then e2 in {e} by A8, A6, XBOOLE_0:def 3;
then e2 = e by TARSKI:def 1;
then e2 DJoins v1,v2,G1 by A8, Th109;
then (the_Source_of G1).e2 = v1 & (the_Target_of G1).e2 = v2
by GLIB_000:def 14;
then v1=w1 & v2=w2 by A5, GLIB_000:def 14;
hence thesis by A2, A7;
end;
end;
suppose A10: not e1 in the_Edges_of G2;
e1 in the_Edges_of G1 by A4, GLIB_000:def 14;
then e1 in {e} by A10, A6, XBOOLE_0:def 3;
then A11: e1 = e by TARSKI:def 1;
per cases by A5, Th75;
suppose A12: e2 DJoins w1,w2,G2;
e1 DJoins v1,v2,G1 by A10, A11, Th109;
then (the_Source_of G1).e1 = v1 & (the_Target_of G1).e1 = v2
by GLIB_000:def 14;
then v1=w1 & v2=w2 by A4, GLIB_000:def 14;
hence thesis by A2, A12;
end;
suppose A13: not e2 in the_Edges_of G2;
e2 in the_Edges_of G1 by A5, GLIB_000:def 14;
then e2 in {e} by A13, A6, XBOOLE_0:def 3;
hence thesis by A11, TARSKI:def 1;
end;
end;
end;
hence thesis by GLIB_000:def 21;
end;
suppose not(v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2);
then G1 == G2 by Def11;
hence thesis by A1, GLIB_000:89;
end;
end;
theorem
for G2 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 & ex e2 being object st e2 DJoins v1,v2,G2
holds G1 is non non-Dmulti
proof
let G2;
let v1,v2 be Vertex of G2;
let e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: not e in the_Edges_of G2 and
A2: ex e2 being object st e2 DJoins v1,v2,G2;
ex e1,e2,u1,u2 being object st e1 DJoins u1,u2,G1 & e2 DJoins u1,u2,G1
& e1 <> e2
proof
consider e2 being object such that
A3: e2 DJoins v1,v2,G2 by A2;
take e,e2,v1,v2;
thus e DJoins v1,v2,G1 by A1, Th109;
thus e2 DJoins v1,v2,G1 by A3, Th74;
thus e <> e2 by A1, A3, GLIB_000:def 14;
end;
hence thesis by GLIB_000:def 21;
end;
theorem Th120:
for G2 for v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
st G2 is non-multi & not v1,v2 are_adjacent
holds G1 is non-multi
proof
let G2;
let v1,v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: G2 is non-multi and
A2: not v1,v2 are_adjacent;
per cases;
suppose A3: v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
for e1,e2,w1,w2 being object holds e1 Joins
w1,w2,G1 & e2 Joins w1,w2,G1 implies e1 = e2
proof
let e1,e2,w1,w2 be object;
assume that
A4: e1 Joins w1,w2,G1 and
A5: e2 Joins w1,w2,G1;
A6: the_Edges_of G1 = the_Edges_of G2 \/ {e} by A3, Def11;
per cases by A4, Th76;
suppose A7: e1 Joins w1,w2,G2;
per cases by A5, Th76;
suppose e2 Joins w1,w2,G2;
hence thesis by A7, A1, GLIB_000:def 20;
end;
suppose A8: not e2 in the_Edges_of G2;
e2 in the_Edges_of G1 by A5, GLIB_000:def 13;
then e2 in {e} by A8, A6, XBOOLE_0:def 3;
then e2 = e by TARSKI:def 1;
then A10: e2 DJoins v1,v2,G1 by A8, Th109;
per cases by A5, GLIB_000:16;
suppose e2 DJoins w1,w2,G1;
then (the_Source_of G1).e2 = w1 & (the_Target_of G1).e2 = w2
by GLIB_000:def 14;
then w1=v1 & w2=v2 by A10, GLIB_000:def 14;
hence thesis by A2, A7, CHORD:def 3;
end;
suppose e2 DJoins w2,w1,G1;
then (the_Source_of G1).e2 = w2 & (the_Target_of G1).e2 = w1
by GLIB_000:def 14;
then w2=v1 & w1=v2 by A10, GLIB_000:def 14;
hence thesis by A2, A7, CHORD:def 3;
end;
end;
end;
suppose A11: not e1 in the_Edges_of G2;
e1 in the_Edges_of G1 by A4, GLIB_000:def 13;
then e1 in {e} by A11, A6, XBOOLE_0:def 3;
then A12: e1 = e by TARSKI:def 1;
then A13: e1 DJoins v1,v2,G1 by A11, Th109;
per cases by A5, Th76;
suppose A14: e2 Joins w1,w2,G2;
per cases by A4, GLIB_000:16;
suppose e1 DJoins w1,w2,G1;
then (the_Source_of G1).e1 = w1 & (the_Target_of G1).e1 = w2
by GLIB_000:def 14;
then w1=v1 & w2=v2 by A13, GLIB_000:def 14;
hence thesis by A2, A14, CHORD:def 3;
end;
suppose e1 DJoins w2,w1,G1;
then (the_Source_of G1).e1 = w2 & (the_Target_of G1).e1 = w1
by GLIB_000:def 14;
then w2=v1 & w1=v2 by A13, GLIB_000:def 14;
hence thesis by A2, A14, CHORD:def 3;
end;
end;
suppose A15: not e2 in the_Edges_of G2;
e2 in the_Edges_of G1 by A5, GLIB_000:def 13;
then e2 in {e} by A15, A6, XBOOLE_0:def 3;
hence thesis by A12, TARSKI:def 1;
end;
end;
end;
hence thesis by GLIB_000:def 20;
end;
suppose not (v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2);
then G1 == G2 by Def11;
hence thesis by A1, GLIB_000:89;
end;
end;
theorem
for G2 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 & v1,v2 are_adjacent
holds G1 is non non-multi
proof
let G2;
let v1,v2 be Vertex of G2;
let e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: not e in the_Edges_of G2 and
A2: v1,v2 are_adjacent;
ex e1,e2,u1,u2 being object st e1 Joins u1,u2,G1 & e2 Joins u1,u2,G1
& e1 <> e2
proof
consider e1 being object such that
A3: e1 Joins v1,v2,G2 by A2, CHORD:def 3;
take e1,e,v1,v2;
thus e1 Joins v1,v2,G1 by A3, Th74;
e DJoins v1,v2,G1 by A1, Th109;
hence e Joins v1,v2,G1 by GLIB_000:16;
thus e1 <> e by A1, A3, GLIB_000:def 13;
end;
hence thesis by GLIB_000:def 20;
end;
theorem Th122:
for G2 for v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
st G2 is acyclic & not v2 in G2.reachableFrom v1
holds G1 is acyclic
proof
let G2;
let v1,v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: G2 is acyclic and
A2: not v2 in G2.reachableFrom v1;
per cases;
suppose A3: v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
not ex W1 being Walk of G1 st W1 is Cycle-like
proof
given W1 being Walk of G1 such that
A4: W1 is Cycle-like;
A5: G2 is Subgraph of G1 by Th61;
A6: the_Vertices_of G1 = the_Vertices_of G2 by A3, Def11;
then A7: W1.vertices() c= the_Vertices_of G2;
per cases;
suppose W1.edges() c= the_Edges_of G2;
then reconsider W=W1 as Walk of G2 by A5, A7, GLIB_001:170;
W is Cycle-like by A4, A5, Th58;
hence contradiction by A1, GLIB_002:def 2;
end;
suppose not W1.edges() c= the_Edges_of G2;
then consider e1 being object such that
A8: e1 in W1.edges() & not e1 in the_Edges_of G2 by TARSKI:def 3;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A3, Def11;
then e1 in {e} by A8, XBOOLE_0:def 3;
then A10: e1 = e by TARSKI:def 1;
then e1 DJoins v1,v2,G1 by A3, Th109;
then e1 Joins v1,v2,G1 by GLIB_000:16;
then consider W2 being Walk of G1 such that
A11: W2 is_Walk_from v1,v2 & not e1 in W2.edges()
by A8, A4, GLIB_001:157;
W2.edges() c= the_Edges_of G1;
then W2.edges() c= the_Edges_of G2 \/ {e} by A3, Def11;
then A12: W2.edges() c= the_Edges_of G2 by A11, A10, ZFMISC_1:135;
W2.vertices() c= the_Vertices_of G2 by A6;
then reconsider W = W2 as Walk of G2 by A5, A12, GLIB_001:170;
reconsider w1=v1, w2=v2 as Vertex of G2;
W is_Walk_from w1,w2 by A11, GLIB_001:19;
hence contradiction by A2, GLIB_002:def 5;
end;
end;
hence G1 is acyclic by GLIB_002:def 2;
end;
suppose not (v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2);
then G1 == G2 by Def11;
hence thesis by A1, GLIB_002:44;
end;
end;
theorem
for G2 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 & v2 in G2.reachableFrom v1
holds G1 is non acyclic
proof
let G2;
let v1,v2 be Vertex of G2;
let e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: not e in the_Edges_of G2 and
A2: v2 in G2.reachableFrom v1;
per cases;
suppose A3: v1 <> v2;
consider W2 being Walk of G2 such that
A4: W2 is_Walk_from v1, v2 by A2, GLIB_002:def 5;
reconsider W1 = W2 as Walk of G1 by Th79;
set P = the Path of W1;
W1 is_Walk_from v1,v2 by A4, GLIB_001:19;
then P is_Walk_from v1, v2 by GLIB_001:160;
then A6: P.first() = v1 & P.last() = v2 by GLIB_001:def 23;
set W = P.addEdge(e);
e DJoins v1,v2,G1 by A1, Th109;
then A7: e Joins v2,v1,G1 by GLIB_000:16;
then A8: W is closed by A6, GLIB_001:63, GLIB_001:119;
A9: W is non trivial by A6, A7, GLIB_001:132;
not e in W2.edges() by A1;
then not e in W1.edges() by GLIB_001:110;
then A10: not e in P.edges() by GLIB_001:163, TARSKI:def 3;
A11: P is open by A3, A6, GLIB_001:def 24;
for n being odd Element of NAT st 1 < n & n <= len P holds P.n <> v1
proof
let n be odd Element of NAT;
reconsider m = 1 as odd Element of NAT by POLYFORM:4;
assume A12: 1 < n & n <= len P;
A13: P.m = v1 by A6, GLIB_001:def 6;
assume A14: P.n = v1;
then n = len P by A12, A13, GLIB_001:def 28;
hence thesis by A3, A6, A14, GLIB_001:def 7;
end;
then W is Path-like by A6, A7, A10, A11, GLIB_001:150;
hence thesis by A8, A9, GLIB_002:def 2;
end;
suppose v1 = v2;
hence G1 is non acyclic by A1, Th117;
end;
end;
:: this is the theorem that spawned most of the preliminaries,
:: although it carries a seemingly obvious meaning.
:: it basically states that adding an edge within a component of a graph
:: doesn't connect it to other components
theorem
for G2 for v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
st G2 is non connected & v2 in G2.reachableFrom v1
holds G1 is non connected
proof
:: the Proof follows this reasoning:
:: assume the additional edge would allow a walk between two vertices
:: (from different components), then the walk taken from this walk
:: with the edge replaced by a certain walk (connecting the vertices of the
:: edge without using it, which is possible because the edge connects
:: two vertices of the same component) would also be walk between those
:: two vertices, leading to a contradiction
let G2;
let v1,v2 be Vertex of G2;
let e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: G2 is non connected and
A2: v2 in G2.reachableFrom v1;
per cases;
suppose A3: v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
not for u,v being Vertex of G1 holds
ex W being Walk of G1 st W is_Walk_from u,v
proof
assume A4: for u,v being Vertex of G1 holds
ex W being Walk of G1 st W is_Walk_from u,v;
consider u,v being Vertex of G2 such that
A5: for W being Walk of G2 holds not W is_Walk_from u,v
by A1, GLIB_002:def 1;
reconsider u1=u,v3=v as Vertex of G1 by Th72;
consider W1 being Walk of G1 such that
A6: W1 is_Walk_from u1,v3 by A4;
:: we simplify the walk to a trail to use its one-on-one property
set T = the Trail of W1;
A7: T is_Walk_from u1,v3 by A6, GLIB_001:160;
per cases;
suppose not e in T.edges();
then reconsider W=T as Walk of G2 by Th113;
W is_Walk_from u,v by A7, GLIB_001:19;
hence contradiction by A5;
end;
suppose e in T.edges();
then consider w1, w2 being Vertex of G1, n being odd Element of NAT
such that
A9: n+2 <= len T and
A10: w1 = T.n & e = T.(n+1) & w2 = T.(n+2) and
A11: e Joins w1, w2,G1 by GLIB_001:103;
set E = G1.walkOf(w1,e,w2);
A12: E is_odd_substring_of T,0 by A9, A10, Th31;
e DJoins v1,v2,G1 by A3, Th109;
then A13: e Joins v1,v2,G1 by GLIB_000:16;
then per cases by A11, GLIB_000:15;
suppose A14: v1 = w1 & v2 = w2;
consider W2 being Walk of G2 such that
A15: W2 is_Walk_from v1,v2 by A2, GLIB_002:def 5;
reconsider W4=W2 as Walk of G1 by Th79;
not e in W2.edges() by A3;
then A16: not e in W4.edges() by GLIB_001:110;
set W5 = T.replaceEdgeWith(e,W4);
A17: W5 is_Walk_from u1,v3 by A7, Th51;
W2.first() = v1 & W2.last() = v2 by A15, GLIB_001:def 23;
then A18: W4.first() = v1 & W4.last() = v2 by GLIB_001:16;
G1.walkOf(W4.first(),e,W4.last()) is_odd_substring_of T, 0
by A12, A14, A18;
then not e in W5.edges() by A13, A16, A18, Th44;
then reconsider W = W5 as Walk of G2 by Th113;
W is_Walk_from u,v by A17, GLIB_001:19;
hence contradiction by A5;
end;
suppose A21: v1 = w2 & v2 = w1;
consider W3 being Walk of G2 such that
A22: W3 is_Walk_from v1,v2 by A2, GLIB_002:def 5;
set W2 = W3.reverse();
A23: W2 is_Walk_from v2,v1 by A22, GLIB_001:23;
reconsider W4=W2 as Walk of G1 by Th79;
not e in W2.edges() by A3;
then A24: not e in W4.edges() by GLIB_001:110;
set W5 = T.replaceEdgeWith(e,W4);
A25: W5 is_Walk_from u1,v3 by A7, Th51;
W2.first() = v2 & W2.last() = v1 by A23, GLIB_001:def 23;
then A26: W4.first() = v2 & W4.last() = v1 by GLIB_001:16;
G1.walkOf(W4.first(),e,W4.last()) is_odd_substring_of T, 0
by A12, A21, A26;
then not e in W5.edges() by A13, A24, A26, Th44, GLIB_000:14;
then reconsider W = W5 as Walk of G2 by Th113;
W is_Walk_from u,v by A25, GLIB_001:19;
hence contradiction by A5;
end;
end;
end;
hence thesis by GLIB_002:def 1;
end;
suppose not (v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2);
then G1 == G2 by Def11;
hence thesis by A1, GLIB_002:8;
end;
end;
:: this theorem means there is at most one edge missing to completion
theorem
for G2 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 &
(for v3, v4 being Vertex of G2 st not v3,v4 are_adjacent holds
(v3 = v4 or (v1 = v3 & v2 = v4) or (v1 = v4 & v2 = v3)))
holds G1 is complete
proof
let G2;
let v1, v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: not e in the_Edges_of G2 and
A2: for v3, v4 being Vertex of G2 st not v3,v4 are_adjacent holds
(v3 = v4 or (v1 = v3 & v2 = v4) or (v1 = v4 & v2 = v3));
for u1,u2 being Vertex of G1 st u1 <> u2 holds u1, u2 are_adjacent
proof
let u1, u2 be Vertex of G1;
assume A3: u1 <> u2;
reconsider u3=u1, u4=u2 as Vertex of G2 by Th108;
per cases;
suppose u3,u4 are_adjacent;
then consider e1 being object such that
A4: e1 Joins u3,u4,G2 by CHORD:def 3;
thus thesis by A4, Th74, CHORD:def 3;
end;
suppose not u3,u4 are_adjacent;
then per cases by A2;
suppose u3 = u4;
hence thesis by A3;
end;
suppose v1 = u3 & v2 = u4;
then e DJoins u1,u2,G1 by A1, Th109;
then e Joins u1,u2,G1 by GLIB_000:16;
hence thesis by CHORD:def 3;
end;
suppose v1 = u4 & v2 = u3;
then e DJoins u2,u1,G1 by A1, Th109;
then e Joins u1,u2,G1 by GLIB_000:16;
hence thesis by CHORD:def 3;
end;
end;
end;
hence thesis by CHORD:def 6;
end;
theorem
for G2 for v1,v2 being Vertex of G2, e being object
for G1 being addEdge of G2,v1,e,v2
st G2 is non complete & v1, v2 are_adjacent holds G1 is non complete
proof
let G2;
let v1, v2 be Vertex of G2, e be object;
let G1 be addEdge of G2,v1,e,v2;
assume that
A1: G2 is non complete and
A2: v1,v2 are_adjacent;
per cases;
suppose A3: not e in the_Edges_of G2;
ex u1,u2 being Vertex of G1 st u1 <> u2 & not u1,u2 are_adjacent
proof
consider u3,u4 being Vertex of G2 such that
A4: u3 <> u4 and
A5: not u3,u4 are_adjacent by A1, CHORD:def 6;
reconsider u1=u3, u2=u4 as Vertex of G1 by Th72;
take u1, u2;
thus u1 <> u2 by A4;
not ex e1 being object st e1 Joins u1,u2,G1
proof
given e1 being object such that
A6: e1 Joins u1,u2,G1;
per cases by A6, Th76;
suppose e1 Joins u1,u2,G2;
hence contradiction by A5, CHORD:def 3;
end;
suppose A7: not e1 in the_Edges_of G2;
A8: e1 in the_Edges_of G1 by A6, GLIB_000:def 13;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A3, Def11;
then e1 in {e} by A7, A8, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 DJoins v1,v2,G1 by A7, Th109;
then e1 Joins v1,v2,G1 by GLIB_000:16;
then per cases by A6, GLIB_000:15;
suppose v1 = u1 & v2 = u2;
hence contradiction by A2, A5;
end;
suppose v1 = u2 & v2 = u1;
hence contradiction by A2, A5;
end;
end;
end;
hence thesis by CHORD:def 3;
end;
hence thesis by CHORD:def 6;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by Def11;
hence thesis by A1, CHORD:62;
end;
end;
definition
let G;
let v1,e,v2 be object;
mode addAdjVertex of G,v1,e,v2 -> Supergraph of G means
:Def12:
the_Vertices_of it = the_Vertices_of G \/ {v2} &
the_Edges_of it = the_Edges_of G \/ {e} &
the_Source_of it = the_Source_of G +* (e .--> v1) &
the_Target_of it = the_Target_of G +* (e .--> v2)
if v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G,
the_Vertices_of it = the_Vertices_of G \/ {v1} &
the_Edges_of it = the_Edges_of G \/ {e} &
the_Source_of it = the_Source_of G +* (e .--> v1) &
the_Target_of it = the_Target_of G +* (e .--> v2)
if not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G
otherwise it == G;
existence
proof
A1: rng (e .--> v1) = rng ({e} --> v1) by FUNCOP_1:def 9
.= {v1} by FUNCOP_1:8;
A2: rng (e .--> v2) = rng ({e} --> v2) by FUNCOP_1:def 9
.= {v2} by FUNCOP_1:8;
A3: dom (e .--> v1) = dom ({e} --> v1) by FUNCOP_1:def 9
.= {e};
A4: dom (e .--> v2) = dom ({e} --> v2) by FUNCOP_1:def 9
.= {e};
hereby
assume A7: v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
set V1 = the_Vertices_of G \/ {v2};
reconsider V1 as non empty set;
set E1 = the_Edges_of G \/ {e};
set S1 = the_Source_of G +* (e .--> v1);
A8: dom S1 = (dom the_Source_of G) \/ dom (e .--> v1) by FUNCT_4:def 1
.= E1 by FUNCT_2:def 1, A3;
A9: the_Vertices_of G c= V1 by XBOOLE_1:7;
(rng the_Source_of G) \/ {v1} c= the_Vertices_of G \/ {v1}
by XBOOLE_1:9;
then (rng the_Source_of G) \/ {v1} c= the_Vertices_of G
by A7, ZFMISC_1:40;
then A10: (rng the_Source_of G) \/ rng (e .--> v1) c= V1
by A1, A9, XBOOLE_1:1;
rng S1 c= (rng the_Source_of G) \/ rng (e .--> v1) by FUNCT_4:17;
then reconsider S1 as Function of E1, V1
by A8, A10, FUNCT_2:2, XBOOLE_1:1;
set T1 = the_Target_of G +* (e .--> v2);
A11: dom T1 = (dom the_Target_of G) \/ dom (e .--> v2) by FUNCT_4:def 1
.= E1 by FUNCT_2:def 1, A4;
A12: (rng the_Target_of G) \/ rng (e .--> v2) c= V1 by A2, XBOOLE_1:9;
rng T1 c= (rng the_Target_of G) \/ rng (e .--> v2) by FUNCT_4:17;
then reconsider T1 as Function of E1, V1
by A11, A12, FUNCT_2:2, XBOOLE_1:1;
set G1 = createGraph(V1,E1,S1,T1);
the_Edges_of G c= E1 by XBOOLE_1:7;
then A13: the_Edges_of G c= the_Edges_of G1 &
the_Vertices_of G c= the_Vertices_of G1 by A9;
for e1 being set st e1 in the_Edges_of G holds
(the_Source_of G).e1 = (the_Source_of G1).e1 &
(the_Target_of G).e1 = (the_Target_of G1).e1
proof
let e1 be set;
assume e1 in the_Edges_of G;
then A14: not e1 in dom (e .--> v1) &
not e1 in dom (e .--> v2) by A7, TARSKI:def 1;
thus (the_Source_of G1).e1
= (the_Source_of G +* (e .--> v1)).e1
.= (the_Source_of G).e1 by A14, FUNCT_4:11;
thus (the_Target_of G1).e1
= (the_Target_of G +* (e .--> v2)).e1
.= (the_Target_of G).e1 by A14, FUNCT_4:11;
thus thesis;
end;
then reconsider G1 as Supergraph of G by A13, Def9;
take G1;
thus the_Vertices_of G1 = the_Vertices_of G \/ {v2} &
the_Edges_of G1 = the_Edges_of G \/ {e} &
the_Source_of G1 = the_Source_of G +* (e .--> v1) &
the_Target_of G1 = the_Target_of G +* (e .--> v2);
end;
hereby
assume A15: not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
set V1 = the_Vertices_of G \/ {v1};
reconsider V1 as non empty set;
set E1 = the_Edges_of G \/ {e};
set S1 = the_Source_of G +* (e .--> v1);
A16: dom S1 = (dom the_Source_of G) \/ dom (e .--> v1) by FUNCT_4:def 1
.= E1 by FUNCT_2:def 1, A3;
A17: the_Vertices_of G c= V1 by XBOOLE_1:7;
A18: (rng the_Source_of G) \/ rng (e .--> v1) c= V1 by A1, XBOOLE_1:9;
rng S1 c= (rng the_Source_of G) \/ rng (e .--> v1) by FUNCT_4:17;
then reconsider S1 as Function of E1, V1
by A16, A18, FUNCT_2:2, XBOOLE_1:1;
set T1 = the_Target_of G +* (e .--> v2);
A19: dom T1 = (dom the_Target_of G) \/ dom (e .--> v2) by FUNCT_4:def 1
.= E1 by FUNCT_2:def 1, A4;
(rng the_Target_of G) \/ {v2} c= the_Vertices_of G \/ {v2}
by XBOOLE_1:9;
then (rng the_Target_of G) \/ {v2} c= the_Vertices_of G
by A15, ZFMISC_1:40;
then A20: (rng the_Target_of G) \/ rng (e .--> v2) c= V1
by A2, A17, XBOOLE_1:1;
rng T1 c= (rng the_Target_of G) \/ rng (e .--> v2) by FUNCT_4:17;
then reconsider T1 as Function of E1, V1
by A19, A20, FUNCT_2:2, XBOOLE_1:1;
set G1 = createGraph(V1,E1,S1,T1);
the_Edges_of G c= E1 by XBOOLE_1:7;
then A21: the_Edges_of G c= the_Edges_of G1 &
the_Vertices_of G c= the_Vertices_of G1 by A17;
for e1 being set st e1 in the_Edges_of G holds
(the_Source_of G).e1 = (the_Source_of G1).e1 &
(the_Target_of G).e1 = (the_Target_of G1).e1
proof
let e1 be set;
assume e1 in the_Edges_of G;
then A22: not e1 in dom (e .--> v1) &
not e1 in dom (e .--> v2) by A15, TARSKI:def 1;
thus (the_Source_of G1).e1
= (the_Source_of G +* (e .--> v1)).e1
.= (the_Source_of G).e1 by A22, FUNCT_4:11;
thus (the_Target_of G1).e1
= (the_Target_of G +* (e .--> v2)).e1
.= (the_Target_of G).e1 by A22, FUNCT_4:11;
thus thesis;
end;
then reconsider G1 as Supergraph of G by A21, Def9;
take G1;
thus the_Vertices_of G1 = the_Vertices_of G \/ {v1} &
the_Edges_of G1 = the_Edges_of G \/ {e} &
the_Source_of G1 = the_Source_of G +* (e .--> v1) &
the_Target_of G1 = the_Target_of G +* (e .--> v2);
end;
assume not (v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) &
not (not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
reconsider G1 = G as Supergraph of G by Th65;
take G1;
thus thesis;
end;
consistency;
end;
definition
let G;
let v1 be Vertex of G;
let e, v2 be object;
redefine mode addAdjVertex of G,v1,e,v2 means :: redefines addAdjVertex (GLIB_006, definition)
:Def13:
the_Vertices_of it = the_Vertices_of G \/ {v2} &
the_Edges_of it = the_Edges_of G \/ {e} &
the_Source_of it = the_Source_of G +* (e .--> v1) &
the_Target_of it = the_Target_of G +* (e .--> v2)
if not v2 in the_Vertices_of G & not e in the_Edges_of G
otherwise it == G;
compatibility by Def12;
consistency;
end;
definition
let G;
let v1,e be object;
let v2 be Vertex of G;
redefine mode addAdjVertex of G,v1,e,v2 means :: redefines addAdjVertex (GLIB_006, definition)
:Def14:
the_Vertices_of it = the_Vertices_of G \/ {v1} &
the_Edges_of it = the_Edges_of G \/ {e} &
the_Source_of it = the_Source_of G +* (e .--> v1) &
the_Target_of it = the_Target_of G +* (e .--> v2)
if not v1 in the_Vertices_of G & not e in the_Edges_of G
otherwise it == G;
compatibility by Def12;
consistency;
end;
theorem
for G for v1,e,v2 being object, G1, G2 being addAdjVertex of G,v1,e,v2
holds G1 == G2
proof
let G;
let v1,e,v2 be object;
let G1, G2 be addAdjVertex of G,v1,e,v2;
per cases;
suppose v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
then
the_Vertices_of G1 = the_Vertices_of G \/ {v2} &
the_Edges_of G1 = the_Edges_of G \/ {e} &
the_Source_of G1 = the_Source_of G +* (e .--> v1) &
the_Target_of G1 = the_Target_of G +* (e .--> v2) &
the_Vertices_of G2 = the_Vertices_of G \/ {v2} &
the_Edges_of G2 = the_Edges_of G \/ {e} &
the_Source_of G2 = the_Source_of G +* (e .--> v1) &
the_Target_of G2 = the_Target_of G +* (e .--> v2) by Def12;
hence thesis by GLIB_000:def 34;
end;
suppose not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
then
the_Vertices_of G1 = the_Vertices_of G \/ {v1} &
the_Edges_of G1 = the_Edges_of G \/ {e} &
the_Source_of G1 = the_Source_of G +* (e .--> v1) &
the_Target_of G1 = the_Target_of G +* (e .--> v2) &
the_Vertices_of G2 = the_Vertices_of G \/ {v1} &
the_Edges_of G2 = the_Edges_of G \/ {e} &
the_Source_of G2 = the_Source_of G +* (e .--> v1) &
the_Target_of G2 = the_Target_of G +* (e .--> v2) by Def12;
hence thesis by GLIB_000:def 34;
end;
suppose not (v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) & not (not v1 in the_Vertices_of G &
v2 in the_Vertices_of G & not e in the_Edges_of G);
then G == G1 & G == G2 by Def12;
hence thesis by GLIB_000:85;
end;
end;
theorem
for G, G2 for v1,e,v2 being object, G1 being addAdjVertex of G,v1,e,v2
st G1 == G2 holds G2 is addAdjVertex of G,v1,e,v2
proof
let G, G2;
let v1,e,v2 be object;
let G1 be addAdjVertex of G,v1,e,v2;
assume A1: G1 == G2;
per cases;
suppose A2: v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v2} &
the_Edges_of G1 = the_Edges_of G \/ {e} &
the_Source_of G1 = the_Source_of G +* (e .--> v1) &
the_Target_of G1 = the_Target_of G +* (e .--> v2) by Def12;
then A3: the_Vertices_of G2 = the_Vertices_of G \/ {v2} &
the_Edges_of G2 = the_Edges_of G \/ {e} &
the_Source_of G2 = the_Source_of G +* (e .--> v1) &
the_Target_of G2 = the_Target_of G +* (e .--> v2) by A1, GLIB_000:def 34;
G2 is Supergraph of G1 by A1, Th62;
then G2 is Supergraph of G by Th66;
hence thesis by A2, A3, Def12;
end;
suppose A4: not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v1} &
the_Edges_of G1 = the_Edges_of G \/ {e} &
the_Source_of G1 = the_Source_of G +* (e .--> v1) &
the_Target_of G1 = the_Target_of G +* (e .--> v2) by Def12;
then A5: the_Vertices_of G2 = the_Vertices_of G \/ {v1} &
the_Edges_of G2 = the_Edges_of G \/ {e} &
the_Source_of G2 = the_Source_of G +* (e .--> v1) &
the_Target_of G2 = the_Target_of G +* (e .--> v2) by A1, GLIB_000:def 34;
G2 is Supergraph of G1 by A1, Th62;
then G2 is Supergraph of G by Th66;
hence thesis by A4, A5, Def12;
end;
suppose A6: not (v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) & not (not v1 in the_Vertices_of G &
v2 in the_Vertices_of G & not e in the_Edges_of G);
then G == G1 by Def12;
then A7: G == G2 by A1, GLIB_000:85;
then G2 is Supergraph of G by Th62;
hence thesis by A6, A7, Def12;
end;
end;
theorem Th129:
for G2 for v1 being Vertex of G2, e,v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2
holds ex G3 being addVertex of G2,v2 st G1 is addEdge of G3,v1,e,v2
proof
let G2;
let v1 be Vertex of G2;
let e,v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2;
set G3 = the addVertex of G2,v2;
take G3;
A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v2} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} &
the_Source_of G1 = the_Source_of G2 +* (e .--> v1) &
the_Target_of G1 = the_Target_of G2 +* (e .--> v2) by A1, Def13;
A3: the_Vertices_of G3 = the_Vertices_of G2 \/ {v2} &
the_Edges_of G3 = the_Edges_of G2 &
the_Source_of G3 = the_Source_of G2 &
the_Target_of G3 = the_Target_of G2 by Def10;
the_Vertices_of G2 c= the_Vertices_of G3 by Def9;
then A5: v1 in the_Vertices_of G3 by TARSKI:def 3;
A6: v2 is Vertex of G3 by Th98;
A8: the_Edges_of G3 c= the_Edges_of G1 by A2, A3, XBOOLE_1:11;
for e1 being set st e1 in the_Edges_of G3 holds
(the_Source_of G3).e1 = (the_Source_of G1).e1 &
(the_Target_of G3).e1 = (the_Target_of G1).e1 by A3, Def9;
then G1 is Supergraph of G3 by A2, A3, A8, Def9;
hence G1 is addEdge of G3,v1,e,v2 by A1, A2, A3, A5, A6, Def11;
end;
theorem Th130:
for G2 for v1, e being object, v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2
holds ex G3 being addVertex of G2,v1 st G1 is addEdge of G3,v1,e,v2
proof
let G2;
let v1, e be object;
let v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2 & not v1 in the_Vertices_of G2;
set G3 = the addVertex of G2,v1;
take G3;
A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v1} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} &
the_Source_of G1 = the_Source_of G2 +* (e .--> v1) &
the_Target_of G1 = the_Target_of G2 +* (e .--> v2) by A1, Def14;
A3: the_Vertices_of G3 = the_Vertices_of G2 \/ {v1} &
the_Edges_of G3 = the_Edges_of G2 &
the_Source_of G3 = the_Source_of G2 &
the_Target_of G3 = the_Target_of G2 by Def10;
the_Vertices_of G2 c= the_Vertices_of G3 by Def9;
then A5: v2 in the_Vertices_of G3 by TARSKI:def 3;
A6: v1 is Vertex of G3 by Th98;
A8: the_Edges_of G3 c= the_Edges_of G1 by A2, A3, XBOOLE_1:11;
for e1 being set st e1 in the_Edges_of G3 holds
(the_Source_of G3).e1 = (the_Source_of G1).e1 &
(the_Target_of G3).e1 = (the_Target_of G1).e1 by A3, Def9;
then G1 is Supergraph of G3 by A2, A3, A8, Def9;
hence G1 is addEdge of G3,v1,e,v2 by A1, A2, A3, A5, A6, Def11;
end;
theorem
for G3 being _Graph, v1 being Vertex of G3, e,v2 being object
for G2 being addVertex of G3,v2, G1 being addEdge of G2,v1,e,v2
st not e in the_Edges_of G3 & not v2 in the_Vertices_of G3
holds G1 is addAdjVertex of G3,v1,e,v2
proof
let G3 be _Graph;
let v1 be Vertex of G3;
let e,v2 be object;
let G2 be addVertex of G3,v2;
let G1 be addEdge of G2,v1,e,v2;
assume A1: not e in the_Edges_of G3 & not v2 in the_Vertices_of G3;
A2: G1 is Supergraph of G3 by Th66;
A3: the_Vertices_of G2 = the_Vertices_of G3 \/ {v2} &
the_Edges_of G2 = the_Edges_of G3 &
the_Source_of G2 = the_Source_of G3 &
the_Target_of G2 = the_Target_of G3 by Def10;
A5: v1 is Vertex of G2 by Th72;
v2 is Vertex of G2 by Th98;
then the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ {e} &
the_Source_of G1 = the_Source_of G2 +* (e .--> v1) &
the_Target_of G1 = the_Target_of G2 +* (e .--> v2) by A1, A3, A5, Def11;
hence G1 is addAdjVertex of G3,v1,e,v2 by A1, A2, A3, Def13;
end;
theorem
for G3 being _Graph, v1, e being object, v2 being Vertex of G3
for G2 being addVertex of G3,v1, G1 being addEdge of G2,v1,e,v2
st not e in the_Edges_of G3 & not v1 in the_Vertices_of G3
holds G1 is addAdjVertex of G3,v1,e,v2
proof
let G3 be _Graph;
let v1, e be object;
let v2 be Vertex of G3;
let G2 be addVertex of G3,v1;
let G1 be addEdge of G2,v1,e,v2;
assume A1: not e in the_Edges_of G3 & not v1 in the_Vertices_of G3;
A2: G1 is Supergraph of G3 by Th66;
A3: the_Vertices_of G2 = the_Vertices_of G3 \/ {v1} &
the_Edges_of G2 = the_Edges_of G3 &
the_Source_of G2 = the_Source_of G3 &
the_Target_of G2 = the_Target_of G3 by Def10;
A5: v2 is Vertex of G2 by Th72;
v1 is Vertex of G2 by Th98;
then the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ {e} &
the_Source_of G1 = the_Source_of G2 +* (e .--> v1) &
the_Target_of G1 = the_Target_of G2 +* (e .--> v2) by A1, A3, A5, Def11;
hence G1 is addAdjVertex of G3,v1,e,v2 by A1, A2, A3, Def14;
end;
theorem Th133:
for G2 for 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 v2 is Vertex of G1
proof
let G2;
let 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 A1: the_Vertices_of G1 = the_Vertices_of G2 \/ {v2} by Def13;
v2 in {v2} by TARSKI:def 1;
hence thesis by A1, XBOOLE_0:def 3;
end;
theorem Th134:
for G2 for 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 v1 is Vertex of G1
proof
let G2;
let 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 A1: the_Vertices_of G1 = the_Vertices_of G2 \/ {v1} by Def14;
v1 in {v1} by TARSKI:def 1;
hence thesis by A1, XBOOLE_0:def 3;
end;
theorem Th135:
for G2 for 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 e DJoins v1,v2,G1 & e Joins v1,v2,G1
proof
let G2 be _Graph;
let v1 be Vertex of G2;
let e, v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not v2 in the_Vertices_of G2 & not e in the_Edges_of G2;
e in {e} by TARSKI:def 1;
then e in the_Edges_of G2 \/ {e} by XBOOLE_0:def 3;
then A3: e in the_Edges_of G1 by A1, Def13;
((the_Source_of G2) +* (e .--> v1)).e = v1 &
((the_Target_of G2) +* (e .--> v2)).e = v2 by FUNCT_4:113;
then (the_Source_of G1).e = v1 & (the_Target_of G1).e = v2 by A1, Def13;
hence e DJoins v1,v2,G1 by A3, GLIB_000:def 14;
hence e Joins v1,v2,G1 by GLIB_000:16;
end;
theorem Th136:
for G2 for 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 e DJoins v1,v2,G1 & e Joins v1,v2,G1
proof
let G2 be _Graph;
let v1, e be object;
let v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not v1 in the_Vertices_of G2 & not e in the_Edges_of G2;
e in {e} by TARSKI:def 1;
then e in the_Edges_of G2 \/ {e} by XBOOLE_0:def 3;
then A3: e in the_Edges_of G1 by A1, Def14;
((the_Source_of G2) +* (e .--> v1)).e = v1 &
((the_Target_of G2) +* (e .--> v2)).e = v2 by FUNCT_4:113;
then (the_Source_of G1).e = v1 & (the_Target_of G1).e = v2 by A1, Def14;
hence e DJoins v1,v2,G1 by A3, GLIB_000:def 14;
hence e Joins v1,v2,G1 by GLIB_000:16;
end;
theorem Th137:
for G2 for 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
for e1, w being object st (w <> v1 or e1 <> e)
holds not e1 Joins w,v2,G1
proof
let G2;
let v1 be Vertex of G2, e be object, v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not v2 in the_Vertices_of G2 & not e in the_Edges_of G2;
let e1, w be object;
assume w <> v1 or e1 <> e;
then per cases;
suppose A2: w <> v1;
assume A3: e1 Joins w,v2,G1;
then per cases by Th76;
suppose e1 Joins w,v2,G2;
hence contradiction by A1, GLIB_000:13;
end;
suppose A4: not e1 in the_Edges_of G2;
A5: e1 in the_Edges_of G1 by A3, GLIB_000:def 13;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, Def12;
then e1 in {e} by A4, A5, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 Joins v1,v2,G1 by A1, Th135;
then per cases by A3, GLIB_000:15;
suppose v1=w & v2=v2;
hence contradiction by A2;
end;
suppose v1=v2 & v2=w;
hence contradiction by A1;
end;
end;
end;
suppose A6: e1 <> e;
assume A7: e1 Joins w,v2,G1;
then per cases by Th76;
suppose e1 Joins w,v2,G2;
hence contradiction by A1, GLIB_000:13;
end;
suppose A8: not e1 in the_Edges_of G2;
A9: e1 in the_Edges_of G1 by A7, GLIB_000:def 13;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, Def12;
then e1 in {e} by A8, A9, XBOOLE_0:def 3;
hence contradiction by A6, TARSKI:def 1;
end;
end;
end;
theorem Th138:
for G2 for 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
for e1, w being object st (w <> v2 or e1 <> e)
holds not e1 Joins v1,w,G1
proof
let G2;
let v1, e be object, v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not v1 in the_Vertices_of G2 & not e in the_Edges_of G2;
let e1, w be object;
assume w <> v2 or e1 <> e;
then per cases;
suppose A2: w <> v2;
assume A3: e1 Joins v1,w,G1;
then per cases by Th76;
suppose e1 Joins v1,w,G2;
hence contradiction by A1, GLIB_000:13;
end;
suppose A4: not e1 in the_Edges_of G2;
A5: e1 in the_Edges_of G1 by A3, GLIB_000:def 13;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, Def12;
then e1 in {e} by A4, A5, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 Joins v1,v2,G1 by A1, Th136;
then per cases by A3, GLIB_000:15;
suppose v1=v1 & v2=w;
hence contradiction by A2;
end;
suppose v1=w & v2=v1;
hence contradiction by A1;
end;
end;
end;
suppose A6: e1 <> e;
assume A7: e1 Joins v1,w,G1;
then per cases by Th76;
suppose e1 Joins v1,w,G2;
hence contradiction by A1, GLIB_000:13;
end;
suppose A8: not e1 in the_Edges_of G2;
A9: e1 in the_Edges_of G1 by A7, GLIB_000:def 13;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, Def12;
then e1 in {e} by A8, A9, XBOOLE_0:def 3;
hence contradiction by A6, TARSKI:def 1;
end;
end;
end;
theorem Th139:
for G2 for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
holds G1.edgesBetween(the_Vertices_of G2) = the_Edges_of G2
proof
let G2;
let v1,e,v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
per cases;
suppose A1: v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {v2} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by Def12;
then A2: the_Edges_of G2 = the_Edges_of G1 \ {e} by A1, ZFMISC_1:117;
for e1 being object holds e1 in G1.edgesBetween(the_Vertices_of G2)
iff e1 in the_Edges_of G1 \ {e}
proof
let e1 be object;
hereby
assume e1 in G1.edgesBetween(the_Vertices_of G2);
then A3: e1 in the_Edges_of G1 &
(the_Source_of G1).e1 in the_Vertices_of G2 &
(the_Target_of G1).e1 in the_Vertices_of G2 by GLIB_000:31;
e DJoins v1,v2,G1 by A1, Th135;
then e1 <> e by A1, A3, GLIB_000:def 14;
then not e1 in {e} by TARSKI:def 1;
hence e1 in the_Edges_of G1 \ {e} by A3, XBOOLE_0:def 5;
end;
assume A4: e1 in the_Edges_of G1 \ {e};
reconsider e2 = e1 as set by TARSKI:1;
A6: e2 in the_Edges_of G2 by A2, A4;
A7: (the_Source_of G2).e2 in the_Vertices_of G2 &
(the_Target_of G2).e2 in the_Vertices_of G2 by A6, FUNCT_2:5;
e2 Joins (the_Source_of G2).e2, (the_Target_of G2).e2, G2
by A6, GLIB_000:def 13;
hence thesis by A7, Th74, GLIB_000:32;
end;
hence thesis by A2, TARSKI:2;
end;
suppose A8: not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {v1} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by Def12;
then A9: the_Edges_of G2 = the_Edges_of G1 \ {e} by A8, ZFMISC_1:117;
for e1 being object holds e1 in G1.edgesBetween(the_Vertices_of G2)
iff e1 in the_Edges_of G1 \ {e}
proof
let e1 be object;
hereby
assume e1 in G1.edgesBetween(the_Vertices_of G2);
then A10: e1 in the_Edges_of G1 &
(the_Source_of G1).e1 in the_Vertices_of G2 &
(the_Target_of G1).e1 in the_Vertices_of G2 by GLIB_000:31;
e DJoins v1,v2,G1 by A8, Th136;
then e1 <> e by A8, A10, GLIB_000:def 14;
then not e1 in {e} by TARSKI:def 1;
hence e1 in the_Edges_of G1 \ {e} by A10, XBOOLE_0:def 5;
end;
assume A11: e1 in the_Edges_of G1 \ {e};
reconsider e2 = e1 as set by TARSKI:1;
A13: e2 in the_Edges_of G2 by A9, A11;
A14: (the_Source_of G2).e2 in the_Vertices_of G2 &
(the_Target_of G2).e2 in the_Vertices_of G2 by A13, FUNCT_2:5;
e2 Joins (the_Source_of G2).e2, (the_Target_of G2).e2, G2
by A13, GLIB_000:def 13;
hence thesis by A14, Th74, GLIB_000:32;
end;
hence thesis by A9, TARSKI:2;
end;
suppose not (v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 &
not e in the_Edges_of G2) & not (
not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2);
then G1 == G2 by Def12;
hence G1.edgesBetween(the_Vertices_of G2)
= G2.edgesBetween(the_Vertices_of G2) by GLIB_000:90
.= the_Edges_of G2 by GLIB_000:34;
end;
end;
theorem Th140:
for G2 for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
holds G2 is inducedSubgraph of G1, the_Vertices_of G2
proof
let G2;
let v1,e,v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
per cases;
suppose v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {v2} by Def12;
then A1: the_Vertices_of G2 is non empty Subset of the_Vertices_of G1
by XBOOLE_1:7;
A2: G2 is Subgraph of G1 by Th61;
the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G2) by Th139;
hence thesis by A1, A2, GLIB_000:def 37;
end;
suppose not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {v1} by Def12;
then A3: the_Vertices_of G2 is non empty Subset of the_Vertices_of G1
by XBOOLE_1:7;
A4: G2 is Subgraph of G1 by Th61;
the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G2) by Th139;
hence thesis by A3, A4, GLIB_000:def 37;
end;
suppose not (v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 &
not e in the_Edges_of G2) & not (
not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2);
then A5: G1 == G2 by Def12;
then A6: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 34;
G1 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:100;
hence thesis by A5, A6, GLIB_000:101;
end;
end;
theorem Th141:
for G2 for v1 being Vertex of G2, e being object, v2 being set
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2
holds G2 is removeVertex of G1, v2
proof
let G2;
let v1 be Vertex of G2, e be object, v2 be set;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {v2} by Def13;
then the_Vertices_of G2 = the_Vertices_of G1 \ {v2} by A1, ZFMISC_1:117;
hence thesis by Th140;
end;
theorem Th142:
for G2 for v1 being set, e being object, v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2
holds G2 is removeVertex of G1, v1
proof
let G2;
let v1 be set, e be object, v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2 & not v1 in the_Vertices_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {v1} by Def14;
then the_Vertices_of G2 = the_Vertices_of G1 \ {v1} by A1, ZFMISC_1:117;
hence thesis by Th140;
end;
theorem
for G being non _trivial _Graph, v1 being Vertex of G, e,v2 being object
for G1 being addAdjVertex of G,v1,e,v2
for G2 being removeVertex of G1,v1
for G3 being removeVertex of G,v1
st not e in the_Edges_of G & not v2 in the_Vertices_of G
holds G2 is addVertex of G3, v2
proof
let G be non _trivial _Graph, v1 be Vertex of G, e,v2 be object;
let G1 be addAdjVertex of G,v1,e,v2;
let G2 be removeVertex of G1,v1;
let G3 be removeVertex of G,v1;
assume A1: not e in the_Edges_of G & not v2 in the_Vertices_of G;
A2: v1 is Vertex of G1 & v1 <> v2 by A1, Th72;
A3: the_Vertices_of G2 = the_Vertices_of G1 \ {v1} by A2, GLIB_000:47
.= (the_Vertices_of G \/ {v2}) \ {v1} by A1, Def12
.= (the_Vertices_of G \ {v1}) \/ ({v2} \ {v1}) by XBOOLE_1:42
.= (the_Vertices_of G \ {v1}) \/ {v2} by A2, ZFMISC_1:14
.= the_Vertices_of G3 \/ {v2} by GLIB_000:47;
:: lemma for equality of edge sets
for e1 being object holds e1 in G1.edgesBetween(the_Vertices_of G1 \ {v1})
iff e1 in G.edgesBetween(the_Vertices_of G \ {v1})
proof
let e1 be object;
set x1 = (the_Source_of G1).e1, y1 = (the_Target_of G1).e1;
set x = (the_Source_of G).e1, y = (the_Target_of G).e1;
hereby
assume e1 in G1.edgesBetween(the_Vertices_of G1 \ {v1});
then A4: e1 in the_Edges_of G1 & x1 in the_Vertices_of G1 \ {v1} &
y1 in the_Vertices_of G1 \ {v1} by GLIB_000:31;
then e1 DJoins x1, y1, G1 by GLIB_000:def 14;
then per cases by Th75;
suppose A5: e1 DJoins x1, y1, G;
then A6: e1 in the_Edges_of G by GLIB_000:def 14;
e1 Joins x1, y1, G by A5, GLIB_000:16;
then A7: x1 in the_Vertices_of G & y1 in the_Vertices_of G
by GLIB_000:13;
not x1 in {v1} & not y1 in {v1} by A4, XBOOLE_0:def 5;
then A8: x1 in the_Vertices_of G\{v1} & y1 in the_Vertices_of G\{v1}
by A7, XBOOLE_0:def 5;
x = x1 & y = y1 by A5, GLIB_000:def 14;
hence e1 in G.edgesBetween(the_Vertices_of G \ {v1})
by A6, A8, GLIB_000:31;
end;
suppose A9: not e1 in the_Edges_of G;
the_Edges_of G1 = the_Edges_of G \/ {e} by A1, Def12;
then e1 in {e} by A4, A9, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 DJoins v1,v2,G1 by A1, Th135;
then x1 = v1 by GLIB_000:def 14;
then x1 in {v1} by TARSKI:def 1;
hence e1 in G.edgesBetween(the_Vertices_of G \ {v1})
by A4, XBOOLE_0:def 5; :: by contradiction
end;
end;
assume e1 in G.edgesBetween(the_Vertices_of G \ {v1});
then A10: e1 in the_Edges_of G & x in the_Vertices_of G \ {v1} &
y in the_Vertices_of G \ {v1} by GLIB_000:31;
the_Vertices_of G c= the_Vertices_of G1 by Def9;
then A11: x in the_Vertices_of G1 \ {v1} & y in the_Vertices_of G1 \ {v1}
by A10, XBOOLE_1:33, TARSKI:def 3;
A12: x = x1 & y = y1 by A10, Def9;
the_Edges_of G c= the_Edges_of G1 by Def9;
hence e1 in G1.edgesBetween(the_Vertices_of G1 \ {v1})
by A10, A11, A12, GLIB_000:31;
end;
then A13: G1.edgesBetween(the_Vertices_of G1 \ {v1})
= G.edgesBetween(the_Vertices_of G \ {v1}) by TARSKI:2;
A14: the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ {v1})
by A2, GLIB_000:47
.= the_Edges_of G3 by A13, GLIB_000:47;
dom the_Source_of G2 = the_Edges_of G2 &
dom the_Target_of G2 = the_Edges_of G2 by GLIB_000:4;
then A16: dom the_Source_of G2 = dom the_Source_of G3 &
dom the_Target_of G2 = dom the_Target_of G3 by A14, GLIB_000:4;
for e1 being object st e1 in dom the_Source_of G2 holds
(the_Source_of G2).e1 = (the_Source_of G3).e1
proof
let e1 be object;
assume e1 in dom the_Source_of G2;
then A17: e1 in the_Edges_of G2;
thus (the_Source_of G2).e1 = (the_Source_of G1).e1 by A17, GLIB_000:def 32
.= (the_Source_of G).e1 by A14, A17, Def9
.= (the_Source_of G3).e1 by A14, A17, GLIB_000:def 32;
end;
then A19: the_Source_of G2 = the_Source_of G3 by A16, FUNCT_1:2;
for e1 being object st e1 in dom the_Target_of G2 holds
(the_Target_of G2).e1 = (the_Target_of G3).e1
proof
let e1 be object;
assume e1 in dom the_Target_of G2;
then A20: e1 in the_Edges_of G2;
thus (the_Target_of G2).e1 = (the_Target_of G1).e1 by A20, GLIB_000:def 32
.= (the_Target_of G).e1 by A14, A20, Def9
.= (the_Target_of G3).e1 by A14, A20, GLIB_000:def 32;
end;
then A22: the_Target_of G2 = the_Target_of G3 by A16, FUNCT_1:2;
:: left is to show Supergraph property
now
the_Vertices_of G c= the_Vertices_of G1 by Def9;
then the_Vertices_of G \ {v1} c= the_Vertices_of G1 \ {v1} by XBOOLE_1:33;
then the_Vertices_of G3 c= the_Vertices_of G1 \ {v1} by GLIB_000:47;
hence the_Vertices_of G3 c= the_Vertices_of G2 by A2, GLIB_000:47;
thus the_Edges_of G3 c= the_Edges_of G2 by A14;
let e1 be set;
assume e1 in the_Edges_of G3;
thus (the_Source_of G3).e1 = (the_Source_of G2).e1 &
(the_Target_of G3).e1 = (the_Target_of G2).e1 by A19, A22;
end;
then G2 is Supergraph of G3 by Def9;
hence thesis by A3, A14, A19, A22, Def10;
end;
theorem
for G being non _trivial _Graph, v1,e being object, v2 being Vertex of G
for G1 being addAdjVertex of G,v1,e,v2
for G2 being removeVertex of G1,v2
for G3 being removeVertex of G,v2
st not e in the_Edges_of G & not v1 in the_Vertices_of G
holds G2 is addVertex of G3, v1
proof
let G be non _trivial _Graph, v1,e be object, v2 be Vertex of G;
let G1 be addAdjVertex of G,v1,e,v2;
let G2 be removeVertex of G1,v2;
let G3 be removeVertex of G,v2;
assume A1: not e in the_Edges_of G & not v1 in the_Vertices_of G;
A2: v2 is Vertex of G1 & v1 <> v2 by A1, Th72;
A3: the_Vertices_of G2 = the_Vertices_of G1 \ {v2} by A2, GLIB_000:47
.= (the_Vertices_of G \/ {v1}) \ {v2} by A1, Def12
.= (the_Vertices_of G \ {v2}) \/ ({v1} \ {v2}) by XBOOLE_1:42
.= (the_Vertices_of G \ {v2}) \/ {v1} by A2, ZFMISC_1:14
.= the_Vertices_of G3 \/ {v1} by GLIB_000:47;
:: lemma for equality of edge sets
for e1 being object holds e1 in G1.edgesBetween(the_Vertices_of G1 \ {v2})
iff e1 in G.edgesBetween(the_Vertices_of G \ {v2})
proof
let e1 be object;
set x1 = (the_Source_of G1).e1, y1 = (the_Target_of G1).e1;
set x = (the_Source_of G).e1, y = (the_Target_of G).e1;
hereby
assume e1 in G1.edgesBetween(the_Vertices_of G1 \ {v2});
then A4: e1 in the_Edges_of G1 & x1 in the_Vertices_of G1 \ {v2} &
y1 in the_Vertices_of G1 \ {v2} by GLIB_000:31;
then e1 DJoins x1, y1, G1 by GLIB_000:def 14;
then per cases by Th75;
suppose A5: e1 DJoins x1, y1, G;
then A6: e1 in the_Edges_of G by GLIB_000:def 14;
e1 Joins x1, y1, G by A5, GLIB_000:16;
then A7: x1 in the_Vertices_of G & y1 in the_Vertices_of G
by GLIB_000:13;
not x1 in {v2} & not y1 in {v2} by A4, XBOOLE_0:def 5;
then A8: x1 in the_Vertices_of G\{v2} & y1 in the_Vertices_of G\{v2}
by A7, XBOOLE_0:def 5;
x = x1 & y = y1 by A5, GLIB_000:def 14;
hence e1 in G.edgesBetween(the_Vertices_of G \ {v2})
by A6, A8, GLIB_000:31;
end;
suppose A9: not e1 in the_Edges_of G;
the_Edges_of G1 = the_Edges_of G \/ {e} by A1, Def12;
then e1 in {e} by A4, A9, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 DJoins v1,v2,G1 by A1, Th136;
then y1 = v2 by GLIB_000:def 14;
then y1 in {v2} by TARSKI:def 1;
hence e1 in G.edgesBetween(the_Vertices_of G \ {v2})
by A4, XBOOLE_0:def 5; :: by contradiction
end;
end;
assume e1 in G.edgesBetween(the_Vertices_of G \ {v2});
then A10: e1 in the_Edges_of G & x in the_Vertices_of G \ {v2} &
y in the_Vertices_of G \ {v2} by GLIB_000:31;
the_Vertices_of G c= the_Vertices_of G1 by Def9;
then A11: x in the_Vertices_of G1 \ {v2} & y in the_Vertices_of G1 \ {v2}
by A10, XBOOLE_1:33, TARSKI:def 3;
A12: x = x1 & y = y1 by A10, Def9;
the_Edges_of G c= the_Edges_of G1 by Def9;
hence e1 in G1.edgesBetween(the_Vertices_of G1 \ {v2})
by A10, A11, A12, GLIB_000:31;
end;
then A13: G1.edgesBetween(the_Vertices_of G1 \ {v2})
= G.edgesBetween(the_Vertices_of G \ {v2}) by TARSKI:2;
A14: the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ {v2})
by A2, GLIB_000:47
.= the_Edges_of G3 by A13, GLIB_000:47;
dom the_Source_of G2 = the_Edges_of G2 &
dom the_Target_of G2 = the_Edges_of G2 by GLIB_000:4;
then A16: dom the_Source_of G2 = dom the_Source_of G3 &
dom the_Target_of G2 = dom the_Target_of G3 by A14, GLIB_000:4;
for e1 being object st e1 in dom the_Source_of G2 holds
(the_Source_of G2).e1 = (the_Source_of G3).e1
proof
let e1 be object;
assume e1 in dom the_Source_of G2;
then A17: e1 in the_Edges_of G2;
thus (the_Source_of G2).e1 = (the_Source_of G1).e1 by A17, GLIB_000:def 32
.= (the_Source_of G).e1 by A14, A17, Def9
.= (the_Source_of G3).e1 by A14, A17, GLIB_000:def 32;
end;
then A19: the_Source_of G2 = the_Source_of G3 by A16, FUNCT_1:2;
for e1 being object st e1 in dom the_Target_of G2 holds
(the_Target_of G2).e1 = (the_Target_of G3).e1
proof
let e1 be object;
assume e1 in dom the_Target_of G2;
then A20: e1 in the_Edges_of G2;
thus (the_Target_of G2).e1 = (the_Target_of G1).e1 by A20, GLIB_000:def 32
.= (the_Target_of G).e1 by A14, A20, Def9
.= (the_Target_of G3).e1 by A14, A20, GLIB_000:def 32;
end;
then A22: the_Target_of G2 = the_Target_of G3 by A16, FUNCT_1:2;
:: left is to show Supergraph property
now
the_Vertices_of G c= the_Vertices_of G1 by Def9;
then the_Vertices_of G \ {v2} c= the_Vertices_of G1 \ {v2} by XBOOLE_1:33;
then the_Vertices_of G3 c= the_Vertices_of G1 \ {v2} by GLIB_000:47;
hence the_Vertices_of G3 c= the_Vertices_of G2 by A2, GLIB_000:47;
thus the_Edges_of G3 c= the_Edges_of G2 by A14;
let e1 be set;
assume e1 in the_Edges_of G3;
thus (the_Source_of G3).e1 = (the_Source_of G2).e1 &
(the_Target_of G3).e1 = (the_Target_of G2).e1 by A19, A22;
end;
then G2 is Supergraph of G3 by Def9;
hence thesis by A3, A14, A19, A22, Def10;
end;
:: What has been left out here is the Proof that the vertex to which
:: a new vertex with edge is added becomes a cut-vertex in the
:: resulting supergraph. A sketch of the Proof is commented below.
:: This theorem would be the easy way to show that any vertex in a (non
:: trivial) path graph that isn't an endvertex is a cut-vertex.
::
:: The difficulty of my Proofs lies in the difficulty of the Proofs of
:: the theorems my Proof would need. First there is
:: theorem (1) for G2 being non trivial _Graph, v1, e,v2 being object,
:: G1 being addAdjVertex of G2,v1,e,v2
:: holds G1.numComponents() = G2.numComponents();
:: which is not hard, just cumbersome. Then
:: theorem (2) for G being _Graph, v being Vertex of G,
:: G2 being removeVertex of G, v
:: st G2.numComponents() in G.numComponents()
:: holds v is isolated;
:: which is harder than it looks, especially since the converse has
:: already been proven in the preliminaries. I found it to need
:: theorem (3) for G being _Graph, u,v,w being Vertex of G
:: st v is non cut-vertex & u in G.reachableFrom(w)
:: holds ex W being Walk st W is_Walk_from w,u & not v in W.vertices();
:: for a contradiction Proof (take v to be non isolated, let w be a
:: neighbour of v; v is non cut-vertex by assumption, so use (3)
:: to show G2.reachableFrom(w) = G1.reachableFrom(w) \ {v},
:: deduce a bijection between component sets of G1 and G2 leading
:: to the contradiction).
:: Last theorem is
:: theorem (4) for G1 being non trivial _Graph, v being Vertex of G,
:: G2 being removeVertex of G1, v
:: st v is non isolated non cut-vertex
:: holds G1.numComponents() = G2.numComponents();
:: which is just a corrolary of (2) and the definition of cut-vertex.
:: Of course (2), (3) and (4) would belong into GLIB_002 to ease theorem
:: finding for future articles.
::
:: The dedicated reader is welcome to prove these theorems and the main one
:: below, or even find a shorter Proof (nevertheless theorems (1)-(3)
:: should be added to the MML because they are stating obvious facts).
::
::theorem
:: for G2 being non trivial _Graph, v1 being Vertex of G2, e,v2 being object,
:: G1 being addAdjVertex of G2,v1,e,v2, w being Vertex of G1
:: st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & w = v1
:: & v1 is non isolated
:: holds w is cut-vertex;
::proof
:: let G2 be non trivial _Graph, v1 be Vertex of G2, e,v2 be object;
:: let G1 be addAdjVertex of G2,v1,e,v2, w be Vertex of G1;
:: assume A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & w=v1
:: & v1 is non isolated;
:: for G4 being removeVertex of G1,w holds
:: G1.numComponents() in G4.numComponents()
:: proof
:: let G4 be removeVertex of G1,w;
:: set G3 = the removeVertex of G2,v1;
:: G4 is removeVertex of G1,v1 by A1;
:: G4 is addVertex of G3, v2
:: C(G1) = C(G2) by (1)
:: C(G4) = C(G3)+1
:: if v1 is cut-vertex in G2:
:: ==> C(G2) in C(G3)
:: if C(G4) = C(G1)
:: ==> C(G1) = C(G4) = C(G3)+1
:: but C(G1)+1 = C(G2)+1 in C(G3)+1, hence contradiction
:: so C(G4) <> C(G1)
:: also C(G4) < C(G1) implies w is isolated by (2)
:: so C(G4) > C(G1) qed
:: if not v1 is cut-vertex in G2:
:: v1 is non isolated
:: ==> C(G3) = C(G2) by (4)
:: ==> C(G4) = C(G1)+1
:: ==> C(G1) in C(G4) qed
:: thus thesis;
:: end;
:: hence thesis by GLIB_002:def 10;
::end;
:: also don't forget the symmetric analogon
:: (for v1, e being object, v2 being Vertex of G2)
theorem Th145:
for G2 for v1 being Vertex of G2, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
for w being Vertex of G1
st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & w = v2
holds w is endvertex
proof
let G2;
let v1 be Vertex of G2, e,v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
let w be Vertex of G1;
assume that
A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 and
A2: w = v2;
ex e1 being object st w.edgesInOut() = {e1} & not e1 Joins w,w,G1
proof
take e;
for e1 being object holds e1 in w.edgesInOut() iff e1 = e
proof
let e1 be object;
hereby
assume e1 in w.edgesInOut();
then A3: e1 in the_Edges_of G1 & ((the_Source_of G1).e1 = w or
(the_Target_of G1).e1 = w) by GLIB_000:61;
thus e1 = e
proof
assume A4: e1 <> e;
per cases by A3;
suppose (the_Source_of G1).e1 = w;
then e1 Joins (the_Target_of G1).e1, w,G1 by A3, GLIB_000:def 13;
hence contradiction by A1, A2, A4, Th137;
end;
suppose (the_Target_of G1).e1 = w;
then e1 Joins (the_Source_of G1).e1, w,G1 by A3, GLIB_000:def 13;
hence contradiction by A1, A2, A4, Th137;
end;
end;
end;
assume A5: e1 = e;
e DJoins v1,v2,G1 by A1, Th135;
then e in the_Edges_of G1 & (the_Target_of G1).e = w
by A2, GLIB_000:def 14;
hence thesis by A5, GLIB_000:61;
end;
hence w.edgesInOut() = {e} by TARSKI:def 1;
w <> v1 by A1, A2;
hence not e Joins w,w,G1 by A1, A2, Th137;
end;
hence thesis by GLIB_000:def 51;
end;
theorem Th146:
for G2 for v1, e being object, v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
for w being Vertex of G1
st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & w = v1
holds w is endvertex
proof
let G2;
let v1,e be object, v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
let w be Vertex of G1;
assume that
A1: not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 and
A2: w = v1;
ex e1 being object st w.edgesInOut() = {e1} & not e1 Joins w,w,G1
proof
take e;
for e1 being object holds e1 in w.edgesInOut() iff e1 = e
proof
let e1 be object;
hereby
assume e1 in w.edgesInOut();
then A3: e1 in the_Edges_of G1 & ((the_Source_of G1).e1 = w or
(the_Target_of G1).e1 = w) by GLIB_000:61;
thus e1 = e
proof
assume A4: e1 <> e;
per cases by A3;
suppose (the_Source_of G1).e1 = w;
then e1 Joins w, (the_Target_of G1).e1, G1 by A3, GLIB_000:def 13;
hence contradiction by A1, A2, A4, Th138;
end;
suppose (the_Target_of G1).e1 = w;
then e1 Joins w, (the_Source_of G1).e1, G1 by A3, GLIB_000:def 13;
hence contradiction by A1, A2, A4, Th138;
end;
end;
end;
assume A5: e1 = e;
e DJoins v1,v2,G1 by A1, Th136;
then e in the_Edges_of G1 & (the_Source_of G1).e = w
by A2, GLIB_000:def 14;
hence thesis by A5, GLIB_000:61;
end;
hence w.edgesInOut() = {e} by TARSKI:def 1;
w <> v2 by A1, A2;
hence not e Joins w,w,G1 by A1, A2, Th138;
end;
hence thesis by GLIB_000:def 51;
end;
theorem Th147:
for G2 for 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 _trivial
proof
let G2;
let v1 be Vertex of G2, e,v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not v2 in the_Vertices_of G2 & not e in the_Edges_of G2;
then consider G3 being addVertex of G2,v2 such that
A2: G1 is addEdge of G3,v1,e,v2 by Th129;
{v2} \ the_Vertices_of G2 <> {} by A1, ZFMISC_1:59;
then G3 is non _trivial by Th93;
hence G1 is non _trivial by A2;
end;
theorem Th148:
for G2 for 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 _trivial
proof
let G2;
let v1, e be object, v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not v1 in the_Vertices_of G2 & not e in the_Edges_of G2;
then consider G3 being addVertex of G2,v1 such that
A2: G1 is addEdge of G3,v1,e,v2 by Th130;
{v1} \ the_Vertices_of G2 <> {} by A1, ZFMISC_1:59;
then G3 is non _trivial by Th93;
hence G1 is non _trivial by A2;
end;
registration
let G be _Graph;
let v be Vertex of G;
cluster -> non _trivial
for addAdjVertex of G,v,the_Edges_of G, the_Vertices_of G;
coherence
proof
let G1 be addAdjVertex of G,v,the_Edges_of G, the_Vertices_of G;
not the_Edges_of G in the_Edges_of G &
not the_Vertices_of G in the_Vertices_of G;
hence thesis by Th147;
end;
cluster -> non _trivial
for addAdjVertex of G,the_Vertices_of G,the_Edges_of G, v;
coherence
proof
:: could have copied the Proof above, but this is
:: just a good example of effective clustering :D
let G1 be addAdjVertex of G,the_Vertices_of G,the_Edges_of G, v;
not the_Edges_of G in the_Edges_of G &
not the_Vertices_of G in the_Vertices_of G;
then consider G3 being addVertex of G,the_Vertices_of G such that
A1: G1 is addEdge of G3,the_Vertices_of G,the_Edges_of G,v by Th130;
thus G1 is non _trivial by A1;
end;
end;
registration
let G be _trivial _Graph;
let v be Vertex of G;
cluster -> complete
for addAdjVertex of G,v,the_Edges_of G,the_Vertices_of G;
coherence
proof
let G1 be addAdjVertex of G,v,the_Edges_of G,the_Vertices_of G;
for u1,u2 being Vertex of G1 st u1 <> u2 holds u1, u2 are_adjacent
proof
let u1,u2 be Vertex of G1;
assume A1: u1 <> u2;
set e = the_Edges_of G;
consider w being Vertex of G such that
A2: the_Vertices_of G = {w} by GLIB_000:22;
A3: v = w by A2, TARSKI:def 1;
A4: not the_Edges_of G in the_Edges_of G &
not the_Vertices_of G in the_Vertices_of G;
then A5: e Joins w,{w},G1 by A2, A3, Th135;
the_Vertices_of G1
= the_Vertices_of G \/ {the_Vertices_of G} by A4, Def13
.= {w, {w}} by A2, ENUMSET1:1;
then A7: {u1,u2} c= {w,{w}};
then per cases by ZFMISC_1:22;
suppose A8: u1 = w;
per cases by A7, ZFMISC_1:22;
suppose u2 = w;
hence thesis by A1, A8;
end;
suppose u2 = {w};
hence thesis by A5, A8, CHORD:def 3;
end;
end;
suppose A9: u1 = {w};
per cases by A7, ZFMISC_1:22;
suppose u2 = w;
hence thesis by CHORD:def 3, A5, A9;
end;
suppose u2 = {w};
hence thesis by A1, A9;
end;
end;
end;
hence thesis by CHORD:def 6;
end;
cluster -> complete
for addAdjVertex of G,the_Vertices_of G,the_Edges_of G,v;
coherence
proof
let G1 be addAdjVertex of G,the_Vertices_of G,the_Edges_of G,v;
for u1,u2 being Vertex of G1 st u1 <> u2 holds u1, u2 are_adjacent
proof
let u1,u2 be Vertex of G1;
assume A10: u1 <> u2;
set e = the_Edges_of G;
consider w being Vertex of G such that
A11: the_Vertices_of G = {w} by GLIB_000:22;
A12: v = w by A11, TARSKI:def 1;
A13: not the_Edges_of G in the_Edges_of G &
not the_Vertices_of G in the_Vertices_of G;
then A14: e Joins {w},w,G1 by A12, A11, Th136;
the_Vertices_of G1
= the_Vertices_of G \/ {the_Vertices_of G} by A13, Def14
.= {w, {w}} by A11, ENUMSET1:1;
then A16: {u1,u2} c= {w,{w}};
then per cases by ZFMISC_1:22;
suppose A17: u1 = w;
per cases by A16, ZFMISC_1:22;
suppose u2 = w;
hence thesis by A10, A17;
end;
suppose u2 = {w};
hence thesis by CHORD:def 3, A14, A17;
end;
end;
suppose A18: u1 = {w};
per cases by A16, ZFMISC_1:22;
suppose u2 = w;
hence thesis by A14, A18, CHORD:def 3;
end;
suppose u2 = {w};
hence thesis by A10, A18;
end;
end;
end;
hence thesis by CHORD:def 6;
end;
end;
registration
let G be loopless _Graph;
let v1,e,v2 be object;
cluster -> loopless for addAdjVertex of G,v1,e,v2;
coherence
proof
let G1 be addAdjVertex of G,v1,e,v2;
per cases;
suppose A1: v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
consider G3 being addVertex of G,v2 such that
A2: G1 is addEdge of G3,v1,e,v2 by A1, Th129;
reconsider w1=v1 as Vertex of G3 by A1, Th72;
reconsider w2=v2 as Vertex of G3 by Th98;
A3: w1 <> w2 by A1;
thus G1 is loopless by A2, A3, Th116;
end;
suppose A4: not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
consider G3 being addVertex of G,v1 such that
A5: G1 is addEdge of G3,v1,e,v2 by A4, Th130;
reconsider w2=v2 as Vertex of G3 by A4, Th72;
reconsider w1=v1 as Vertex of G3 by Th98;
A6: w1 <> w2 by A4;
thus G1 is loopless by A5, A6, Th116;
end;
suppose not (v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) &
not (not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def12;
hence thesis by GLIB_000:89;
end;
end;
end;
registration
let G be non-Dmulti _Graph;
let v1,e,v2 be object;
cluster -> non-Dmulti for addAdjVertex of G,v1,e,v2;
coherence
proof
let G1 be addAdjVertex of G,v1,e,v2;
per cases;
suppose A1: v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
consider G3 being addVertex of G,v2 such that
A2: G1 is addEdge of G3,v1,e,v2 by A1, Th129;
reconsider w1=v1 as Vertex of G3 by A1, Th72;
reconsider w2=v2 as Vertex of G3 by Th98;
A3: not ex e1 being object st e1 DJoins w1,w2,G3
proof
w2 in {w2} by TARSKI:def 1;
then w2 in {w2} \ the_Vertices_of G by A1, XBOOLE_0:def 5;
then A4: w2.edgesInOut() = {} by Th92, GLIB_000:def 49;
given e1 being object such that
A5: e1 DJoins w1,w2,G3;
e1 Joins w2,w1,G3 by A5, GLIB_000:16;
hence contradiction by A4, GLIB_000:62;
end;
thus G1 is non-Dmulti by A2, A3, Th118;
end;
suppose A6: not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
consider G3 being addVertex of G,v1 such that
A7: G1 is addEdge of G3,v1,e,v2 by A6, Th130;
reconsider w2=v2 as Vertex of G3 by A6, Th72;
reconsider w1=v1 as Vertex of G3 by Th98;
A8: not ex e1 being object st e1 DJoins w1,w2,G3
proof
w1 in {w1} by TARSKI:def 1;
then w1 in {w1} \ the_Vertices_of G by A6, XBOOLE_0:def 5;
then A9: w1.edgesInOut() = {} by Th92, GLIB_000:def 49;
given e1 being object such that
A10: e1 DJoins w1,w2,G3;
e1 Joins w1,w2,G3 by A10, GLIB_000:16;
hence contradiction by A9, GLIB_000:62;
end;
thus G1 is non-Dmulti by A7, A8, Th118;
end;
suppose not (v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) &
not (not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def12;
hence thesis by GLIB_000:89;
end;
end;
end;
registration
let G be non-multi _Graph;
let v1,e,v2 be object;
cluster -> non-multi for addAdjVertex of G,v1,e,v2;
coherence
proof
let G1 be addAdjVertex of G,v1,e,v2;
per cases;
suppose A1: v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
consider G3 being addVertex of G,v2 such that
A2: G1 is addEdge of G3,v1,e,v2 by A1, Th129;
reconsider w1=v1 as Vertex of G3 by A1, Th72;
reconsider w2=v2 as Vertex of G3 by Th98;
not ex e1 being object st e1 Joins w1,w2,G3
proof
w2 in {w2} by TARSKI:def 1;
then w2 in {w2} \ the_Vertices_of G by A1, XBOOLE_0:def 5;
then A3: w2.edgesInOut() = {} by Th92, GLIB_000:def 49;
given e1 being object such that
A4: e1 Joins w1,w2,G3;
e1 Joins w2,w1,G3 by A4, GLIB_000:14;
hence contradiction by A3, GLIB_000:62;
end;
then A5: not w1,w2 are_adjacent by CHORD:def 3;
thus G1 is non-multi by A2, A5, Th120;
end;
suppose A6: not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
consider G3 being addVertex of G,v1 such that
A7: G1 is addEdge of G3,v1,e,v2 by A6, Th130;
reconsider w2=v2 as Vertex of G3 by A6, Th72;
reconsider w1=v1 as Vertex of G3 by Th98;
not ex e1 being object st e1 Joins w1,w2,G3
proof
w1 in {w1} by TARSKI:def 1;
then w1 in {w1} \ the_Vertices_of G by A6, XBOOLE_0:def 5;
then A8: w1.edgesInOut() = {} by Th92, GLIB_000:def 49;
given e1 being object such that
A9: e1 Joins w1,w2,G3;
thus contradiction by A8, A9, GLIB_000:62;
end;
hence G1 is non-multi by A7, Th120, CHORD:def 3;
end;
suppose not (v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) &
not (not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def12;
hence thesis by GLIB_000:89;
end;
end;
end;
registration
let G be Dsimple _Graph;
let v1,e,v2 be object;
cluster -> Dsimple for addAdjVertex of G,v1,e,v2;
coherence;
end;
registration
let G be simple _Graph;
let v1,e,v2 be object;
cluster -> simple for addAdjVertex of G,v1,e,v2;
coherence;
end;
theorem Th149:
for G2 for v1 being Vertex of G2, e,v2 being object
for G1 being addAdjVertex of G2,v1,e,v2, W being Walk of G1
st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 &
((not e in W.edges() & W is non trivial) or not v2 in W.vertices())
holds W is Walk of G2
proof
let G2;
let v1 be Vertex of G2, e,v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
let W be Walk of G1;
assume that
A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 and
A2: (not e in W.edges() & W is non trivial) or not v2 in W.vertices();
reconsider w=v2, e1=e as set by TARSKI:1;
per cases by A2;
suppose A3: not e in W.edges() & W is non trivial;
consider G3 being addVertex of G2,v2 such that
A4: G1 is addEdge of G3,v1,e,v2 by A1, Th129;
A5: not e in the_Edges_of G3 by A1, Def10;
A6: v1 is Vertex of G3 by Th72;
v2 is Vertex of G3 by Th98;
then G3 is removeEdge of G1, e1 by A4, A5, A6, Th112;
then reconsider W3=W as Walk of G3 by A3, GLIB_001:172;
W3.vertices() misses {v2} \ the_Vertices_of G2 by A3, Th94;
hence thesis by Th95;
end;
suppose A7: not v2 in W.vertices();
reconsider G3=G2 as removeVertex of G1, w by A1, Th141;
reconsider w as Vertex of G1 by A1, Th133;
A8: not w in W.vertices() by A7;
G1 is non _trivial by A1, Th147;
then W is Walk of G3 by A8, GLIB_001:171;
hence thesis;
end;
end;
theorem Th150:
for G2 for v1, e being object, v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2, W being Walk of G1
st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 &
((not e in W.edges() & W is non trivial) or not v1 in W.vertices())
holds W is Walk of G2
proof
let G2;
let v1, e be object, v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
let W be Walk of G1;
assume that
A1: not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 and
A2: (not e in W.edges() & W is non trivial) or not v1 in W.vertices();
reconsider w=v1, e1=e as set by TARSKI:1;
per cases by A2;
suppose A3: not e in W.edges() & W is non trivial;
consider G3 being addVertex of G2,v1 such that
A4: G1 is addEdge of G3,v1,e,v2 by A1, Th130;
A5: not e in the_Edges_of G3 by A1, Def10;
A6: v2 is Vertex of G3 by Th72;
v1 is Vertex of G3 by Th98;
then G3 is removeEdge of G1, e1 by A4, A5, A6, Th112;
then reconsider W3=W as Walk of G3 by A3, GLIB_001:172;
W3.vertices() misses {v1} \ the_Vertices_of G2 by A3, Th94;
hence thesis by Th95;
end;
suppose A7: not v1 in W.vertices();
reconsider G3=G2 as removeVertex of G1, w by A1, Th142;
reconsider w as Vertex of G1 by A1, Th134;
A8: not w in W.vertices() by A7;
G1 is non _trivial by A1, Th148;
then W is Walk of G3 by A8, GLIB_001:171;
hence thesis;
end;
end;
theorem Th151:
for G2 for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2, T being Trail of G1
st not e in the_Edges_of G2 & T.first() in the_Vertices_of G2 &
T.last() in the_Vertices_of G2
holds not e in T.edges()
proof
let G2;
let v1,e,v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
let T be Trail of G1;
assume that
A1: not e in the_Edges_of G2 and
A2: T.first() in the_Vertices_of G2 & T.last() in the_Vertices_of G2;
per cases;
suppose A3: v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2;
per cases;
suppose A4: v2 in T.vertices();
reconsider w=v2 as Vertex of G1 by A1, A3, Th133;
w is endvertex by A1, A3, Th145;
hence thesis by A2, A3, A4, GLIB_001:143;
end;
suppose not v2 in T.vertices();
then reconsider W=T as Walk of G2 by A1, A3, Th149;
not e in W.edges() by A1;
hence thesis by GLIB_001:110;
end;
end;
suppose A6: not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2;
per cases;
suppose A7: v1 in T.vertices();
reconsider w=v1 as Vertex of G1 by A1, A6, Th134;
w is endvertex by A1, A6, Th146;
hence thesis by A2, A6, A7, GLIB_001:143;
end;
suppose not v1 in T.vertices();
then reconsider W=T as Walk of G2 by A1, A6, Th150;
not e in W.edges() by A1;
hence thesis by GLIB_001:110;
end;
end;
suppose not (v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2) &
not (not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2);
then G1 == G2 by Def12;
then not e in the_Edges_of G1 by A1, GLIB_000:def 34;
hence not e in T.edges();
end;
end;
registration
let G be connected _Graph;
let v1,e,v2 be object;
cluster -> connected for addAdjVertex of G,v1,e,v2;
coherence
proof
let G1 be addAdjVertex of G,v1,e,v2;
per cases;
suppose A1: v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
for u1,u2 being Vertex of G1 holds
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2
proof
let u1,u2 be Vertex of G1;
per cases;
suppose u1 in the_Vertices_of G;
then reconsider w1=u1 as Vertex of G;
per cases;
suppose u2 in the_Vertices_of G;
then reconsider w2=u2 as Vertex of G;
consider W being Walk of G such that
A2: W is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W1=W as Walk of G1 by Th79;
take W1;
thus W1 is_Walk_from u1,u2 by A2, GLIB_001:19;
end;
suppose A3: not u2 in the_Vertices_of G;
the_Vertices_of G1 = the_Vertices_of G \/ {v2} by A1, Def12;
then u2 in {v2} by A3, XBOOLE_0:def 3;
then u2=v2 by TARSKI:def 1;
then A4: e Joins v1,u2,G1 by A1, Th135;
reconsider w2=v1 as Vertex of G by A1;
consider W2 being Walk of G such that
A5: W2 is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W=W2 as Walk of G1 by Th79;
W is_Walk_from u1,v1 by A5, GLIB_001:19;
then A6: W.first() = u1 & W.last() = v1 by GLIB_001:def 23;
set W1=W.addEdge(e);
take W1;
thus thesis by A4, A6, GLIB_001:63;
end;
end;
suppose A7: not u1 in the_Vertices_of G;
A8: the_Vertices_of G1 = the_Vertices_of G \/ {v2} by A1, Def12;
then u1 in {v2} by A7, XBOOLE_0:def 3;
then A9: u1=v2 by TARSKI:def 1;
then e DJoins v1,u1,G1 by A1, Th135;
then A10: e Joins u1,v1,G1 by GLIB_000:16;
per cases;
suppose u2 in the_Vertices_of G;
then reconsider w2=u2 as Vertex of G;
reconsider w1=v1 as Vertex of G by A1;
consider W2 being Walk of G such that
A11: W2 is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W=W2 as Walk of G1 by Th79;
W is_Walk_from v1,u2 by A11, GLIB_001:19;
then A12: W.first() = v1 & W.last() = u2 by GLIB_001:def 23;
set W3 = G1.walkOf(u1,e,v1);
A13: W3.first() = u1 & W3.last() = v1 by A10, GLIB_001:15;
set W1 = W3.append(W);
take W1;
thus thesis by A12, A13, GLIB_001:30;
end;
suppose not u2 in the_Vertices_of G;
then u2 in {v2} by A8, XBOOLE_0:def 3;
then u2=u1 by TARSKI:def 1, A9;
then A14: G1.walkOf(u1) is_Walk_from u1,u2 by GLIB_001:13;
take G1.walkOf(u1);
thus thesis by A14;
end;
end;
end;
hence thesis by GLIB_002:def 1;
end;
suppose A15: not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
for u1,u2 being Vertex of G1 holds
ex W1 being Walk of G1 st W1 is_Walk_from u1,u2
proof
let u1,u2 be Vertex of G1;
per cases;
suppose u1 in the_Vertices_of G;
then reconsider w1=u1 as Vertex of G;
per cases;
suppose u2 in the_Vertices_of G;
then reconsider w2=u2 as Vertex of G;
consider W being Walk of G such that
A16: W is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W1=W as Walk of G1 by Th79;
take W1;
thus W1 is_Walk_from u1,u2 by A16, GLIB_001:19;
end;
suppose A17: not u2 in the_Vertices_of G;
the_Vertices_of G1 = the_Vertices_of G \/ {v1} by A15, Def12;
then u2 in {v1} by A17, XBOOLE_0:def 3;
then u2=v1 by TARSKI:def 1;
then e DJoins u2,v2,G1 by A15, Th136;
then A18: e Joins v2,u2,G1 by GLIB_000:16;
reconsider w2=v2 as Vertex of G by A15;
consider W2 being Walk of G such that
A19: W2 is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W=W2 as Walk of G1 by Th79;
W is_Walk_from u1,v2 by A19, GLIB_001:19;
then A20: W.first() = u1 & W.last() = v2 by GLIB_001:def 23;
set W1=W.addEdge(e);
take W1;
thus thesis by A18, A20, GLIB_001:63;
end;
end;
suppose A21: not u1 in the_Vertices_of G;
A22: the_Vertices_of G1 = the_Vertices_of G \/ {v1} by A15, Def12;
then u1 in {v1} by A21, XBOOLE_0:def 3;
then A23: u1=v1 by TARSKI:def 1;
then A24: e Joins u1,v2,G1 by A15, Th136;
per cases;
suppose u2 in the_Vertices_of G;
then reconsider w2=u2 as Vertex of G;
reconsider w1=v2 as Vertex of G by A15;
consider W2 being Walk of G such that
A25: W2 is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W=W2 as Walk of G1 by Th79;
W is_Walk_from v2,u2 by A25, GLIB_001:19;
then A26: W.first() = v2 & W.last() = u2 by GLIB_001:def 23;
set W3 = G1.walkOf(u1,e,v2);
A27: W3.first() = u1 & W3.last() = v2 by A24, GLIB_001:15;
set W1 = W3.append(W);
take W1;
thus thesis by A26, A27, GLIB_001:30;
end;
suppose not u2 in the_Vertices_of G;
then u2 in {v1} by A22, XBOOLE_0:def 3;
then u2=u1 by TARSKI:def 1, A23;
then A28: G1.walkOf(u1) is_Walk_from u1,u2 by GLIB_001:13;
take G1.walkOf(u1);
thus thesis by A28;
end;
end;
end;
hence thesis by GLIB_002:def 1;
end;
suppose not (v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) &
not (not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def12;
hence thesis by GLIB_002:8;
end;
end;
end;
registration
let G be non connected _Graph;
let v1,e,v2 be object;
cluster -> non connected for addAdjVertex of G,v1,e,v2;
coherence
proof
let G1 be addAdjVertex of G,v1,e,v2;
per cases;
suppose A1: v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
ex u1,u2 being Vertex of G1 st
for W1 being Walk of G1 holds not W1 is_Walk_from u1,u2
proof
consider w1,w2 being Vertex of G such that
A2: for W being Walk of G holds not W is_Walk_from w1,w2
by GLIB_002:def 1;
reconsider u1=w1,u2=w2 as Vertex of G1 by Th72;
take u1, u2;
let W1 be Walk of G1;
assume A3: W1 is_Walk_from u1,u2;
set T = the Trail of W1;
W1.first() = u1 & W1.last() = u2 by A3, GLIB_001:def 23;
then A4: T is_Walk_from u1,u2 by GLIB_001:def 32;
then A5: T.first() = w1 & T.last() = w2 by GLIB_001:def 23;
w1 <> w2
proof
assume w1 = w2;
then G.walkOf(w1) is_Walk_from w1,w2 by GLIB_001:13;
hence contradiction by A2;
end;
then A6: T is non trivial by A5, GLIB_001:127;
not e in T.edges() by A1, A5, Th151;
then reconsider W=T as Walk of G by A1, A6, Th149;
W is_Walk_from w1,w2 by A4, GLIB_001:19;
hence contradiction by A2;
end;
hence thesis by GLIB_002:def 1;
end;
suppose A7: not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
ex u1,u2 being Vertex of G1 st
for W1 being Walk of G1 holds not W1 is_Walk_from u1,u2
proof
consider w1,w2 being Vertex of G such that
A8: for W being Walk of G holds not W is_Walk_from w1,w2
by GLIB_002:def 1;
reconsider u1=w1,u2=w2 as Vertex of G1 by Th72;
take u1, u2;
let W1 be Walk of G1;
assume A9: W1 is_Walk_from u1,u2;
set T = the Trail of W1;
W1.first() = u1 & W1.last() = u2 by A9, GLIB_001:def 23;
then A10: T is_Walk_from u1,u2 by GLIB_001:def 32;
then A11: T.first() = w1 & T.last() = w2 by GLIB_001:def 23;
w1 <> w2
proof
assume w1 = w2;
then G.walkOf(w1) is_Walk_from w1,w2 by GLIB_001:13;
hence contradiction by A8;
end;
then A12: T is non trivial by A11, GLIB_001:127;
not e in T.edges() by A7, A11, Th151;
then reconsider W=T as Walk of G by A7, A12, Th150;
W is_Walk_from w1,w2 by A10, GLIB_001:19;
hence contradiction by A8;
end;
hence thesis by GLIB_002:def 1;
end;
suppose not (v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) &
not (not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def12;
hence thesis by GLIB_002:8;
end;
end;
end;
registration
let G be acyclic _Graph;
let v1,e,v2 be object;
cluster -> acyclic for addAdjVertex of G,v1,e,v2;
coherence
proof
let G1 be addAdjVertex of G,v1,e,v2;
per cases;
suppose A1: v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
consider G3 being addVertex of G,v2 such that
A2: G1 is addEdge of G3,v1,e,v2 by A1, Th129;
reconsider w1=v1 as Vertex of G3 by A1, Th72;
A3: v2 in {v2} by TARSKI:def 1;
reconsider w2=v2 as Vertex of G3 by Th98;
w2 in {v2} \ the_Vertices_of G by A3, A1, XBOOLE_0:def 5;
then w2 is isolated by Th92;
then not w1 in G3.reachableFrom w2 by A1, Th53;
then not w2 in G3.reachableFrom w1 by Th54;
hence G1 is acyclic by A2, Th122;
end;
suppose A6: not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
consider G3 being addVertex of G,v1 such that
A7: G1 is addEdge of G3,v1,e,v2 by A6, Th130;
reconsider w2=v2 as Vertex of G3 by A6, Th72;
A8: v1 in {v1} by TARSKI:def 1;
reconsider w1=v1 as Vertex of G3 by Th98;
w1 in {v1} \ the_Vertices_of G by A8, A6, XBOOLE_0:def 5;
then A9: w1 is isolated by Th92;
not w2 in G3.reachableFrom w1 by A6, A9, Th53;
hence G1 is acyclic by A7, Th122;
end;
suppose not (v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) &
not (not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G);
then G1 == G by Def12;
hence thesis by GLIB_002:44;
end;
end;
end;
registration
let G be Tree-like _Graph;
let v1,e,v2 be object;
cluster -> Tree-like for addAdjVertex of G,v1,e,v2;
coherence;
end;
theorem Th152:
for G2 for v1 being Vertex of G2, e,v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2
& G2 is non _trivial
holds G1 is non complete
proof
let G2;
let v1 be Vertex of G2, e,v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
assume that
A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 and
A2: G2 is non _trivial;
ex u,v being Vertex of G1 st u <> v & not u, v are_adjacent
proof
consider u1,u2 being Vertex of G2 such that
A3: u1 <> u2 by A2, GLIB_000:21;
A4: u1 <> v2 & u2 <> v2 by A1;
reconsider u1,u2 as Vertex of G1 by Th72;
reconsider v2 as Vertex of G1 by A1, Th133;
per cases;
suppose A5: u1 <> v1;
take u1,v2;
not ex e1 being object st e1 Joins u1,v2,G1 by A1, A5, Th137;
hence thesis by A4, CHORD:def 3;
end;
suppose A6: u2 <> v1;
take u2,v2;
not ex e1 being object st e1 Joins u2,v2,G1 by A1, A6, Th137;
hence thesis by A4, CHORD:def 3;
end;
suppose u1=v1 & u2=v1;
hence thesis by A3;
end;
end;
hence thesis by CHORD:def 6;
end;
theorem Th153:
for G2 for v1, e being object, v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2
& G2 is non _trivial
holds G1 is non complete
proof
let G2;
let v1,e be object, v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
assume that
A1: not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 and
A2: G2 is non _trivial;
ex u,v being Vertex of G1 st u <> v & not u, v are_adjacent
proof
consider u1,u2 being Vertex of G2 such that
A3: u1 <> u2 by A2, GLIB_000:21;
A4: u1 <> v1 & u2 <> v1 by A1;
reconsider u1,u2 as Vertex of G1 by Th72;
reconsider v1 as Vertex of G1 by A1, Th134;
per cases;
suppose A5: u1 <> v2;
take v1,u1;
not ex e1 being object st e1 Joins v1,u1,G1 by A1, A5, Th138;
hence thesis by A4, CHORD:def 3;
end;
suppose A6: u2 <> v2;
take v1,u2;
not ex e1 being object st e1 Joins v1,u2,G1 by A1, A6, Th138;
hence thesis by A4, CHORD:def 3;
end;
suppose u1=v2 & u2=v2;
hence thesis by A3;
end;
end;
hence thesis by CHORD:def 6;
end;
registration
let G be non complete _Graph;
let v1,e,v2 be object;
cluster -> non complete for addAdjVertex of G,v1,e,v2;
coherence
proof
let G1 be addAdjVertex of G,v1,e,v2;
A1: G is non _trivial;
per cases;
suppose v1 in the_Vertices_of G & not e in the_Edges_of G &
not v2 in the_Vertices_of G;
hence G1 is non complete by A1, Th152;
end;
suppose not v1 in the_Vertices_of G & not e in the_Edges_of G &
v2 in the_Vertices_of G;
hence G1 is non complete by A1, Th153;
end;
suppose not (v1 in the_Vertices_of G & not e in the_Edges_of G &
not v2 in the_Vertices_of G) &
not (not v1 in the_Vertices_of G & not e in the_Edges_of G &
v2 in the_Vertices_of G);
then G == G1 by Def12;
hence thesis by CHORD:62;
end;
end;
end;
registration
let G be non _trivial _Graph;
let v be Vertex of G;
cluster -> non complete
for addAdjVertex of G,v,the_Edges_of G,the_Vertices_of G;
coherence
proof
let G1 be addAdjVertex of G,v,the_Edges_of G,the_Vertices_of G;
not the_Edges_of G in the_Edges_of G &
not the_Vertices_of G in the_Vertices_of G;
hence thesis by Th152;
end;
cluster -> non complete
for addAdjVertex of G,the_Vertices_of G,the_Edges_of G,v;
coherence
proof
let G1 be addAdjVertex of G,the_Vertices_of G,the_Edges_of G,v;
not the_Edges_of G in the_Edges_of G &
not the_Vertices_of G in the_Vertices_of G;
hence thesis by Th153;
end;
end;
theorem
for G2 for v1 being Vertex of G2, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2
holds G1.order() = G2.order() +` 1 & G1.size() = G2.size() +` 1
proof
let G2;
let v1 be Vertex of G2, e, v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v2} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by Def13;
A3: the_Vertices_of G2 misses {v2} & the_Edges_of G2 misses {e}
by A1, ZFMISC_1:50;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= card the_Vertices_of G2 +` card {v2} by A2, A3, CARD_2:35
.= G2.order() +` card {v2} by GLIB_000:def 24
.= G2.order() +` 1 by CARD_2:42;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= card the_Edges_of G2 +` card {e} by A2, A3, CARD_2:35
.= G2.size() +` card {e} by GLIB_000:def 25
.= G2.size() +` 1 by CARD_2:42;
end;
theorem
for G2 for v1, e being object, v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2
holds G1.order() = G2.order() +` 1 & G1.size() = G2.size() +` 1
proof
let G2;
let v1, e being object, v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2 & not v1 in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v1} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by Def14;
A3: the_Vertices_of G2 misses {v1} & the_Edges_of G2 misses {e}
by A1, ZFMISC_1:50;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= card the_Vertices_of G2 +` card {v1} by A2, A3, CARD_2:35
.= G2.order() +` card {v1} by GLIB_000:def 24
.= G2.order() +` 1 by CARD_2:42;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= card the_Edges_of G2 +` card {e} by A2, A3, CARD_2:35
.= G2.size() +` card {e} by GLIB_000:def 25
.= G2.size() +` 1 by CARD_2:42;
end;
theorem
for G2 being _finite _Graph, v1 being Vertex of G2, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2
holds G1.order() = G2.order() + 1 & G1.size() = G2.size() + 1
proof
let G2 be _finite _Graph;
let v1 be Vertex of G2, e, v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v2} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by Def13;
A3: the_Vertices_of G2 misses {v2} & the_Edges_of G2 misses {e}
by A1, ZFMISC_1:50;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= card the_Vertices_of G2 + card {v2} by A2, A3, CARD_2:40
.= G2.order() + card {v2} by GLIB_000:def 24
.= G2.order() + 1 by CARD_2:42;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= card the_Edges_of G2 + card {e} by A2, A3, CARD_2:40
.= G2.size() + card {e} by GLIB_000:def 25
.= G2.size() + 1 by CARD_2:42;
end;
theorem
for G2 being _finite _Graph for v1, e being object, v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2
holds G1.order() = G2.order() + 1 & G1.size() = G2.size() + 1
proof
let G2 be _finite _Graph;
let v1, e being object, v2 be Vertex of G2;
let G1 be addAdjVertex of G2,v1,e,v2;
assume A1: not e in the_Edges_of G2 & not v1 in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v1} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by Def14;
A3: the_Vertices_of G2 misses {v1} & the_Edges_of G2 misses {e}
by A1, ZFMISC_1:50;
thus G1.order() = card the_Vertices_of G1 by GLIB_000:def 24
.= card the_Vertices_of G2 + card {v1} by A2, A3, CARD_2:40
.= G2.order() + card {v1} by GLIB_000:def 24
.= G2.order() + 1 by CARD_2:42;
thus G1.size() = card the_Edges_of G1 by GLIB_000:def 25
.= card the_Edges_of G2 + card {e} by A2, A3, CARD_2:40
.= G2.size() + card {e} by GLIB_000:def 25
.= G2.size() + 1 by CARD_2:42;
end;
registration
let G be _finite _Graph;
let v1,e,v2 be object;
cluster -> _finite for addAdjVertex of G,v1,e,v2;
coherence
proof
let G1 be addAdjVertex of G,v1,e,v2;
per cases;
suppose v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v2} &
the_Edges_of G1 = the_Edges_of G \/ {e} by Def12;
hence thesis by GLIB_000:def 17;
end;
suppose not v1 in the_Vertices_of G & v2 in the_Vertices_of G &
not e in the_Edges_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v1} &
the_Edges_of G1 = the_Edges_of G \/ {e} by Def12;
hence thesis by GLIB_000:def 17;
end;
suppose not ((v1 in the_Vertices_of G & not v2 in the_Vertices_of G &
not e in the_Edges_of G) or (not v1 in the_Vertices_of G &
v2 in the_Vertices_of G & not e in the_Edges_of G));
then G1 == G by Def12;
hence thesis by GLIB_000:89;
end;
end;
end;
:: added by SK, 9.12.2024
registration
let G be non _trivial connected _Graph;
cluster -> non isolated for Vertex of G;
coherence
proof
let v be Vertex of G;
set w = the Element of (the_Vertices_of G) \ {v};
(the_Vertices_of G) \ {v} <> {} by GLIB_000:20;
then A1: w in the_Vertices_of G & w <> v by ZFMISC_1:56;
then reconsider w as Vertex of G;
consider W being Walk of G such that
A2: W is_Walk_from v,w by GLIB_002:def 1;
w in G.reachableFrom(v) by A2, GLIB_002:def 5;
hence thesis by A1, Th53;
end;
end;