:: Euler circuits and paths
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received July 29, 1997
:: Copyright (c) 1997-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_2, XBOOLE_0, SUBSET_1, FINSEQ_1, ABIAN, INT_1,
ARYTM_1, RELAT_1, XXREAL_0, ARYTM_3, GRAPH_2, FUNCT_1, CARD_1, GRAPH_1,
GLIB_000, STRUCT_0, TREES_2, ORDINAL4, NAT_1, PARTFUN1, TARSKI, RELAT_2,
FINSET_1, FUNCT_4, FUNCOP_1, ZFMISC_1, FINSEQ_6, GRAPH_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, INT_1,
NAT_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, XXREAL_2, STRUCT_0,
GRAPH_1, GRAPH_2, MSSCYC_1, ABIAN, XXREAL_0, FINSEQ_6;
constructors WELLORD2, FUNCT_4, FINSEQ_4, ABIAN, GRAPH_2, MSSCYC_1, XXREAL_2,
RELSET_1, PRE_POLY, FINSEQ_6;
registrations XBOOLE_0, ORDINAL1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0,
NAT_1, INT_1, CARD_1, MEMBERED, FINSEQ_1, ABIAN, GRAPH_2, MSSCYC_1,
RELAT_1, XXREAL_2, STRUCT_0, RELSET_1, FINSEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, PARTFUN1, GRAPH_1, GRAPH_2, MSSCYC_1, XBOOLE_0;
equalities GRAPH_1, GRAPH_2, FUNCOP_1;
expansions TARSKI, GRAPH_1, GRAPH_2, MSSCYC_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, NAT_1, FUNCOP_1,
FUNCT_4, PARTFUN1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSEQ_4, FINSEQ_5, GRAPH_1, GRAPH_2, MSSCYC_1, ABIAN, RELSET_1,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, XXREAL_2, INT_1,
XTUPLE_0, FINSEQ_6;
schemes NAT_1, DOMAIN_1, XBOOLE_0, RECDEF_1;
begin :: Preliminaries
definition
let D be set, T be non empty FinSequenceSet of D,
S be non empty Subset of T;
redefine mode Element of S -> FinSequence of D; :: redefines Element (SUBSET_1, definition)
coherence
proof
let x be Element of S;
x is Element of T;
hence thesis;
end;
end;
registration
let i, j be even Integer;
cluster i-j -> even;
coherence
proof
2 divides j by ABIAN:def 1;
then consider l being Integer such that
A1: j = 2*l by INT_1:def 3;
2 divides i by ABIAN:def 1;
then consider k being Integer such that
A2: i = 2*k by INT_1:def 3;
i-j = 2*(k-l) by A2,A1;
hence thesis;
end;
end;
theorem
for i, j being Integer holds (i is even iff j is even) iff (i-j) is even;
Lm1: for p be FinSequence, m, n be Nat st 1<=m & m<=n+1 & n<=len p
holds len (m, n)-cut p +m = n+1 & for i being Nat st i<len (m, n)
-cut p holds ((m, n)-cut p).(i+1)=p.(m+i)
proof
let p be FinSequence, m, n be Nat such that
A1: 1<=m and
A2: m<=n+1 and
A3: n<=len p;
A4: m = n+1 or m < n+1 by A2,XXREAL_0:1;
per cases by A4,NAT_1:13;
suppose
A5: m = n+1;
then n < m by XREAL_1:29;
then (m, n)-cut p = {} by FINSEQ_6:def 4;
hence len (m, n)-cut p +m = n+1 by A5;
not(1<=m & m<=n & n<=len p) by A5,XREAL_1:29;
hence thesis by CARD_1:27,FINSEQ_6:def 4;
end;
suppose
m<=n;
hence thesis by A1,A3,FINSEQ_6:def 4;
end;
end;
theorem Th2:
for p being FinSequence, m, n, a being Nat st a in dom
(m, n)-cut p ex k being Nat st k in dom p & p.k = ((m,n)-cut p).a &
k+1 = m+a & m <= k & k <= n
proof
let p be FinSequence, m, n, a be Nat such that
A1: a in dom (m, n)-cut p;
set cp = (m,n)-cut p;
A2: a <= len cp by A1,FINSEQ_3:25;
per cases;
suppose
A3: 1<=m & m<=n & n<=len p;
0+1<= a by A1,FINSEQ_3:25;
then consider i1 being Nat such that
0<=i1 and
A4: i1<len cp and
A5: a=i1+1 by A2,FINSEQ_6:127;
take k = m+i1;
m <= k by NAT_1:11;
then
A6: 1 <= k by A3,XXREAL_0:2;
A7: len cp +m = n+1 by A3,FINSEQ_6:def 4;
A8: m+i1 < m + len cp by A4,XREAL_1:6;
then m+i1 <= n by A7,NAT_1:13;
then k <= len p by A3,XXREAL_0:2;
hence k in dom p by A6,FINSEQ_3:25;
thus p.k = cp.a by A3,A4,A5,FINSEQ_6:def 4;
thus k+1 = m+a by A5;
thus thesis by A7,A8,NAT_1:11,13;
end;
suppose
not (1<=m & m<=n & n<=len p);
hence thesis by A1,FINSEQ_6:def 4,RELAT_1:38;
end;
end;
definition
let G be Graph;
mode Vertex of G is Element of the carrier of G;
end;
reserve G for Graph,
v, v1, v2 for Vertex of G,
c for Chain of G,
p, p1, p2 for Path of G,
vs, vs1, vs2 for FinSequence of the carrier of G,
e, X for set,
n, m for Nat;
theorem
vs is_vertex_seq_of c implies vs is non empty;
Lm2: 1 <= n & n <= len p & 1 <= m & m <= len p & n<>m implies p.n <> p.m
proof
assume that
A1: 1 <= n & n <= len p & 1 <= m & m <= len p and
A2: n<>m;
n in dom p & m in dom p by A1,FINSEQ_3:25;
hence thesis by A2,FUNCT_1:def 4;
end;
theorem Th4:
e in the carrier' of G implies <*e*> is Path of G
proof
assume e in the carrier' of G;
then reconsider c = <*e*> as Chain of G by MSSCYC_1:5;
now
let n, m be Nat;
A1: len c = 1 by FINSEQ_1:39;
assume 1 <= n & n < m & m <= len c;
hence c.n <> c.m by A1,XXREAL_0:2;
end;
hence thesis by GRAPH_1:def 16;
end;
theorem Th5:
(m,n)-cut p is Path of G
proof
per cases;
suppose
not 1<=m or not n<=len p or m > n;
then (m,n)-cut p = {} by FINSEQ_6:def 4;
hence thesis by GRAPH_1:14;
end;
suppose
1<=m & m<=n & n<=len p;
then reconsider q = (m,n)-cut p as Chain of G by GRAPH_2:41;
assume not (m,n)-cut p is Path of G;
then consider a, b being Nat such that
A1: 1 <= a and
A2: a < b and
A3: b <= len q and
A4: q.a = q.b by GRAPH_1:def 16;
1 <= b by A1,A2,XXREAL_0:2;
then b in dom q by A3,FINSEQ_3:25;
then consider kb being Nat such that
A5: kb in dom p & p.kb = q.b and
A6: kb+1 = m+b and
m <= kb and
kb <= n by Th2;
a <= len q by A2,A3,XXREAL_0:2;
then a in dom q by A1,FINSEQ_3:25;
then consider ka being Nat such that
A7: ka in dom p & p.ka = q.a and
A8: ka+1 = m+a and
m <= ka and
ka <= n by Th2;
ka = kb by A4,A7,A5,FUNCT_1:def 4;
hence contradiction by A2,A8,A6;
end;
end;
theorem Th6:
rng p1 misses rng p2 & vs1 is_vertex_seq_of p1 & vs2
is_vertex_seq_of p2 & vs1.len vs1 = vs2.1 implies p1^p2 is Path of G
proof
set c1 = p1, c2 = p2;
assume that
A1: rng c1 misses rng c2 and
A2: vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1.len vs1 = vs2.1;
reconsider c = c1^c2 as Chain of G by A2,GRAPH_2:43;
now
let n, m be Nat such that
A3: 1 <= n and
A4: n < m and
A5: m <= len c and
A6: c.n = c.m;
1 <= m by A3,A4,XXREAL_0:2;
then
A7: m in dom c by A5,FINSEQ_3:25;
n <= len c by A4,A5,XXREAL_0:2;
then
A8: n in dom c by A3,FINSEQ_3:25;
per cases by A8,A7,FINSEQ_1:25;
suppose
A9: n in dom c1 & m in dom c1;
then c1.n = c.n by FINSEQ_1:def 7
.= c1.m by A6,A9,FINSEQ_1:def 7;
hence contradiction by A4,A9,FUNCT_1:def 4;
end;
suppose
A10: n in dom c1 & ex m2 being Nat st m2 in dom c2 & m=len c1 + m2;
then
A11: c1.n in rng c1 by FUNCT_1:def 3;
consider m2 being Nat such that
A12: m2 in dom c2 and
A13: m=len c1 + m2 by A10;
A14: c2.m2 in rng c2 by A12,FUNCT_1:def 3;
c1.n = c.n by A10,FINSEQ_1:def 7
.= c2.m2 by A6,A12,A13,FINSEQ_1:def 7;
hence contradiction by A1,A11,A14,XBOOLE_0:3;
end;
suppose
A15: m in dom c1 & ex n2 being Nat st n2 in dom c2 & n=len c1 + n2;
then consider n2 being Nat such that
n2 in dom c2 and
A16: n=len c1 + n2;
m <= len c1 by A15,FINSEQ_3:25;
then len c1 + n2 < len c1 by A4,A16,XXREAL_0:2;
hence contradiction by NAT_1:11;
end;
suppose
A17: (ex n2 being Nat st n2 in dom c2 & n=len c1 + n2) & ex m2 being
Nat st m2 in dom c2 & m=len c1 + m2;
then consider n2 being Nat such that
A18: n2 in dom c2 & n=len c1 + n2;
consider m2 being Nat such that
A19: m2 in dom c2 & m=len c1 + m2 by A17;
c2.n2 = c.n by A18,FINSEQ_1:def 7
.= c2.m2 by A6,A19,FINSEQ_1:def 7;
hence contradiction by A4,A19,A18,FUNCT_1:def 4;
end;
end;
hence thesis by GRAPH_1:def 16;
end;
theorem Th7:
c = {} implies c is cyclic
proof
set v = the Vertex of G;
assume c = {};
then
A1: <*v*> is_vertex_seq_of c by GRAPH_2:32;
<*v*>.1 = <*v*>.len <*v*> by FINSEQ_1:40;
hence thesis by A1;
end;
registration
let G be Graph;
cluster cyclic for Path of G;
existence
proof
reconsider p = {} as Path of G by GRAPH_1:14;
take p;
thus thesis by Th7;
end;
end;
theorem Th8:
for p being cyclic Path of G holds ((m+1,len p)-cut p)^(1,m)-cut
p is cyclic Path of G
proof
let p be cyclic Path of G;
per cases by NAT_1:14,XXREAL_0:1;
suppose
A1: m = 0;
0 <= len p;
then len (1,m)-cut p +1 = 0+1 by A1,Lm1;
then
A2: (1,m)-cut p = {};
(m+1,len p)-cut p = p by A1,FINSEQ_6:133;
hence thesis by A2,FINSEQ_1:34;
end;
suppose
A3: 1 <= m & len p = m;
1 <= m+1 by NAT_1:12;
then len (m+1,len p)-cut p +(m+1) = len p +1 by A3,Lm1;
then (m+1,len p)-cut p = {} by A3;
then ((m+1,len p)-cut p)^(1,m)-cut p = (1,m)-cut p by FINSEQ_1:34
.= p by A3,FINSEQ_6:133;
hence thesis;
end;
suppose
A4: 1 <= m & len p < m;
m <= m+1 by NAT_1:11;
then len p < m+1 by A4,XXREAL_0:2;
then
A5: (m+1,len p)-cut p = {} by FINSEQ_6:def 4;
(1,m)-cut p = {} by A4,FINSEQ_6:def 4;
then ((m+1,len p)-cut p)^(1,m)-cut p = {} by A5,FINSEQ_1:34;
hence thesis by Th7,GRAPH_1:14;
end;
suppose
A6: 1 <= m & m < len p;
set n1 = m, n = m+1;
A7: 1 <= n by A6,NAT_1:13;
reconsider r1 = (1,n1)-cut p, r2 = (n, len p)-cut p as Path of G by Th5;
consider vs being FinSequence of the carrier of G such that
A8: vs is_vertex_seq_of p by GRAPH_2:33;
reconsider vs1 = (1,n)-cut vs, vs2 = (n, len vs)-cut vs as FinSequence of
the carrier of G;
A9: n <= len p by A6,NAT_1:13;
A10: len vs = len p +1 by A8;
A11: vs2 is_vertex_seq_of r2 by A7,A9,A8,GRAPH_2:42;
len p <= len p +1 by NAT_1:11;
then
A12: n <= len vs by A9,A10,XXREAL_0:2;
then
A13: n < len vs +1 by NAT_1:13;
len vs1 +1 = n +1 by A7,A12,FINSEQ_6:def 4;
then
A14: 1 < len vs1 by A6,NAT_1:13;
A15: vs1 is_vertex_seq_of r1 by A6,A8,GRAPH_2:42;
len vs <= len vs +1 by NAT_1:11;
then n <= len vs +1 by A12,XXREAL_0:2;
then len vs2 +n = len vs +1 by A7,Lm1;
then 1+n <= len vs2 +n by A13,NAT_1:13;
then
A16: 1 <= len vs2 by XREAL_1:6;
reconsider vs9 = vs2^'vs1 as FinSequence of the carrier of G;
set r = r2 ^ r1;
A17: vs.len vs = vs.1 by A8,MSSCYC_1:6;
A18: vs1.1 = vs.1 & vs2.len vs2 = vs.len vs by A7,A12,FINSEQ_6:138;
then reconsider r as Chain of G by A17,A15,A11,GRAPH_2:43;
A19: vs9 is_vertex_seq_of r by A17,A15,A11,A18,GRAPH_2:44;
p = r1 ^ r2 by A6,FINSEQ_6:135;
then rng r1 misses rng r2 by FINSEQ_3:91;
then reconsider r as Path of G by A17,A15,A11,A18,Th6;
vs1.len vs1 = vs.n & vs2.1 = vs.n by A7,A12,FINSEQ_6:138;
then vs9.1 = vs1.len vs1 by A16,FINSEQ_6:140
.= vs9.len vs9 by A14,FINSEQ_6:142;
then r is cyclic Path of G by A19,MSSCYC_1:def 2;
hence thesis;
end;
end;
theorem Th9:
m+1 in dom p implies len (((m+1,len p)-cut p)^(1,m)-cut p) = len
p & rng (((m+1,len p)-cut p)^(1,m)-cut p) = rng p & (((m+1,len p)-cut p)^(1,m)
-cut p).1 = p.(m+1)
proof
set r2 = (m+1,len p)-cut p;
set r1 = (1,m)-cut p;
set r = r2^r1;
set n = m+1;
assume
A1: m+1 in dom p;
then
A2: m+1 <= len p by FINSEQ_3:25;
then
A3: n < len p +1 by NAT_1:13;
m <= m+1 by NAT_1:11;
then
A4: p = r1 ^ r2 by A2,FINSEQ_6:135,XXREAL_0:2;
thus len r = len r1 + len r2 by FINSEQ_1:22
.= len p by A4,FINSEQ_1:22;
thus rng r = rng r1 \/ rng r2 by FINSEQ_1:31
.= rng p by A4,FINSEQ_1:31;
A5: 1 <= m+1 by A1,FINSEQ_3:25;
then len r2 +n = len p +1 by A2,FINSEQ_6:def 4;
then 1+n <= len r2 +n by A3,NAT_1:13;
then
A6: 1 <= len r2 by XREAL_1:6;
then 1 in dom r2 by FINSEQ_3:25;
hence r.1 = r2.(0+1) by FINSEQ_1:def 7
.= p.(n+0) by A5,A2,A6,FINSEQ_6:def 4
.= p.n;
end;
theorem Th10:
for p being cyclic Path of G st n in dom p ex p9 being cyclic
Path of G st p9.1 = p.n & len p9 = len p & rng p9 = rng p
proof
let p be cyclic Path of G;
assume
A1: n in dom p;
then
A2: 1 <= n by FINSEQ_3:25;
per cases by A2,XXREAL_0:1;
suppose
A3: n = 1;
take p;
thus thesis by A3;
end;
suppose
1 < n;
then 1+1 <= n by NAT_1:13;
then consider n1 being Nat such that
1<=n1 and
n1<n and
A4: n=n1+1 by FINSEQ_6:127;
reconsider r = ((n, len p)-cutp)^((1,n1)-cut p) as cyclic Path of G by A4
,Th8;
take r;
thus thesis by A1,A4,Th9;
end;
end;
theorem Th11: :: see MSSCYC_1:4
for s, t being Vertex of G st s = (the Source of G).e & t = (the
Target of G).e holds <*t, s*> is_vertex_seq_of <*e*>
proof
let s, t be Element of the carrier of G;
assume
A1: s = (the Source of G).e & t = (the Target of G).e;
set c = <*e*>;
set vs = <*t, s*>;
A2: vs/.(1+1) = s by FINSEQ_4:17;
A3: len c = 1 by FINSEQ_1:39;
hence len vs = len c + 1 by FINSEQ_1:44;
let n be Nat;
assume 1<=n & n<=len c;
then
A4: n = 1 by A3,XXREAL_0:1;
c.1 = e & vs/.1 = t by FINSEQ_4:17;
hence thesis by A1,A4,A2;
end;
theorem Th12:
e in the carrier' of G & vs is_vertex_seq_of c & vs.len vs = (
the Source of G).e implies c^<*e*> is Chain of G & ex vs9 being FinSequence of
the carrier of G st vs9 = vs^'<*(the Source of G).e, (the Target of G).e*> &
vs9 is_vertex_seq_of c^<*e*> & vs9.1 = vs.1 & vs9.len vs9 = (the Target of G).e
proof
assume that
A1: e in the carrier' of G and
A2: vs is_vertex_seq_of c;
reconsider ec = <*e*> as Chain of G by A1,MSSCYC_1:5;
reconsider s = (the Source of G).e, t = (the Target of G).e as Vertex of G
by A1,FUNCT_2:5;
reconsider vse = <*s, t*> as FinSequence of the carrier of G;
A3: vse is_vertex_seq_of ec & vse.1 = s by MSSCYC_1:4;
assume
A4: vs.len vs = (the Source of G).e;
hence c^<*e*> is Chain of G by A2,A3,GRAPH_2:43;
reconsider ce = c^ec as Chain of G by A2,A4,A3,GRAPH_2:43;
take vs9 = vs^'vse;
thus vs9 = vs^'<*(the Source of G).e, (the Target of G).e*>;
vs9 is_vertex_seq_of ce by A2,A4,A3,GRAPH_2:44;
hence vs9 is_vertex_seq_of c^<*e*>;
len vs = len c +1 by A2;
then 1 <= len vs by NAT_1:11;
hence vs9.1 = vs.1 by FINSEQ_6:140;
A5: len vse = 2 by FINSEQ_1:44;
then vse.len vse = t;
hence thesis by A5,FINSEQ_6:142;
end;
theorem Th13:
e in the carrier' of G & vs is_vertex_seq_of c & vs.len vs = (
the Target of G).e implies c^<*e*> is Chain of G & ex vs9 being FinSequence of
the carrier of G st vs9 = vs^'<*(the Target of G).e, (the Source of G).e*> &
vs9 is_vertex_seq_of c^<*e*> & vs9.1 = vs.1 & vs9.len vs9 = (the Source of G).e
proof
assume that
A1: e in the carrier' of G and
A2: vs is_vertex_seq_of c;
reconsider ec = <*e*> as Chain of G by A1,MSSCYC_1:5;
reconsider s = (the Source of G).e, t = (the Target of G).e as Vertex of G
by A1,FUNCT_2:5;
assume
A3: vs.len vs = (the Target of G).e;
reconsider vse = <*t, s*> as FinSequence of the carrier of G;
A4: vse is_vertex_seq_of ec & vse.1 = t by Th11;
hence c^<*e*> is Chain of G by A2,A3,GRAPH_2:43;
reconsider ce = c^ec as Chain of G by A2,A3,A4,GRAPH_2:43;
take vs9 = vs^'vse;
thus vs9 = vs^'<*(the Target of G).e, (the Source of G).e*>;
vs9 is_vertex_seq_of ce by A2,A3,A4,GRAPH_2:44;
hence vs9 is_vertex_seq_of c^<*e*>;
len vs = len c +1 by A2;
then 1 <= len vs by NAT_1:11;
hence vs9.1 = vs.1 by FINSEQ_6:140;
A5: len vse = 2 by FINSEQ_1:44;
then vse.len vse = s;
hence thesis by A5,FINSEQ_6:142;
end;
Lm3: for G being Graph, c being Chain of G, vs being FinSequence of the
carrier of G st vs is_vertex_seq_of c for n being Nat st 1 <= n & n <= len c
holds 1 <= n & n <= len vs & 1 <= n+1 & n+1 <= len vs & (vs.n = (the Target of
G).(c.n) & vs.(n+1) = (the Source of G).(c.n) or vs.n = (the Source of G).(c.n)
& vs.(n+1) = (the Target of G).(c.n))
proof
let G be Graph, c be Chain of G, vs be FinSequence of the carrier of G;
assume
A1: vs is_vertex_seq_of c;
then
A2: len vs = len c +1;
let n be Nat such that
A3: 1 <= n and
A4: n <= len c;
thus 1 <= n by A3;
len c <= len c + 1 by NAT_1:11;
hence
A5: n <= len vs by A4,A2,XXREAL_0:2;
thus 1 <= n+1 by NAT_1:11;
thus
A6: n+1 <= len vs by A4,A2,XREAL_1:6;
reconsider n as Element of NAT by ORDINAL1:def 12;
A7: vs.n = vs/.n by A3,A5,FINSEQ_4:15;
A8: vs.(n+1) = vs/.(n+1) by A6,FINSEQ_4:15,NAT_1:11;
c.n joins vs/.n, vs/.(n+1) by A1,A3,A4;
hence thesis by A7,A8;
end;
theorem
vs is_vertex_seq_of c implies for n being Element of NAT st n in dom c
holds (vs.n = (the Target of G).(c.n) & vs.(n+1) = (the Source of G).(c.n) or
vs.n = (the Source of G).(c.n) & vs.(n+1) = (the Target of G).(c.n))
proof
assume
A1: vs is_vertex_seq_of c;
let n be Element of NAT;
assume n in dom c;
then 1 <= n & n <= len c by FINSEQ_3:25;
hence thesis by A1,Lm3;
end;
theorem Th15:
vs is_vertex_seq_of c & e in rng c implies (the Target of G).e
in rng vs & (the Source of G).e in rng vs
proof
assume that
A1: vs is_vertex_seq_of c and
A2: e in rng c;
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then
A3: rng c c= the carrier' of G by FINSEQ_1:def 4;
then reconsider e9 = e as Element of the carrier' of G by A2;
reconsider t = (the Target of G).e, s = (the Source of G).e as Vertex of G
by A2,A3,FUNCT_2:5;
e9 in rng c by A2;
then t in G-VSet rng c & s in G-VSet rng c;
hence thesis by A1,A2,GRAPH_2:31,RELAT_1:38;
end;
definition
let G be Graph, X be set;
redefine func G-VSet X -> Subset of the carrier of G; :: redefines -VSet (GRAPH_2, definition)
coherence
proof
defpred P[set] means ex e being Element of the carrier' of G st e in X & (
$1 = (the Source of G).e or $1 = (the Target of G).e);
{ v where v is Vertex of G : P[v] } is Subset of the carrier of G from
DOMAIN_1:sch 7;
hence thesis;
end;
end;
theorem Th16:
G-VSet {} = {}
proof
assume not thesis;
then consider x being object such that
A1: x in G-VSet {} by XBOOLE_0:def 1;
ex v being Vertex of G st x = v & ex e being Element of the carrier' of G
st e in {} & (v = (the Source of G).e or v = (the Target of G ).e) by A1;
hence contradiction;
end;
theorem Th17:
e in the carrier' of G & e in X implies G-VSet X is non empty
proof
assume that
A1: e in the carrier' of G and
A2: e in X;
reconsider v = (the Source of G).e as Vertex of G by A1,FUNCT_2:5;
v in G-VSet X by A1,A2;
hence thesis;
end;
theorem Th18:
G is connected iff for v1, v2 st v1 <> v2 ex c, vs st c is non
empty & vs is_vertex_seq_of c & vs.1 = v1 & vs.len vs = v2
proof
set E = the carrier' of G;
set S = the Source of G;
set T = the Target of G;
thus G is connected implies for v1, v2 being Vertex of G st v1 <> v2 ex c
being Chain of G, vs being FinSequence of the carrier of G st c is non empty &
vs is_vertex_seq_of c & vs.1 = v1 & vs.len vs = v2
proof
reconsider V = the carrier of G as non empty set;
assume
A1: G is connected;
let v1, v2 be Vertex of G;
set V1 = { v where v is Element of V : v = v1 or ex c being Chain of G, vs
being FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c
& vs.1 = v1 & vs.len vs = v };
set V2 = (V) \ V1;
v1 in V1;
then reconsider V1 as non empty set;
assume
A2: v1 <> v2;
assume
A3: not thesis;
now
assume v2 in V1;
then
ex v being Vertex of G st v = v2 &( v = v1 or ex c being Chain of G,
vs being FinSequence of the carrier of G st c is non empty & vs
is_vertex_seq_of c & vs.1 = v1 & vs.len vs = v);
hence contradiction by A2,A3;
end;
then reconsider V2 as non empty set by XBOOLE_0:def 5;
defpred P[set] means $1 = v1 or ex c being Chain of G, vs being
FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & vs.
1 = v1 & vs.len vs = $1;
A4: { v where v is Element of V : P[v] } is Subset of V from DOMAIN_1:sch
7;
defpred P[object] means
(the Source of G).$1 in V1 & (the Target of G).$1 in
V1;
consider E1 being set such that
A5: for e being object holds e in E1 iff e in E & P[e] from XBOOLE_0:sch
1;
A6: dom S = E by FUNCT_2:def 1;
set E2 = (E) \ E1;
A7: dom (S|E2) = dom S /\ E2 by RELAT_1:61
.= E2 by A6,XBOOLE_1:28;
A8: rng S c= V by RELAT_1:def 19;
rng (S|E2) c= V2
proof
let v be object;
assume v in rng (S|E2);
then consider e being object such that
A9: e in dom (S|E2) and
A10: (S|E2).e = v by FUNCT_1:def 3;
reconsider e as Element of the carrier' of G by A7,A9;
A11: (S|E2).e = S.e by A9,FUNCT_1:47;
A12: not e in E1 by A7,A9,XBOOLE_0:def 5;
per cases by A5,A12;
suppose
not e in E;
hence thesis by A7,A9;
end;
suppose
A13: not (the Source of G).e in V1;
S.e in V by A7,A9,FUNCT_2:5;
hence thesis by A10,A11,A13,XBOOLE_0:def 5;
end;
suppose
A14: not (the Target of G).e in V1;
reconsider Te = T.e as Vertex of G by A7,A9,FUNCT_2:5;
v in rng (S|E2) & rng (S|E2) c= rng S by A9,A10,FUNCT_1:def 3
,RELAT_1:70;
then
A15: v in rng S;
assume not v in V2;
then v in V1 by A8,A15,XBOOLE_0:def 5;
then consider v9 being Vertex of G such that
A16: v9 = v and
A17: v9 = v1 or ex c being Chain of G, vs being FinSequence of the
carrier of G st c is non empty & vs is_vertex_seq_of c & vs.1 = v1 & vs.len vs
= v9;
thus contradiction
proof
per cases by A17;
suppose
A18: v9 = v1;
reconsider ec = <*e*> as Chain of G by A7,A9,MSSCYC_1:5;
reconsider vs = <*v1, Te*> as FinSequence of the carrier of G;
len vs = 2 by FINSEQ_1:44;
then
A19: vs.1 = v1 & vs.len vs = Te;
vs is_vertex_seq_of ec by A10,A11,A16,A18,MSSCYC_1:4;
hence contradiction by A14,A19;
end;
suppose
ex c being Chain of G, vs being FinSequence of the
carrier of G st c is non empty & vs is_vertex_seq_of c & vs.1 = v1 & vs.len vs
= v9;
then consider
c being Chain of G, vs being FinSequence of the carrier
of G such that
c is non empty and
A20: vs is_vertex_seq_of c and
A21: vs.1 = v1 and
A22: vs.len vs = v9;
reconsider c9 = c^<*e*> as Chain of G by A7,A9,A10,A11,A16,A20,A22
,Th12;
ex vs9 being FinSequence of the carrier of G st vs9 = vs^'<*S
.e,T.e*> & vs9 is_vertex_seq_of c9 & vs9.1 = vs.1 & vs9.len vs9 = Te by A7,A9
,A10,A11,A16,A20,A22,Th12;
hence contradiction by A14,A21;
end;
end;
end;
end;
then reconsider S2 = S|E2 as Function of E2, V2 by A7,FUNCT_2:def 1
,RELSET_1:4;
A23: dom T = E by FUNCT_2:def 1;
A24: dom (T|E2) = dom T /\ E2 by RELAT_1:61
.= E2 by A23,XBOOLE_1:28;
A25: rng T c= V by RELAT_1:def 19;
rng (T|E2) c= V2
proof
let v be object;
assume v in rng (T|E2);
then consider e being object such that
A26: e in dom (T|E2) and
A27: (T|E2).e = v by FUNCT_1:def 3;
reconsider e as Element of the carrier' of G by A24,A26;
A28: (T|E2).e = T.e by A26,FUNCT_1:47;
A29: not e in E1 by A24,A26,XBOOLE_0:def 5;
per cases by A5,A29;
suppose
not e in E;
hence thesis by A24,A26;
end;
suppose
A30: not (the Target of G).e in V1;
T.e in V by A24,A26,FUNCT_2:5;
hence thesis by A27,A28,A30,XBOOLE_0:def 5;
end;
suppose
A31: not (the Source of G).e in V1;
reconsider Se = S.e as Vertex of G by A24,A26,FUNCT_2:5;
v in rng (T|E2) & rng (T|E2) c= rng T by A26,A27,FUNCT_1:def 3
,RELAT_1:70;
then
A32: v in rng T;
assume not v in V2;
then v in V1 by A25,A32,XBOOLE_0:def 5;
then consider v9 being Vertex of G such that
A33: v9 = v and
A34: v9 = v1 or ex c being Chain of G, vs being FinSequence of the
carrier of G st c is non empty & vs is_vertex_seq_of c & vs.1 = v1 & vs.len vs
= v9;
thus contradiction
proof
per cases by A34;
suppose
A35: v9 = v1;
reconsider ec = <*e*> as Chain of G by A24,A26,MSSCYC_1:5;
reconsider vs = <*v1, Se*> as FinSequence of the carrier of G;
len vs = 2 by FINSEQ_1:44;
then
A36: vs.1 = v1 & vs.len vs = Se;
vs is_vertex_seq_of ec by A27,A28,A33,A35,Th11;
hence contradiction by A31,A36;
end;
suppose
ex c being Chain of G, vs being FinSequence of the
carrier of G st c is non empty & vs is_vertex_seq_of c & vs.1 = v1 & vs.len vs
= v9;
then consider
c being Chain of G, vs being FinSequence of the carrier
of G such that
c is non empty and
A37: vs is_vertex_seq_of c and
A38: vs.1 = v1 and
A39: vs.len vs = v9;
reconsider c9 = c^<*e*> as Chain of G by A24,A26,A27,A28,A33,A37
,A39,Th13;
ex vs9 being FinSequence of the carrier of G st vs9 = vs^'<*T
.e,S.e*> & vs9 is_vertex_seq_of c9 & vs9.1 = vs.1 & vs9.len vs9 = Se by A24,A26
,A27,A28,A33,A37,A39,Th13;
hence contradiction by A31,A38;
end;
end;
end;
end;
then reconsider T2 = T|E2 as Function of E2, V2 by A24,FUNCT_2:def 1
,RELSET_1:4;
A40: E1 c= E
by A5;
A41: dom (T|E1) = dom T /\ E1 by RELAT_1:61
.= E /\ E1 by FUNCT_2:def 1
.= E1 by A40,XBOOLE_1:28;
rng (T|E1) c= V1
proof
let v be object;
assume v in rng (T|E1);
then consider e being object such that
A42: e in dom (T|E1) and
A43: (T|E1).e = v by FUNCT_1:def 3;
(T|E1).e = T.e by A42,FUNCT_1:47;
hence thesis by A5,A41,A42,A43;
end;
then reconsider T1 = T|E1 as Function of E1, V1 by A41,FUNCT_2:def 1
,RELSET_1:4;
A44: dom (S|E1) = dom S /\ E1 by RELAT_1:61
.= E /\ E1 by FUNCT_2:def 1
.= E1 by A40,XBOOLE_1:28;
rng (S|E1) c= V1
proof
let v be object;
assume v in rng (S|E1);
then consider e being object such that
A45: e in dom (S|E1) and
A46: (S|E1).e = v by FUNCT_1:def 3;
(S|E1).e = S.e by A45,FUNCT_1:47;
hence thesis by A5,A44,A45,A46;
end;
then reconsider S1 = S|E1 as Function of E1, V1 by A44,FUNCT_2:def 1
,RELSET_1:4;
reconsider G1 = MultiGraphStruct (# V1, E1, S1, T1 #), G2 =
MultiGraphStruct (# V2, E2, S2, T2 #) as Graph;
A47: G is_sum_of G1, G2
proof
reconsider MG = the MultiGraphStruct of G as strict Graph;
thus
A48: (the Target of G1) tolerates (the Target of G2)
proof
let x be object;
assume
A49: x in dom (the Target of G1) /\ dom (the Target of G2);
then x in dom (the Target of G2) by XBOOLE_0:def 4;
then
A50: x in E2 by FUNCT_2:def 1;
x in dom (the Target of G1) by A49,XBOOLE_0:def 4;
then x in E1 by FUNCT_2:def 1;
hence thesis by A50,XBOOLE_0:def 5;
end;
thus
A51: (the Source of G1) tolerates (the Source of G2)
proof
let x be object;
assume
A52: x in dom (the Source of G1) /\ dom (the Source of G2);
then x in dom (the Source of G2) by XBOOLE_0:def 4;
then
A53: x in E2 by FUNCT_2:def 1;
x in dom (the Source of G1) by A52,XBOOLE_0:def 4;
then x in E1 by FUNCT_2:def 1;
hence thesis by A53,XBOOLE_0:def 5;
end;
A54: ( for v be set st v in the carrier' of G1 holds (the Source of MG).
v = (the Source of G1).v & (the Target of MG).v = (the Target of G1).v)& for v
be set st v in the carrier' of G2 holds (the Source of MG).v = (the Source of
G2).v & (the Target of MG).v = (the Target of G2).v by FUNCT_1:49;
the carrier of MG = (the carrier of G1) \/ (the carrier of G2) &
the carrier' of MG = (the carrier' of G1) \/ (the carrier' of G2) by A4,A40,
XBOOLE_1:45;
hence thesis by A48,A51,A54,GRAPH_1:def 5;
end;
V1 misses V2 by XBOOLE_1:79;
hence contradiction by A1,A47;
end;
assume
A55: for v1, v2 being Vertex of G st v1 <> v2 ex c being Chain of G, vs
being FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c
& vs.1 = v1 & vs.len vs = v2;
thus G is connected
proof
given G1, G2 being Graph such that
A56: (the carrier of G1) misses (the carrier of G2) and
A57: G is_sum_of G1, G2;
set v2 = the Vertex of G2;
set v1 = the Vertex of G1;
set V2 = the carrier of G2;
set V1 = the carrier of G1;
set T2 = the Target of G2;
set T1 = the Target of G1;
set S2 = the Source of G2;
set S1 = the Source of G1;
set E1 = the carrier' of G1;
A58: the MultiGraphStruct of G = G1 \/ G2 by A57;
A59: T1 tolerates T2 & S1 tolerates S2 by A57;
then
A60: E = E1 \/ the carrier' of G2 by A58,GRAPH_1:def 5;
the carrier of the MultiGraphStruct of G = V1 \/ V2 by A59,A58,
GRAPH_1:def 5;
then reconsider v19 = v1, v29 = v2 as Vertex of G by XBOOLE_0:def 3;
A61: (the carrier of G1) /\ (the carrier of G2) = {} by A56;
then v1 <> v2 by XBOOLE_0:def 4;
then consider
c being Chain of G, vs being FinSequence of the carrier of G such
that
c is non empty and
A62: vs is_vertex_seq_of c and
A63: vs.1 = v19 and
A64: vs.len vs = v29 by A55;
defpred P[Nat] means $1 in dom vs & vs.$1 is Vertex of G2;
A65: len vs = len c +1 by A62;
c is FinSequence of E by MSSCYC_1:def 1;
then
A66: rng c c= E by FINSEQ_1:def 4;
1 <= len c+1 by NAT_1:11;
then len vs in dom vs by A65,FINSEQ_3:25;
then
A67: ex k being Nat st P[k] by A64;
consider k being Nat such that
A68: P[k] and
A69: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A67);
A70: 1 <= k by A68,FINSEQ_3:25;
k <> 1 by A61,A63,A68,XBOOLE_0:def 4;
then 1 < k by A70,XXREAL_0:1;
then 1+1 <= k by NAT_1:13;
then consider i being Nat such that
A71: 1<=i and
A72: i<k and
A73: k=i+1 by FINSEQ_6:127;
set e = c.i;
A74: k <= len vs by A68,FINSEQ_3:25;
then
A75: i <= len c by A65,A73,XREAL_1:6;
then i in dom c by A71,FINSEQ_3:25;
then
A76: e in rng c by FUNCT_1:def 3;
i <= len vs by A72,A74,XXREAL_0:2;
then
A77: i in dom vs by A71,FINSEQ_3:25;
per cases by A60,A66,A76,XBOOLE_0:def 3;
suppose
A78: e in E1;
then
A79: T1.e in V1 by FUNCT_2:5;
A80: S1.e in V1 by A78,FUNCT_2:5;
thus contradiction
proof
per cases by A62,A71,A75,Lm3;
suppose
vs.i = T.e & vs.(i+1) = S.e;
then vs.k in V1 by A59,A58,A73,A78,A80,GRAPH_1:def 5;
hence contradiction by A61,A68,XBOOLE_0:def 4;
end;
suppose
vs.i = S.e & vs.(i+1) = T.e;
then vs.k in V1 by A59,A58,A73,A78,A79,GRAPH_1:def 5;
hence contradiction by A61,A68,XBOOLE_0:def 4;
end;
end;
end;
suppose
A81: e in the carrier' of G2;
then
A82: T2.e in V2 by FUNCT_2:5;
A83: S2.e in V2 by A81,FUNCT_2:5;
thus contradiction
proof
per cases by A62,A71,A75,Lm3;
suppose
vs.i = T.e & vs.(i+1) = S.e;
then vs.i in V2 by A59,A58,A81,A82,GRAPH_1:def 5;
hence contradiction by A69,A72,A77;
end;
suppose
vs.i = S.e & vs.(i+1) = T.e;
then vs.i in V2 by A59,A58,A81,A83,GRAPH_1:def 5;
hence contradiction by A69,A72,A77;
end;
end;
end;
end;
end;
theorem Th19:
for G being connected Graph, X being set, v being Vertex of G st
X meets the carrier' of G & not v in G-VSet X ex v9 being Vertex of G, e being
Element of the carrier' of G st v9 in G-VSet X & not e in X & (v9 = (the Target
of G).e or v9 = (the Source of G).e)
proof
let G be connected Graph, X be set, v be Vertex of G;
assume that
A1: X meets the carrier' of G and
A2: not v in G-VSet X;
ex e being object st e in X & e in the carrier' of G by A1,XBOOLE_0:3;
then G-VSet X is non empty by Th17;
then consider vv being object such that
A3: vv in G-VSet X;
reconsider vv as Vertex of G by A3;
consider c being Chain of G, vs being FinSequence of the carrier of G such
that
A4: c is non empty and
A5: vs is_vertex_seq_of c and
A6: vs.1 = vv and
A7: vs.len vs = v by A2,A3,Th18;
defpred P[Nat] means 1 <= $1 & $1 <= len c & not vs.($1+1) in G-VSet X;
A8: len vs = len c +1 by A5;
1+0 <= len c by A4,NAT_1:13;
then
A9: ex n being Nat st P[n] by A2,A7,A8;
consider k being Nat such that
A10: P[k] and
A11: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A9);
len c <= len c +1 by NAT_1:11;
then k <= len vs by A8,A10,XXREAL_0:2;
then k in dom vs by A10,FINSEQ_3:25;
then reconsider v9 = vs.k as Vertex of G by FINSEQ_2:11;
reconsider c as FinSequence of the carrier' of G by MSSCYC_1:def 1;
A12: rng c c= the carrier' of G by FINSEQ_1:def 4;
k in dom c by A10,FINSEQ_3:25;
then c.k in rng c by FUNCT_1:def 3;
then reconsider e = c.k as Element of the carrier' of G by A12;
take v9;
take e;
hereby
per cases by A10,XXREAL_0:1;
suppose
k = 1;
hence v9 in G-VSet X by A3,A6;
end;
suppose
A13: 1 < k;
assume
A14: not v9 in G-VSet X;
consider p being Element of NAT such that
A15: k=1+p and
A16: 1 <= p by A13,FINSEQ_4:84;
p <= k by A15,NAT_1:11;
then p <= len c by A10,XXREAL_0:2;
then k <= p by A11,A15,A16,A14;
hence contradiction by A15,NAT_1:13;
end;
end;
hereby
1 <= k+1 & k+1 <= len vs by A8,A10,NAT_1:11,XREAL_1:6;
then k+1 in dom vs by FINSEQ_3:25;
then reconsider v99 = vs.(k+1) as Vertex of G by FINSEQ_2:11;
assume
A17: e in X;
v99 = (the Target of G).e or v99 = (the Source of G).e by A5,A10,Lm3;
hence contradiction by A10,A17;
end;
thus thesis by A5,A10,Lm3;
end;
begin :: Degree of a vertex
definition
let G be Graph, v be Vertex of G, X be set;
func Edges_In(v, X) -> Subset of the carrier' of G means
:Def1:
for e being
set holds e in it iff e in the carrier' of G & e in X & (the Target of G).e = v
;
existence
proof
defpred P[object] means $1 in X & (the Target of G).$1 = v;
consider IT being set such that
A1: for x being object holds x in IT iff x in the carrier' of G & P[x]
from XBOOLE_0:sch 1;
take IT;
for x being object st x in IT holds x in the carrier' of G by A1;
hence IT is Subset of the carrier' of G by TARSKI:def 3;
thus thesis by A1;
end;
uniqueness
proof
let it1, it2 be Subset of the carrier' of G such that
A2: for e being set holds e in it1 iff e in the carrier' of G & e in X
& (the Target of G).e = v and
A3: for e being set holds e in it2 iff e in the carrier' of G & e in X
& (the Target of G).e = v;
now
let e be object;
e in it1 iff e in the carrier' of G & e in X & (the Target of G).e =
v by A2;
hence e in it1 iff e in it2 by A3;
end;
hence thesis by TARSKI:2;
end;
func Edges_Out(v, X) -> Subset of the carrier' of G means
:Def2:
for e being
set holds e in it iff e in the carrier' of G & e in X & (the Source of G).e = v
;
existence
proof
defpred P[object] means $1 in X & (the Source of G).$1 = v;
consider IT being set such that
A4: for x being object holds x in IT iff x in the carrier' of G & P[x]
from XBOOLE_0:sch 1;
take IT;
for x being object st x in IT holds x in the carrier' of G by A4;
hence IT is Subset of the carrier' of G by TARSKI:def 3;
thus thesis by A4;
end;
uniqueness
proof
let it1, it2 be Subset of the carrier' of G such that
A5: for e being set holds e in it1 iff e in the carrier' of G & e in X
& (the Source of G).e = v and
A6: for e being set holds e in it2 iff e in the carrier' of G & e in
X & (the Source of G).e = v;
now
let e be object;
e in it1 iff e in the carrier' of G & e in X & (the Source of G).e
= v by A5;
hence e in it1 iff e in it2 by A6;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let G be Graph, v be Vertex of G, X be set;
func Edges_At(v, X) -> Subset of the carrier' of G equals
Edges_In(v, X) \/
Edges_Out(v, X);
correctness;
end;
registration
let G be finite Graph, v be Vertex of G, X be set;
cluster Edges_In(v, X) -> finite;
correctness
proof
the carrier' of G is finite by GRAPH_1:def 11;
hence thesis;
end;
cluster Edges_Out(v, X) -> finite;
correctness
proof
the carrier' of G is finite by GRAPH_1:def 11;
hence thesis;
end;
cluster Edges_At(v, X) -> finite;
correctness;
end;
registration
let G be Graph, v be Vertex of G, X be empty set;
cluster Edges_In(v, X) -> empty;
correctness
by Def1;
cluster Edges_Out(v, X) -> empty;
correctness
by Def2;
cluster Edges_At(v, X) -> empty;
correctness;
end;
definition
let G be Graph, v be Vertex of G;
func Edges_In v -> Subset of the carrier' of G equals
Edges_In(v, the
carrier' of G);
correctness;
func Edges_Out v -> Subset of the carrier' of G equals
Edges_Out(v, the
carrier' of G);
correctness;
end;
theorem Th20:
Edges_In(v, X) c= Edges_In v
proof
let e be object;
assume
A1: e in Edges_In(v, X);
then (the Target of G).e = v by Def1;
hence thesis by A1,Def1;
end;
theorem Th21:
Edges_Out(v, X) c= Edges_Out v
proof
let e be object;
assume
A1: e in Edges_Out(v, X);
then (the Source of G).e = v by Def2;
hence thesis by A1,Def2;
end;
registration
let G be finite Graph, v be Vertex of G;
cluster Edges_In v -> finite;
correctness;
cluster Edges_Out v -> finite;
correctness;
end;
reserve G for finite Graph,
v for Vertex of G,
c for Chain of G,
vs for FinSequence of the carrier of G,
X1, X2 for set;
theorem Th22:
card Edges_In v = EdgesIn v
proof
consider X being finite set such that
A1: for z being set holds z in X iff z in the carrier' of G & (the
Target of G).z = v and
A2: EdgesIn v = card(X) by GRAPH_1:def 21;
now
let e be object;
e in Edges_In (v, the carrier' of G) iff e in the carrier' of G & (the
Target of G).e = v by Def1;
hence e in Edges_In v iff e in X by A1;
end;
hence thesis by A2,TARSKI:2;
end;
theorem Th23:
card Edges_Out v = EdgesOut v
proof
consider X being finite set such that
A1: for z being set holds z in X iff z in the carrier' of G & (the
Source of G).z = v and
A2: EdgesOut v = card(X) by GRAPH_1:def 22;
now
let e be object;
e in Edges_Out (v, the carrier' of G) iff e in the carrier' of G & (
the Source of G).e = v by Def2;
hence e in Edges_Out v iff e in X by A1;
end;
hence thesis by A2,TARSKI:2;
end;
definition
let G be finite Graph, v be Vertex of G, X be set;
func Degree(v, X) -> Element of NAT equals
card Edges_In(v, X) + card
Edges_Out(v, X);
correctness;
end;
theorem Th24:
Degree v = Degree(v, the carrier' of G)
proof
thus Degree v = card Edges_In v + EdgesOut v by Th22
.= card Edges_In(v, the carrier' of G) + card Edges_Out v by Th23
.= Degree(v, the carrier' of G);
end;
theorem Th25:
Degree(v, X) <> 0 implies Edges_At(v, X) is non empty
proof
assume
A1: Degree(v, X) <> 0;
assume
A2: not thesis;
then Edges_In(v, X) = {};
hence contradiction by A1,A2;
end;
theorem Th26:
e in the carrier' of G & not e in X & (v = (the Target of G).e
or v = (the Source of G).e) implies Degree v <> Degree(v, X)
proof
set T = the Target of G, S = the Source of G, E = the carrier' of G;
assume that
A1: e in E and
A2: not e in X and
A3: v = T.e or v = S.e;
A4: Degree v = Degree(v, E) by Th24;
Edges_Out v = Edges_Out(v, E);
then
A5: Edges_Out(v, X) c= Edges_Out(v, E) by Th21;
Edges_In v = Edges_In(v, E);
then
A6: Edges_In(v, X) c= Edges_In(v, E) by Th20;
per cases by A3;
suppose
A7: v = T.e;
A8: not e in Edges_In(v, X) by A2,Def1;
e in Edges_In(v, E) by A1,A7,Def1;
then Edges_In(v, X) c< Edges_In(v, E) by A6,A8;
then card Edges_In(v, X) < card Edges_In(v, E) by CARD_2:48;
hence thesis by A4,A5,NAT_1:43,XREAL_1:8;
end;
suppose
A9: v = S.e;
A10: not e in Edges_Out(v, X) by A2,Def2;
e in Edges_Out(v, E) by A1,A9,Def2;
then Edges_Out(v, X) c< Edges_Out(v, E) by A5,A10;
then card Edges_Out(v, X) < card Edges_Out(v, E) by CARD_2:48;
hence thesis by A4,A6,NAT_1:43,XREAL_1:8;
end;
end;
theorem Th27:
X2 c= X1 implies card Edges_In(v, X1\X2) = card Edges_In(v, X1)
- card Edges_In(v, X2)
proof
assume
A1: X2 c= X1;
then
A2: X1 = X2 \/ (X1\X2) by XBOOLE_1:45;
now
let x be object;
hereby
assume
A3: x in Edges_In(v,X1);
then x in X1 by Def1;
then
A4: x in X2 or x in X1\X2 by A2,XBOOLE_0:def 3;
(the Target of G).x = v by A3,Def1;
then x in Edges_In(v,X2) or x in Edges_In(v, X1\X2) by A3,A4,Def1;
hence x in Edges_In(v,X2) \/ Edges_In(v, X1\X2) by XBOOLE_0:def 3;
end;
assume
A5: x in Edges_In(v,X2) \/ Edges_In(v, X1\X2);
then
A6: x in Edges_In(v,X2) or x in Edges_In(v, X1\X2) by XBOOLE_0:def 3;
then
A7: x in X2 or x in X1\X2 by Def1;
(the Target of G).x = v by A6,Def1;
hence x in Edges_In(v,X1) by A1,A5,A7,Def1;
end;
then
A8: Edges_In(v,X1) = Edges_In(v,X2) \/ Edges_In(v, X1\X2) by TARSKI:2;
Edges_In(v, X2) misses Edges_In(v, X1\X2)
proof
assume not thesis;
then consider x being object such that
A9: x in Edges_In(v, X2) /\ Edges_In(v, X1\X2) by XBOOLE_0:4;
x in Edges_In(v, X1\X2) by A9,XBOOLE_0:def 4;
then
A10: x in X1\X2 by Def1;
x in Edges_In(v, X2) by A9,XBOOLE_0:def 4;
then x in X2 by Def1;
hence contradiction by A10,XBOOLE_0:def 5;
end;
then card Edges_In(v,X1) = card Edges_In(v,X2) + card Edges_In(v, X1\X2) by
A8,CARD_2:40;
hence thesis;
end;
theorem Th28:
X2 c= X1 implies card Edges_Out(v, X1\X2) = card Edges_Out(v, X1
) - card Edges_Out(v, X2)
proof
assume
A1: X2 c= X1;
then
A2: X1 = X2 \/ (X1\X2) by XBOOLE_1:45;
now
let x be object;
hereby
assume
A3: x in Edges_Out(v,X1);
then x in X1 by Def2;
then
A4: x in X2 or x in X1\X2 by A2,XBOOLE_0:def 3;
(the Source of G).x = v by A3,Def2;
then x in Edges_Out(v,X2) or x in Edges_Out(v, X1\X2) by A3,A4,Def2;
hence x in Edges_Out(v,X2) \/ Edges_Out(v, X1\X2) by XBOOLE_0:def 3;
end;
assume
A5: x in Edges_Out(v,X2) \/ Edges_Out(v, X1\X2);
then
A6: x in Edges_Out(v,X2) or x in Edges_Out(v, X1\X2) by XBOOLE_0:def 3;
then
A7: x in X2 or x in X1\X2 by Def2;
(the Source of G).x = v by A6,Def2;
hence x in Edges_Out(v,X1) by A1,A5,A7,Def2;
end;
then
A8: Edges_Out(v,X1) = Edges_Out(v,X2) \/ Edges_Out(v, X1\X2) by TARSKI:2;
Edges_Out(v, X2) misses Edges_Out(v, X1\X2)
proof
assume not thesis;
then consider x being object such that
A9: x in Edges_Out(v, X2) /\ Edges_Out(v, X1\X2) by XBOOLE_0:4;
x in Edges_Out(v, X1\X2) by A9,XBOOLE_0:def 4;
then
A10: x in X1\X2 by Def2;
x in Edges_Out(v, X2) by A9,XBOOLE_0:def 4;
then x in X2 by Def2;
hence contradiction by A10,XBOOLE_0:def 5;
end;
then card Edges_Out(v,X1) = card Edges_Out(v,X2) + card Edges_Out(v, X1\X2)
by A8,CARD_2:40;
hence thesis;
end;
theorem Th29:
X2 c= X1 implies Degree(v, X1 \ X2) = Degree(v, X1) - Degree(v, X2)
proof
assume X2 c= X1;
then
card Edges_In(v, X1\X2) = card Edges_In(v, X1) - card Edges_In(v, X2) &
card Edges_Out(v, X1\X2) = card Edges_Out(v, X1) - card Edges_Out(v, X2) by
Th27,Th28;
hence thesis;
end;
theorem Th30:
Edges_In(v, X) = Edges_In(v, X/\the carrier' of G) & Edges_Out(v
, X) = Edges_Out(v, X/\the carrier' of G)
proof
set E = the carrier' of G;
now
let x be object;
hereby
assume
A1: x in Edges_In(v, X);
then x in X by Def1;
then
A2: x in X/\E by A1,XBOOLE_0:def 4;
(the Target of G).x = v by A1,Def1;
hence x in Edges_In(v, X/\E) by A1,A2,Def1;
end;
assume
A3: x in Edges_In(v, X/\E);
then x in X/\E by Def1;
then
A4: x in X by XBOOLE_0:def 4;
(the Target of G).x = v by A3,Def1;
hence x in Edges_In(v, X) by A3,A4,Def1;
end;
hence Edges_In(v, X) = Edges_In(v, X/\the carrier' of G) by TARSKI:2;
now
let x be object;
hereby
assume
A5: x in Edges_Out(v, X);
then x in X by Def2;
then
A6: x in X/\E by A5,XBOOLE_0:def 4;
(the Source of G).x = v by A5,Def2;
hence x in Edges_Out(v, X/\E) by A5,A6,Def2;
end;
assume
A7: x in Edges_Out(v, X/\E);
then x in X/\E by Def2;
then
A8: x in X by XBOOLE_0:def 4;
(the Source of G).x = v by A7,Def2;
hence x in Edges_Out(v, X) by A7,A8,Def2;
end;
hence thesis by TARSKI:2;
end;
theorem Th31:
Degree(v, X) = Degree(v, X/\the carrier' of G)
proof
set E = the carrier' of G;
thus Degree(v, X) = card Edges_In(v, X/\E) + card Edges_Out(v, X) by Th30
.= Degree(v, X/\the carrier' of G) by Th30;
end;
theorem Th32:
c is non empty & vs is_vertex_seq_of c implies (v in rng vs iff
Degree(v, rng c) <> 0)
proof
assume that
A1: c is non empty and
A2: vs is_vertex_seq_of c;
hereby
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then
A3: rng c c= the carrier' of G by FINSEQ_1:def 4;
assume that
A4: v in rng vs and
A5: Degree(v, rng c) = 0;
A6: Edges_In(v, rng c) = {} & Edges_Out(v, rng c) = {} by A5;
A7: 0+1 <= len c by A1,NAT_1:13;
A8: len vs = len c + 1 by A2;
consider i being Nat such that
A9: i in dom vs and
A10: vs.i = v by A4,FINSEQ_2:10;
A11: 1 <= i by A9,FINSEQ_3:25;
A12: i <= len vs by A9,FINSEQ_3:25;
per cases by A12,XXREAL_0:1;
suppose
A13: i = len vs;
set ic = len c;
ic in dom c by A7,FINSEQ_3:25;
then
A14: c.ic in rng c by FUNCT_1:def 3;
vs.len vs = (the Target of G).(c.len c) or vs.len vs = (the Source
of G).(c.len c) by A2,A7,Lm3;
hence contradiction by A6,A10,A3,A13,A14,Def1,Def2;
end;
suppose
i < len vs;
then
A15: i <= len c by A8,NAT_1:13;
then i in dom c by A11,FINSEQ_3:25;
then
A16: c.i in rng c by FUNCT_1:def 3;
vs.i = (the Target of G).(c.i) or vs.i = (the Source of G).(c.i) by A2
,A11,A15,Lm3;
hence contradiction by A6,A10,A3,A16,Def1,Def2;
end;
end;
assume that
A17: Degree(v, rng c) <> 0 and
A18: not v in rng vs;
per cases by A17;
suppose
card Edges_In(v, rng c) <> 0;
then consider e being object such that
A19: e in Edges_In(v, rng c) by CARD_1:27,XBOOLE_0:def 1;
A20: (the Target of G).e = v by A19,Def1;
e in rng c by A19,Def1;
then consider i being Nat such that
A21: i in dom c and
A22: c.i = e by FINSEQ_2:10;
A23: 1 <= i by A21,FINSEQ_3:25;
A24: i <= len c by A21,FINSEQ_3:25;
then 1 <= i+1 & i+1 <= len vs by A2,A23,Lm3;
then
A25: i+1 in dom vs by FINSEQ_3:25;
i <= len vs by A2,A23,A24,Lm3;
then
A26: i in dom vs by A23,FINSEQ_3:25;
vs.i = (the Target of G).(c.i) & vs.(i+1) = (the Source of G).(c .i)
or vs.i = (the Source of G).(c.i) & vs.(i+1) = (the Target of G).(c.i) by A2
,A23,A24,Lm3;
hence contradiction by A18,A20,A22,A26,A25,FUNCT_1:def 3;
end;
suppose
card Edges_Out(v, rng c) <> 0;
then consider e being object such that
A27: e in Edges_Out(v, rng c) by CARD_1:27,XBOOLE_0:def 1;
A28: (the Source of G).e = v by A27,Def2;
e in rng c by A27,Def2;
then consider i being Nat such that
A29: i in dom c and
A30: c.i = e by FINSEQ_2:10;
A31: 1 <= i by A29,FINSEQ_3:25;
A32: i <= len c by A29,FINSEQ_3:25;
then 1 <= i+1 & i+1 <= len vs by A2,A31,Lm3;
then
A33: i+1 in dom vs by FINSEQ_3:25;
i <= len vs by A2,A31,A32,Lm3;
then
A34: i in dom vs by A31,FINSEQ_3:25;
vs.i = (the Target of G).(c.i) & vs.(i+1) = (the Source of G).(c .i)
or vs.i = (the Source of G).(c.i) & vs.(i+1) = (the Target of G).(c.i) by A2
,A31,A32,Lm3;
hence contradiction by A18,A28,A30,A34,A33,FUNCT_1:def 3;
end;
end;
theorem Th33:
for G being non void finite connected Graph, v being Vertex of G
holds Degree v <> 0
proof
let G be non void finite connected Graph, v be Vertex of G;
assume
A1: Degree v = 0;
set E = the carrier' of G;
A2: Degree v = Degree(v, E) by Th24
.= card Edges_In(v, E) + card Edges_Out(v, E);
then
A3: Edges_In(v, E) = {} by A1;
A4: Edges_Out(v, E) = {} by A1,A2;
set S = the Source of G;
set T = the Target of G;
consider e being object such that
A5: e in E by XBOOLE_0:def 1;
reconsider s = S.e as Vertex of G by A5,FUNCT_2:5;
per cases;
suppose
v = s;
hence contradiction by A4,A5,Def2;
end;
suppose
v <> s;
then consider
c be Chain of G, vs be FinSequence of the carrier of G such that
A6: c is non empty and
A7: vs is_vertex_seq_of c and
A8: vs.1 = v and
vs.len vs = s by Th18;
A9: 0+1 <= len c by A6,NAT_1:13;
then 1 in dom c by FINSEQ_3:25;
then
A10: c.1 in rng c by FUNCT_1:def 3;
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then
A11: rng c c= the carrier' of G by FINSEQ_1:def 4;
vs.1 = T.(c.1) or vs.1 = S.(c.1) by A7,A9,Lm3;
hence contradiction by A3,A4,A8,A11,A10,Def1,Def2;
end;
end;
begin :: Adding an edge to a graph
definition
let G be Graph, v1, v2 be Vertex of G;
func AddNewEdge(v1, v2) -> strict Graph means
:Def7:
the carrier of it = the
carrier of G & the carrier' of it = (the carrier' of G) \/ {the carrier' of G}
& the Source of it = (the Source of G) +* ((the carrier' of G) .--> v1) & the
Target of it = (the Target of G) +* ((the carrier' of G) .--> v2);
existence
proof
set T = the Target of G;
set E = the carrier' of G;
set V = the carrier of G;
set Eit = E \/ {E};
set t = E .--> v2;
A1: {v1} c= V by ZFMISC_1:31;
set Tit = T +* (E .--> v2);
A3: {v2} c= V by ZFMISC_1:31;
rng t = {v2} & rng T c= V by FUNCOP_1:8,RELAT_1:def 19;
then rng Tit c= rng T \/ rng t & rng T \/ rng t c= V by A3,FUNCT_4:17
,XBOOLE_1:8;
then
A4: rng Tit c= V;
dom Tit = dom T \/ dom t by FUNCT_4:def 1
.= Eit by FUNCT_2:def 1;
then reconsider Tit as Function of Eit, V by A4,FUNCT_2:def 1,RELSET_1:4;
set S = the Source of G;
set s = E .--> v1;
set Sit = S +* (E .--> v1);
A6: dom Sit = dom S \/ dom s by FUNCT_4:def 1
.= Eit by FUNCT_2:def 1;
rng s = {v1} & rng S c= V by FUNCOP_1:8,RELAT_1:def 19;
then rng Sit c= rng S \/ rng s & rng S \/ rng s c= V by A1,FUNCT_4:17
,XBOOLE_1:8;
then rng Sit c= V;
then reconsider Sit as Function of Eit, V by A6,FUNCT_2:def 1,RELSET_1:4;
reconsider IT = MultiGraphStruct(#V, Eit, Sit, Tit#) as strict non empty
MultiGraphStruct;
take IT;
thus thesis;
end;
uniqueness;
end;
registration
let G be finite Graph, v1, v2 be Vertex of G;
cluster AddNewEdge(v1, v2) -> finite;
coherence
proof
reconsider E = the carrier' of G as finite set by GRAPH_1:def 11;
reconsider V = the carrier of G as finite set by GRAPH_1:def 11;
the carrier of AddNewEdge(v1, v2) = V by Def7;
hence the carrier of AddNewEdge(v1, v2) is finite;
the carrier' of AddNewEdge(v1, v2) = E \/ {the carrier' of G} by Def7;
hence thesis;
end;
end;
reserve G for Graph,
v, v1, v2 for Vertex of G,
c for Chain of G,
p for Path of G,
vs for FinSequence of the carrier of G,
v9 for Vertex of AddNewEdge(v1, v2),
p9 for Path of AddNewEdge(v1, v2),
vs9 for FinSequence of the carrier of AddNewEdge(v1, v2);
theorem Th34:
(the carrier' of G) in the carrier' of AddNewEdge(v1, v2) & the
carrier' of G = (the carrier' of AddNewEdge(v1, v2)) \ {the carrier' of G} & (
the Source of AddNewEdge(v1, v2)).(the carrier' of G) = v1 & (the Target of
AddNewEdge(v1, v2)).(the carrier' of G) = v2
proof
set G9 = AddNewEdge(v1, v2);
set E = the carrier' of G;
set S = the Source of G;
set T = the Target of G;
set E9 = the carrier' of G9;
A1: E9 = E \/ {E} by Def7;
E in {E} by TARSKI:def 1;
hence E in E9 by A1,XBOOLE_0:def 3;
now
let x be object;
hereby
assume
A2: x in E; then
reconsider x1=x as set;
not x1 in x1;
then x <> E by A2;
then
A3: not x in {E} by TARSKI:def 1;
x in E9 by A1,A2,XBOOLE_0:def 3;
hence x in E9 \ {E} by A3,XBOOLE_0:def 5;
end;
assume
A4: x in E9 \ {E};
then not x in {E} by XBOOLE_0:def 5;
hence x in E by A1,A4,XBOOLE_0:def 3;
end;
hence E = E9 \ {E} by TARSKI:2;
A5: E in dom (E .--> v1) by TARSKI:def 1;
the Source of G9 = S +* (E .--> v1) by Def7;
hence (the Source of G9).E = (E .--> v1).E by A5,FUNCT_4:13
.= v1 by FUNCOP_1:72;
A6: E in dom (E .--> v2) by TARSKI:def 1;
the Target of G9 = T +* (E .--> v2) by Def7;
hence (the Target of G9).E = (E .--> v2).E by A6,FUNCT_4:13
.= v2 by FUNCOP_1:72;
end;
theorem Th35:
e in the carrier' of G implies (the Source of AddNewEdge(v1, v2)
).e = (the Source of G).e & (the Target of AddNewEdge(v1, v2)).e = (the Target
of G).e
proof
set S = the Source of G;
set T = the Target of G;
set E = the carrier' of G;
set G9 = AddNewEdge(v1, v2);
set S9 = the Source of G9;
set T9 = the Target of G9;
assume
A1: e in the carrier' of G;
A2: not e in dom (E .--> v1)
proof
assume e in dom(E .--> v1);
then e in {E};
then e = E by TARSKI:def 1;
hence contradiction by A1;
end;
thus S9.e = (S +* (E .--> v1)).e by Def7
.= S.e by A2,FUNCT_4:11;
A3: not e in dom (E .--> v2)
proof
assume e in dom(E .--> v2);
then e in {E};
then e = E by TARSKI:def 1;
hence contradiction by A1;
end;
thus T9.e = (T +* (E .--> v2)).e by Def7
.= T.e by A3,FUNCT_4:11;
end;
theorem Th36:
vs9 = vs & vs is_vertex_seq_of c implies vs9 is_vertex_seq_of c
proof
assume that
A1: vs9 = vs and
A2: vs is_vertex_seq_of c;
thus len vs9 = len c + 1 by A1,A2;
let n be Nat;
set T = the Target of G;
set S = the Source of G;
set v = c.n;
set x = vs/.n;
set y = vs/.(n+1);
assume
A3: 1<=n & n<=len c;
then c.n joins vs/.n, vs/.(n+1) by A2;
then
A4: S.v = x & T.v = y or S.v = y & T.v = x;
set G9 = AddNewEdge(v1, v2);
set S9 = the Source of G9;
set T9 = the Target of G9;
A5: the carrier of G = the carrier of G9 by Def7;
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then
A6: rng c c= the carrier' of G by FINSEQ_1:def 4;
n in dom c by A3,FINSEQ_3:25;
then c.n in rng c by FUNCT_1:def 3;
then S9.v = S.v & T.v = T9.v by A6,Th35;
hence thesis by A1,A5,A4;
end;
theorem Th37:
c is Chain of AddNewEdge(v1, v2)
proof
set G9 = AddNewEdge(v1, v2);
consider p being FinSequence of the carrier of G such that
A1: p is_vertex_seq_of c by GRAPH_2:33;
c is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then
A2: rng c c= the carrier' of G by FINSEQ_1:def 4;
the carrier' of G9 = (the carrier' of G) \/ {the carrier' of G} by Def7;
then the carrier' of G c= the carrier' of G9 by XBOOLE_1:7;
then rng c c= the carrier' of G9 by A2;
hence c is FinSequence of the carrier' of G9 by FINSEQ_1:def 4;
reconsider p9 = p as FinSequence of the carrier of G9 by Def7;
take p9;
thus thesis by A1,Th36;
end;
theorem
p is Path of AddNewEdge(v1, v2) by Th37;
theorem Th39:
v9 = v1 & v1 <> v2 implies Edges_In(v9, X) = Edges_In(v1, X)
proof
assume that
A1: v9 = v1 and
A2: v1 <> v2;
set G9 = AddNewEdge(v1, v2);
set E = the carrier' of G;
set T = the Target of G;
set E9 = the carrier' of G9;
set T9 = the Target of G9;
A3: E9 = E \/ {E} by Def7;
now
let x be object;
hereby
assume
A4: x in Edges_In(v9, X);
then
A5: x in X by Def1;
A6: T9.x = v9 by A4,Def1;
T9.E = v2 by Th34;
then not x in {E} by A1,A2,A6,TARSKI:def 1;
then
A7: x in E by A3,A4,XBOOLE_0:def 3;
then T.x = v1 by A1,A6,Th35;
hence x in Edges_In(v1, X) by A5,A7,Def1;
end;
assume
A8: x in Edges_In(v1, X);
then T.x = v1 by Def1;
then
A9: T9.x = v9 by A1,A8,Th35;
x in X & x in E9 by A3,A8,Def1,XBOOLE_0:def 3;
hence x in Edges_In(v9, X) by A9,Def1;
end;
hence thesis by TARSKI:2;
end;
theorem Th40:
v9 = v2 & v1 <> v2 implies Edges_Out(v9, X) = Edges_Out(v2, X)
proof
assume that
A1: v9 = v2 and
A2: v1 <> v2;
set G9 = AddNewEdge(v1, v2);
set E = the carrier' of G;
set S = the Source of G;
set E9 = the carrier' of G9;
set S9 = the Source of G9;
A3: E9 = E \/ {E} by Def7;
now
let x be object;
hereby
assume
A4: x in Edges_Out(v9, X);
then
A5: x in X by Def2;
A6: S9.x = v9 by A4,Def2;
S9.E = v1 by Th34;
then not x in {E} by A1,A2,A6,TARSKI:def 1;
then
A7: x in E by A3,A4,XBOOLE_0:def 3;
then S.x = v2 by A1,A6,Th35;
hence x in Edges_Out(v2, X) by A5,A7,Def2;
end;
assume
A8: x in Edges_Out(v2, X);
then S.x = v2 by Def2;
then
A9: S9.x = v9 by A1,A8,Th35;
x in X & x in E9 by A3,A8,Def2,XBOOLE_0:def 3;
hence x in Edges_Out(v9, X) by A9,Def2;
end;
hence thesis by TARSKI:2;
end;
theorem Th41:
v9 = v1 & (the carrier' of G) in X implies Edges_Out(v9, X) =
Edges_Out(v1, X) \/ {the carrier' of G} & Edges_Out(v1, X) misses {the carrier'
of G}
proof
assume that
A1: v9 = v1 and
A2: (the carrier' of G) in X;
set G9 = AddNewEdge(v1, v2);
set E = the carrier' of G;
set S = the Source of G;
set E9 = the carrier' of G9;
set S9 = the Source of G9;
A3: E9 = E \/ {E} by Def7;
now
let x be object;
hereby
assume
A4: x in Edges_Out(v9, X);
then
A5: x in X by Def2;
A6: S9.x = v9 by A4,Def2;
per cases by A3,A4,XBOOLE_0:def 3;
suppose
A7: x in E;
then S.x = v1 by A1,A6,Th35;
then x in Edges_Out(v1, X) by A5,A7,Def2;
hence x in Edges_Out(v1, X) \/ {E} by XBOOLE_0:def 3;
end;
suppose
x in {E};
hence x in Edges_Out(v1, X) \/ {E} by XBOOLE_0:def 3;
end;
end;
assume
A8: x in Edges_Out(v1, X) \/ {E};
per cases by A8,XBOOLE_0:def 3;
suppose
A9: x in Edges_Out(v1, X);
then S.x = v1 by Def2;
then
A10: S9.x = v9 by A1,A9,Th35;
x in X & x in E9 by A3,A9,Def2,XBOOLE_0:def 3;
hence x in Edges_Out(v9, X) by A10,Def2;
end;
suppose
A11: x in {E};
A12: S9.E = v1 by Th34;
x = E & x in E9 by A3,A11,TARSKI:def 1,XBOOLE_0:def 3;
hence x in Edges_Out(v9, X) by A1,A2,A12,Def2;
end;
end;
hence Edges_Out(v9, X) = Edges_Out(v1, X) \/ {E} by TARSKI:2;
assume Edges_Out(v1, X) /\ {E} <> {};
then consider x being object such that
A13: x in Edges_Out(v1, X) /\ {E} by XBOOLE_0:def 1;
x in {E} by A13,XBOOLE_0:def 4;
then
A14: x = E by TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
A: not xx in xx;
x in E by A13;
hence contradiction by A14,A;
end;
theorem Th42:
v9 = v2 & (the carrier' of G) in X implies Edges_In(v9, X) =
Edges_In(v2, X) \/ {the carrier' of G} & Edges_In(v2, X) misses {the carrier'
of G}
proof
assume that
A1: v9 = v2 and
A2: (the carrier' of G) in X;
set G9 = AddNewEdge(v1, v2);
set E = the carrier' of G;
set T = the Target of G;
set E9 = the carrier' of G9;
set T9 = the Target of G9;
A3: E9 = E \/ {E} by Def7;
now
let x be object;
hereby
assume
A4: x in Edges_In(v9, X);
then
A5: x in X by Def1;
A6: T9.x = v9 by A4,Def1;
per cases by A3,A4,XBOOLE_0:def 3;
suppose
A7: x in E;
then T.x = v2 by A1,A6,Th35;
then x in Edges_In(v2, X) by A5,A7,Def1;
hence x in Edges_In(v2, X) \/ {E} by XBOOLE_0:def 3;
end;
suppose
x in {E};
hence x in Edges_In(v2, X) \/ {E} by XBOOLE_0:def 3;
end;
end;
assume
A8: x in Edges_In(v2, X) \/ {E};
per cases by A8,XBOOLE_0:def 3;
suppose
A9: x in Edges_In(v2, X);
then T.x = v2 by Def1;
then
A10: T9.x = v9 by A1,A9,Th35;
x in X & x in E9 by A3,A9,Def1,XBOOLE_0:def 3;
hence x in Edges_In(v9, X) by A10,Def1;
end;
suppose
A11: x in {E};
A12: T9.E = v2 by Th34;
x = E & x in E9 by A3,A11,TARSKI:def 1,XBOOLE_0:def 3;
hence x in Edges_In(v9, X) by A1,A2,A12,Def1;
end;
end;
hence Edges_In(v9, X) = Edges_In(v2, X) \/ {E} by TARSKI:2;
assume Edges_In(v2, X) /\ {E} <> {};
then consider x being object such that
A13: x in Edges_In(v2, X) /\ {E} by XBOOLE_0:def 1;
x in {E} by A13,XBOOLE_0:def 4;
then
A14: x = E by TARSKI:def 1;
A: x in E by A13;
reconsider xx = x as set by TARSKI:1;
not xx in xx;
hence contradiction by A14,A;
end;
theorem Th43:
v9 = v & v <> v2 implies Edges_In(v9, X) = Edges_In(v, X)
proof
assume that
A1: v9 = v and
A2: v <> v2;
set G9 = AddNewEdge(v1, v2);
set E = the carrier' of G;
set T = the Target of G;
set E9 = the carrier' of G9;
set T9 = the Target of G9;
A3: E9 = E \/ {E} by Def7;
now
let x be object;
hereby
assume
A4: x in Edges_In(v9, X);
then
A5: x in X by Def1;
A6: T9.x = v9 by A4,Def1;
T9.E = v2 by Th34;
then not x in {E} by A1,A2,A6,TARSKI:def 1;
then
A7: x in E by A3,A4,XBOOLE_0:def 3;
then T.x = v by A1,A6,Th35;
hence x in Edges_In(v, X) by A5,A7,Def1;
end;
assume
A8: x in Edges_In(v, X);
then T.x = v by Def1;
then
A9: T9.x = v9 by A1,A8,Th35;
x in X & x in E9 by A3,A8,Def1,XBOOLE_0:def 3;
hence x in Edges_In(v9, X) by A9,Def1;
end;
hence thesis by TARSKI:2;
end;
theorem Th44:
v9 = v & v <> v1 implies Edges_Out(v9, X) = Edges_Out(v, X)
proof
assume that
A1: v9 = v and
A2: v <> v1;
set G9 = AddNewEdge(v1, v2);
set E = the carrier' of G;
set S = the Source of G;
set E9 = the carrier' of G9;
set S9 = the Source of G9;
A3: E9 = E \/ {E} by Def7;
now
let x be object;
hereby
assume
A4: x in Edges_Out(v9, X);
then
A5: x in X by Def2;
A6: S9.x = v9 by A4,Def2;
S9.E = v1 by Th34;
then not x in {E} by A1,A2,A6,TARSKI:def 1;
then
A7: x in E by A3,A4,XBOOLE_0:def 3;
then S.x = v by A1,A6,Th35;
hence x in Edges_Out(v, X) by A5,A7,Def2;
end;
assume
A8: x in Edges_Out(v, X);
then S.x = v by Def2;
then
A9: S9.x = v9 by A1,A8,Th35;
x in X & x in E9 by A3,A8,Def2,XBOOLE_0:def 3;
hence x in Edges_Out(v9, X) by A9,Def2;
end;
hence thesis by TARSKI:2;
end;
theorem Th45:
not (the carrier' of G) in rng p9 implies p9 is Path of G
proof
set G9 = AddNewEdge(v1, v2);
set S = the Source of G;
set T = the Target of G;
set E = the carrier' of G;
set S9 = the Source of G9;
set T9 = the Target of G9;
the carrier' of G9 = E \/ {E} by Def7;
then
A1: rng p9 c= E \/ {E} by FINSEQ_1:def 4;
assume
A2: not (the carrier' of G) in rng p9;
A3: rng p9 c= E
proof
let x be object;
assume
A4: x in rng p9;
then x in E or x in {E} by A1,XBOOLE_0:def 3;
hence thesis by A2,A4,TARSKI:def 1;
end;
p9 is Chain of G
proof
thus p9 is FinSequence of the carrier' of G by A3,FINSEQ_1:def 4;
consider vs9 being FinSequence of the carrier of G9 such that
A5: vs9 is_vertex_seq_of p9 by MSSCYC_1:def 1;
reconsider vs = vs9 as FinSequence of the carrier of G by Def7;
take vs;
thus vs is_vertex_seq_of p9
proof
thus
A6: len vs = len p9 + 1 by A5;
let n be Nat;
assume that
A7: 1<=n and
A8: n<=len p9;
set e = p9.n;
reconsider vn9 = vs9/.n, vn19 = vs9/.(n+1) as Vertex of G9;
p9.n joins vs9/.n, vs9/.(n+1) by A5,A7,A8;
then
A9: S9.e = vn9 & T9.e = vn19 or S9.e = vn19 & T9.e = vn9;
reconsider vn = vs/.n, vn1 = vs/.(n+1) as Vertex of G;
1 <= n+1 & n+1 <= len vs by A6,A8,NAT_1:11,XREAL_1:6;
then
A10: n+1 in dom vs by FINSEQ_3:25;
then
A11: vn1 = vs.(n+1) by PARTFUN1:def 6
.= vn19 by A10,PARTFUN1:def 6;
n in dom p9 by A7,A8,FINSEQ_3:25;
then e in rng p9 by FUNCT_1:def 3;
then
A12: S9.e = S.e & T9.e = T.e by A3,Th35;
len p9 <= len vs by A6,NAT_1:11;
then n <= len vs by A8,XXREAL_0:2;
then
A13: n in dom vs by A7,FINSEQ_3:25;
then vn = vs.n by PARTFUN1:def 6
.= vn9 by A13,PARTFUN1:def 6;
hence thesis by A9,A12,A11;
end;
end;
then reconsider p99 = p9 as Chain of G;
p99 is one-to-one;
hence thesis;
end;
theorem Th46:
not (the carrier' of G) in rng p9 & vs = vs9 & vs9
is_vertex_seq_of p9 implies vs is_vertex_seq_of p9
proof
set G9 = AddNewEdge(v1, v2);
set S = the Source of G;
set T = the Target of G;
set E = the carrier' of G;
set S9 = the Source of G9;
set T9 = the Target of G9;
the carrier' of G9 = E \/ {E} by Def7;
then
A1: rng p9 c= E \/ {E} by FINSEQ_1:def 4;
assume
A2: not (the carrier' of G) in rng p9;
A3: rng p9 c= E
proof
let x be object;
assume
A4: x in rng p9;
then x in E or x in {E} by A1,XBOOLE_0:def 3;
hence thesis by A2,A4,TARSKI:def 1;
end;
assume that
A5: vs = vs9 and
A6: vs9 is_vertex_seq_of p9;
thus vs is_vertex_seq_of p9
proof
thus
A7: len vs = len p9 + 1 by A5,A6;
let n be Nat;
assume that
A8: 1<=n and
A9: n<=len p9;
set e = p9.n;
reconsider vn9 = vs9/.n, vn19 = vs9/.(n+1) as Vertex of G9;
p9.n joins vs9/.n, vs9/.(n+1) by A6,A8,A9;
then
A10: S9.e = vn9 & T9.e = vn19 or S9.e = vn19 & T9.e = vn9;
reconsider vn = vs/.n, vn1 = vs/.(n+1) as Vertex of G;
1 <= n+1 & n+1 <= len vs by A7,A9,NAT_1:11,XREAL_1:6;
then
A11: n+1 in dom vs by FINSEQ_3:25;
then
A12: vn1 = vs.(n+1) by PARTFUN1:def 6
.= vn19 by A5,A11,PARTFUN1:def 6;
n in dom p9 by A8,A9,FINSEQ_3:25;
then e in rng p9 by FUNCT_1:def 3;
then
A13: S9.e = S.e & T9.e = T.e by A3,Th35;
len p9 <= len vs by A7,NAT_1:11;
then n <= len vs by A9,XXREAL_0:2;
then
A14: n in dom vs by A8,FINSEQ_3:25;
then vn = vs.n by PARTFUN1:def 6
.= vn9 by A5,A14,PARTFUN1:def 6;
hence thesis by A10,A13,A12;
end;
end;
registration
let G be connected Graph, v1, v2 be Vertex of G;
cluster AddNewEdge(v1, v2) -> connected;
coherence
proof
set G9 = AddNewEdge(v1, v2);
now
let v19, v29 be Vertex of G9;
reconsider v1 = v19, v2 = v29 as Vertex of G by Def7;
assume v19 <> v29;
then consider
c being Chain of G, vs being FinSequence of the carrier of G
such that
A1: c is non empty and
A2: vs is_vertex_seq_of c and
A3: vs.1 = v1 & vs.len vs = v2 by Th18;
reconsider vs9 = vs as FinSequence of the carrier of G9 by Def7;
reconsider c9 = c as Chain of G9 by Th37;
take c9;
take vs9;
thus c9 is non empty by A1;
thus vs9 is_vertex_seq_of c9 by A2,Th36;
thus vs9.1 = v19 & vs9.len vs9 = v29 by A3;
end;
hence thesis by Th18;
end;
end;
reserve G for finite Graph,
v, v1, v2 for Vertex of G,
vs for FinSequence of the carrier of G,
v9 for Vertex of AddNewEdge(v1, v2);
theorem Th47:
v9 = v & v1 <> v2 & (v = v1 or v = v2) & (the carrier' of G) in
X implies Degree(v9, X) = Degree(v, X) +1
proof
assume that
A1: v9 = v and
A2: v1 <> v2 and
A3: v = v1 or v = v2 and
A4: (the carrier' of G) in X;
set E = the carrier' of G;
per cases by A3;
suppose
A5: v = v1;
then
Edges_In(v9, X) = Edges_In(v, X) & Edges_Out(v9, X) = Edges_Out(v, X)
\/ {E} by A1,A2,A4,Th39,Th41;
hence
Degree(v9, X) = card Edges_In(v, X) + (card Edges_Out(v, X) + card {E
}) by A1,A4,A5,Th41,CARD_2:40
.= card Edges_In(v, X) + card Edges_Out(v, X) + card {E}
.= Degree(v, X) +1 by CARD_1:30;
end;
suppose
A6: v = v2;
then
Edges_Out(v9, X) = Edges_Out(v, X) & Edges_In(v9, X) = Edges_In(v, X)
\/ {E} by A1,A2,A4,Th40,Th42;
hence
Degree(v9, X) = card Edges_In(v, X) + card {E} + card Edges_Out(v, X)
by A1,A4,A6,Th42,CARD_2:40
.= card Edges_In(v, X) + card Edges_Out(v, X) + card {E}
.= Degree(v, X) +1 by CARD_1:30;
end;
end;
theorem Th48:
v9 = v & v <> v1 & v <> v2 implies Degree(v9, X) = Degree(v, X)
proof
assume that
A1: v9 = v and
A2: v <> v1 and
A3: v <> v2;
thus Degree(v9, X) = card Edges_In(v,X) + card Edges_Out(v9,X) by A1,A3,Th43
.= Degree(v, X) by A1,A2,Th44;
end;
begin :: Some properties of and operations on cycles
Lm4: for G being finite Graph, c be cyclic Path of G, vs being FinSequence of
the carrier of G, v being Vertex of G st vs is_vertex_seq_of c & v in rng vs
holds Degree(v, rng c) is even
proof
let G be finite Graph, c be cyclic Path of G, vs be FinSequence of the
carrier of G,v be Vertex of G;
assume that
A1: vs is_vertex_seq_of c and
A2: v in rng vs;
set S = the Source of G;
set T = the Target of G;
per cases;
suppose
c is empty;
then reconsider rc = rng c as empty set;
Degree(v, rc)= 2 * 0;
hence thesis;
end;
suppose
A3: c is non empty;
set ev = { n where n is Element of NAT : 1 <= n & n <= len c & vs.n = v };
A4: ev c= Seg len c
proof
let x be object;
assume x in ev;
then ex n being Element of NAT st x = n & 1 <= n & n <= len c & vs.n = v;
hence thesis by FINSEQ_1:1;
end;
reconsider rc = rng c as non empty set by A3;
A5: len vs = len c + 1 by A1;
set evout = [:{1}, Edges_Out(v, rc):];
set evin = [:{0}, Edges_In(v, rc):];
A6: card evout = card {1} * card Edges_Out(v, rc) by CARD_2:46
.= 1 * card Edges_Out(v, rc) by CARD_1:30
.= card Edges_Out(v, rc);
A7: card evin = card {0} * card Edges_In(v, rc) by CARD_2:46
.= 1 * card Edges_In(v, rc) by CARD_1:30
.= card Edges_In(v, rc);
now
assume
A8: evin \/ evout is empty;
then evin is empty;
then Degree(v, rc) = 0 + 0 by A7,A6,A8;
hence contradiction by A1,A2,A3,Th32;
end;
then reconsider evio = evin \/ evout as non empty set;
A9: evin misses evout
proof
assume not thesis;
then consider x being object such that
A10: x in evin /\ evout by XBOOLE_0:4;
x in evout by A10,XBOOLE_0:def 4;
then consider x21, x22 being object such that
A11: x21 in {1} and
x22 in Edges_Out(v,rc) and
A12: x = [x21,x22] by ZFMISC_1:def 2;
A13: x21 = 1 by A11,TARSKI:def 1;
x in evin by A10,XBOOLE_0:def 4;
then consider x11, x12 being object such that
A14: x11 in {0} and
x12 in Edges_In(v, rc) and
A15: x = [x11,x12] by ZFMISC_1:def 2;
x11 = 0 by A14,TARSKI:def 1;
hence contradiction by A15,A12,A13,XTUPLE_0:1;
end;
reconsider ev as Subset of Seg len c by A4;
A16: rc c= the carrier' of G by FINSEQ_1:def 4;
then reconsider G9 = G as non void finite Graph;
reconsider vs9 = vs as FinSequence of the carrier of G9;
A17: vs9.1 = vs.(len vs) by A1,MSSCYC_1:6;
now
A18: 0+1 <= len c by A3,NAT_1:13;
consider n being object such that
A19: n in dom vs and
A20: vs.n = v by A2,FUNCT_1:def 3;
reconsider n as Element of NAT by A19;
A21: n <= len vs by A19,FINSEQ_3:25;
A22: 1 <= n by A19,FINSEQ_3:25;
thus ev is non empty
proof
per cases by A21,XXREAL_0:1;
suppose
n = len vs;
then 1 in ev by A17,A20,A18;
hence thesis;
end;
suppose
n < len vs;
then n <= len c by A5,NAT_1:13;
then n in ev by A20,A22;
hence thesis;
end;
end;
end;
then reconsider ev as finite non empty set;
set ev92 = [:2, ev:];
now
defpred R[Element of ev92, Element of evio, Element of NAT] means $1 = [
1,$3] & ((vs.$3 = S.(c.$3) & $2 = [1,c.$3]) or (vs.$3 = T.(c.$3) & $2 = [0,c.$3
] & T.(c.$3) <> S.(c.$3)));
defpred L[Element of ev92, Element of evio, Element of NAT] means $1 = [
0,$3] & ((ex k being Element of NAT st 1 <= k & $3 = k+1 & (vs.$3 = T.(c.k) &
$2 = [0, c.k] or vs.$3 = S.(c.k) & $2 = [1, c.k] & T.(c.k) <> S.(c.k))) or $3 =
1 & (vs.1 = T.(c.len c) & $2 = [0, c.len c] or vs.1 = S.(c.len c) & $2 = [1, c.
len c] & T.(c.len c) <> S.(c.len c)));
take Z = { [x, y] where x is Element of ev92, y is Element of evio : ex
n being Element of NAT st 1 <= n & n <= len c & (L[x, y, n] or R[x, y, n])};
thus for x being object st x in ev92
ex y being object st y in evin \/ evout & [x,y] in Z
proof
A23: 1 in {1} by TARSKI:def 1;
let x be object;
A24: 0 in {0} by TARSKI:def 1;
assume
A25: x in ev92;
then consider u, w being object such that
A26: [u, w] = x by RELAT_1:def 1;
reconsider x9 = x as Element of ev92 by A25;
A27: u in 2 by A25,A26,ZFMISC_1:87;
w in ev by A25,A26,ZFMISC_1:87;
then consider n being Element of NAT such that
A28: w = n and
A29: 1 <= n and
A30: n <= len c and
A31: vs.n = v;
per cases by A27,CARD_1:50,TARSKI:def 2;
suppose
A32: u = 0;
thus ex y being object st y in evin \/ evout & [x,y] in Z
proof
per cases by A29,XXREAL_0:1;
suppose
1 < n;
then consider k being Element of NAT such that
A33: n = 1+k and
A34: 1 <= k by FINSEQ_4:84;
k <= n by A33,NAT_1:11;
then
A35: k <= len c by A30,XXREAL_0:2;
then k in dom c by A34,FINSEQ_3:25;
then reconsider e = c.k as Element of rc by FUNCT_1:def 3;
A36: e in rc;
thus thesis
proof
per cases by A1,A34,A35,Lm3;
suppose
A37: T.(c.k) = vs.(k+1);
take y = [0, c.k];
e in Edges_In(v, rc) by A16,A31,A33,A36,A37,Def1;
then
A38: y in evin by A24,ZFMISC_1:87;
hence y in evin \/ evout by XBOOLE_0:def 3;
reconsider y9 = y as Element of evio by A38,XBOOLE_0:def 3;
L[x9,y9,n] by A26,A28,A32,A33,A34,A37;
hence thesis by A29,A30;
end;
suppose
A39: S.(c.k) = vs.(k+1) & T.(c.k) <> S.(c.k);
take y = [1, c.k];
e in Edges_Out(v, rc) by A16,A31,A33,A36,A39,Def2;
then
A40: y in evout by A23,ZFMISC_1:87;
hence y in evin \/ evout by XBOOLE_0:def 3;
reconsider y9 = y as Element of evio by A40,XBOOLE_0:def 3;
L[x9,y9,n] by A26,A28,A32,A33,A34,A39;
hence thesis by A29,A30;
end;
end;
end;
suppose
A41: n = 1;
A42: 1 <= len c by A29,A30,XXREAL_0:2;
then len c in dom c by FINSEQ_3:25;
then reconsider e = c.len c as Element of rc by FUNCT_1:def 3;
A43: 1 <= len c by A29,A30,XXREAL_0:2;
A44: e in rc & vs.1 = vs.(len c + 1) by A1,MSSCYC_1:6;
thus thesis
proof
per cases by A1,A42,Lm3;
suppose
A45: T.(c.len c) = vs.(len c+1);
take y = [0, c.len c];
e in Edges_In(v, rc) by A16,A31,A41,A44,A45,Def1;
then
A46: y in evin by A24,ZFMISC_1:87;
hence y in evin \/ evout by XBOOLE_0:def 3;
reconsider y9 = y as Element of evio by A46,XBOOLE_0:def 3;
L[x9,y9,1] by A1,A26,A28,A32,A41,A45,MSSCYC_1:6;
hence thesis by A43;
end;
suppose
A47: S.(c.len c) = vs.(len c+1) & T.(c.len c) <> S.(c. len c);
take y = [1, c.len c];
e in Edges_Out(v, rc) by A16,A31,A41,A44,A47,Def2;
then
A48: y in evout by A23,ZFMISC_1:87;
hence y in evin \/ evout by XBOOLE_0:def 3;
reconsider y9 = y as Element of evio by A48,XBOOLE_0:def 3;
L[x9,y9,1] by A1,A26,A28,A32,A41,A47,MSSCYC_1:6;
hence thesis by A43;
end;
end;
end;
end;
end;
suppose
A49: u = 1;
n in dom c by A29,A30,FINSEQ_3:25;
then reconsider e = c.n as Element of rc by FUNCT_1:def 3;
A50: e in rc;
thus ex y being object st y in evin \/ evout & [x,y] in Z
proof
per cases by A1,A29,A30,Lm3;
suppose
A51: vs.n = S.(c.n);
take y = [1,c.n];
e in Edges_Out(v, rc) by A16,A31,A50,A51,Def2;
then
A52: y in evout by A23,ZFMISC_1:87;
hence y in evin \/ evout by XBOOLE_0:def 3;
reconsider y9 = y as Element of evio by A52,XBOOLE_0:def 3;
R[x9,y9,n] by A26,A28,A49,A51;
hence thesis by A29,A30;
end;
suppose
A53: vs.n = T.(c.n) & T.(c.n) <> S.(c.n);
take y = [0,c.n];
e in Edges_In(v, rc) by A16,A31,A50,A53,Def1;
then
A54: y in evin by A24,ZFMISC_1:87;
hence y in evin \/ evout by XBOOLE_0:def 3;
reconsider y9 = y as Element of evio by A54,XBOOLE_0:def 3;
R[x9,y9,n] by A26,A28,A49,A53;
hence thesis by A29,A30;
end;
end;
end;
end;
thus for y being object st y in evin \/ evout
ex x being object st x in ev92 & [x,y] in Z
proof
let y be object;
assume
A55: y in evin \/ evout;
then reconsider y9 = y as Element of evio;
per cases by A55,XBOOLE_0:def 3;
suppose
A56: y in evin;
then consider u, e being object such that
A57: [u,e] = y by RELAT_1:def 1;
A58: e in Edges_In(v, rc) by A56,A57,ZFMISC_1:87;
then
A59: T.e = v by Def1;
e in rc by A58,Def1;
then consider n being object such that
A60: n in dom c and
A61: e = c.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A60;
A62: dom c = Seg len c by FINSEQ_1:def 3;
then
A63: 1 <= n by A60,FINSEQ_1:1;
A64: 1 in 2 by CARD_1:50,TARSKI:def 2;
A65: 0 in 2 by CARD_1:50,TARSKI:def 2;
A66: n <= len c by A60,A62,FINSEQ_1:1;
A67: u in {0} by A56,A57,ZFMISC_1:87;
then
A68: u = 0 by TARSKI:def 1;
thus ex x being object st x in ev92 & [x,y] in Z
proof
per cases by A1,A63,A66,Lm3;
suppose
A69: vs.(n+1) = T.(c.n);
thus thesis
proof
per cases by A66,XXREAL_0:1;
suppose
A70: n = len c;
take x = [0, 1];
vs.1 = v by A1,A59,A61,A69,A70,MSSCYC_1:6;
then
A71: 1 in ev by A63,A70;
hence x in ev92 by A65,ZFMISC_1:87;
reconsider x9 = x as Element of ev92 by A65,A71,ZFMISC_1:87;
1 <= len c & L[x9,y9,1] by A1,A57,A67,A60,A61,A62,A69,A70,
FINSEQ_1:1,MSSCYC_1:6,TARSKI:def 1;
hence thesis;
end;
suppose
A72: n < len c;
take x = [0, n+1];
A73: 1 <= n+1 & n+1 <= len c by A72,NAT_1:11,13;
then
A74: n+1 in ev by A59,A61,A69;
hence x in ev92 by A65,ZFMISC_1:87;
reconsider x9 = x as Element of ev92 by A65,A74,ZFMISC_1:87;
L[x9,y9,n+1] by A57,A68,A61,A63,A69;
hence thesis by A73;
end;
end;
end;
suppose
A75: vs.n = T.(c.n) & T.(c.n) <> S.(c.n);
take x = [1, n];
A76: n in ev by A59,A61,A63,A66,A75;
hence x in ev92 by A64,ZFMISC_1:87;
reconsider x9 = x as Element of ev92 by A64,A76,ZFMISC_1:87;
R[x9,y9, n] by A57,A67,A61,A75,TARSKI:def 1;
hence thesis by A63,A66;
end;
end;
end;
suppose
A77: y in evout;
then consider u, e being object such that
A78: [u,e] = y by RELAT_1:def 1;
A79: e in Edges_Out(v, rc) by A77,A78,ZFMISC_1:87;
then
A80: S.e = v by Def2;
e in rc by A79,Def2;
then consider n being object such that
A81: n in dom c and
A82: e = c.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A81;
A83: dom c = Seg len c by FINSEQ_1:def 3;
then
A84: 1 <= n by A81,FINSEQ_1:1;
A85: 1 in 2 by CARD_1:50,TARSKI:def 2;
A86: 0 in 2 by CARD_1:50,TARSKI:def 2;
A87: n <= len c by A81,A83,FINSEQ_1:1;
A88: u in {1} by A77,A78,ZFMISC_1:87;
then
A89: u = 1 by TARSKI:def 1;
thus ex x being object st x in ev92 & [x,y] in Z
proof
per cases by A1,A84,A87,Lm3;
suppose
A90: vs.(n+1) = S.(c.n) & T.(c.n) <> S.(c.n);
thus thesis
proof
per cases by A87,XXREAL_0:1;
suppose
A91: n = len c;
take x = [0, 1];
vs.1 = v by A1,A80,A82,A90,A91,MSSCYC_1:6;
then
A92: 1 in ev by A84,A91;
hence x in ev92 by A86,ZFMISC_1:87;
reconsider x9 = x as Element of ev92 by A86,A92,ZFMISC_1:87;
1 <= len c & L[x9,y9,1] by A1,A78,A88,A81,A82,A83,A90,A91,
FINSEQ_1:1,MSSCYC_1:6,TARSKI:def 1;
hence thesis;
end;
suppose
A93: n < len c;
take x = [0, n+1];
A94: 1 <= n+1 & n+1 <= len c by A93,NAT_1:11,13;
then
A95: n+1 in ev by A80,A82,A90;
hence x in ev92 by A86,ZFMISC_1:87;
reconsider x9 = x as Element of ev92 by A86,A95,ZFMISC_1:87;
L[x9,y9,n+1] by A78,A89,A82,A84,A90;
hence thesis by A94;
end;
end;
end;
suppose
A96: vs.n = S.(c.n);
take x = [1, n];
A97: n in ev by A80,A82,A84,A87,A96;
hence x in ev92 by A85,ZFMISC_1:87;
reconsider x9 = x as Element of ev92 by A85,A97,ZFMISC_1:87;
R[x9,y9, n] by A78,A88,A82,A96,TARSKI:def 1;
hence thesis by A84,A87;
end;
end;
end;
end;
thus for x,y,z,u being object st [x,y] in Z & [z,u] in Z holds
x = z iff y = u
proof
let x,y,z,u be object;
assume that
A98: [x,y] in Z and
A99: [z,u] in Z;
consider x9 being Element of ev92, y9 being Element of evio such that
A100: [x,y] = [x9,y9] and
A101: ex n being Element of NAT st 1 <= n & n <= len c & (L[x9,y9,
n] or R[x9,y9,n]) by A98;
consider z9 being Element of ev92, u9 being Element of evio such that
A102: [z,u] = [z9,u9] and
A103: ex n being Element of NAT st 1 <= n & n <= len c & (L[z9,u9,
n] or R[z9,u9,n]) by A99;
A104: x = x9 by A100,XTUPLE_0:1;
A105: y = y9 by A100,XTUPLE_0:1;
consider n2 being Element of NAT such that
A106: 1 <= n2 and
A107: n2 <= len c and
A108: L[z9,u9,n2] or R[z9,u9,n2] by A103;
consider n1 being Element of NAT such that
A109: 1 <= n1 and
A110: n1 <= len c and
A111: L[x9,y9,n1] or R[x9,y9,n1] by A101;
A112: z = z9 by A102,XTUPLE_0:1;
thus x = z implies y = u
proof
assume
A113: x = z;
per cases by A111,A108;
suppose
A114: L[x9,y9,n1] & L[z9,u9,n2];
then
A115: n1 = n2 by A104,A112,A113,XTUPLE_0:1;
thus y = u
proof
per cases by A114;
suppose
(ex k being Element of NAT st 1 <= k & n1 = k+1 & (
vs.n1 = T.(c.k) & y9 = [0, c.k] or vs.n1 = S.(c.k) & y9 = [1, c.k] & T.(c.k) <>
S.(c.k))) & ex k being Element of NAT st 1 <= k & n2 = k+1 & (vs.n2 = T.(c.k) &
u9 = [0, c.k] or vs.n2 = S.(c.k) & u9 = [1, c.k] & T.(c.k) <> S.(c.k));
hence thesis by A102,A105,A115,XTUPLE_0:1;
end;
suppose
(ex k being Element of NAT st 1 <= k & n1 = k+1 & (
vs.n1 = T.(c.k) & y9 = [0, c.k] or vs.n1 = S.(c.k) & y9 = [1, c.k] & T.(c.k) <>
S.(c.k))) & n2 = 1 & (vs.1 = T.(c.len c) & u9 = [0, c.len c] or vs.1 = S.(c.len
c) & u9 = [1, c.len c] & T.(c.len c) <> S.(c.len c));
hence thesis by A115;
end;
suppose
n1 = 1 & (vs.1 = T.(c.len c) & y9 = [0, c.len c] or
vs.1 = S.(c.len c) & y9 = [1, c.len c] & T.(c.len c) <> S.(c.len c)) & ex k
being Element of NAT st 1 <= k & n2 = k+1 & (vs.n2 = T.(c.k) & u9 = [0, c.k] or
vs.n2 = S.(c.k) & u9 = [1, c.k] & T.(c.k) <> S.(c.k));
hence thesis by A115;
end;
suppose
n1 = 1 & (vs.1 = T.(c.len c) & y9 = [0, c.len c] or
vs.1 = S.(c.len c) & y9 = [1, c.len c] & T.(c.len c) <> S.(c.len c)) & n2 = 1 &
(vs.1 = T.(c.len c) & u9 = [0, c.len c] or vs.1 = S.(c.len c) & u9 = [1, c.len
c] & T.(c.len c) <> S.(c.len c));
hence thesis by A102,A105,XTUPLE_0:1;
end;
end;
end;
suppose
L[x9,y9,n1] & R[z9,u9,n2];
hence thesis by A104,A112,A113,XTUPLE_0:1;
end;
suppose
R[x9,y9,n1] & L[z9,u9,n2];
hence thesis by A104,A112,A113,XTUPLE_0:1;
end;
suppose
A116: R[x9,y9,n1] & R[z9,u9,n2];
then n1 = n2 by A104,A112,A113,XTUPLE_0:1;
hence thesis by A100,A102,A116,XTUPLE_0:1;
end;
end;
A117: u = u9 by A102,XTUPLE_0:1;
thus y = u implies x = z
proof
assume
A118: y = u;
per cases by A111,A108;
suppose
A119: L[x9,y9,n1] & L[z9,u9,n2];
thus x = z
proof
per cases by A119;
suppose
A120: (ex k being Element of NAT st 1 <= k & n1 = k+1 & (
vs.n1 = T.(c.k) & y9 = [0, c.k] or vs.n1 = S.(c.k) & y9 = [1, c.k] & T.(c.k) <>
S.(c.k))) & ex k being Element of NAT st 1 <= k & n2 = k+1 & (vs.n2 = T.(c.k) &
u9 = [0, c.k] or vs.n2 = S.(c.k) & u9 = [1, c.k] & T.(c.k) <> S.(c.k));
then consider k2 being Element of NAT such that
A121: 1 <= k2 and
A122: n2 = k2+1 and
A123: vs.n2 = T.(c.k2) & u9 = [0, c.k2] or vs.n2 = S.(c.k2
) & u9 = [1, c.k2] & T.(c.k2) <> S.(c.k2);
k2 <= n2 by A122,NAT_1:12;
then
A124: k2 <= len c by A107,XXREAL_0:2;
consider k1 being Element of NAT such that
A125: 1 <= k1 and
A126: n1 = k1+1 and
A127: vs.n1 = T.(c.k1) & y9 = [0, c.k1] or vs.n1 = S.(c.k1
) & y9 = [1, c.k1] & T.(c.k1) <> S.(c.k1) by A120;
k1 <= n1 by A126,NAT_1:12;
then
A128: k1 <= len c by A110,XXREAL_0:2;
c.k1 = c.k2 by A105,A117,A118,A127,A123,XTUPLE_0:1;
then k1 = k2 by A125,A121,A128,A124,Lm2;
hence thesis by A100,A102,A119,A126,A122,XTUPLE_0:1;
end;
suppose
A129: (ex k being Element of NAT st 1 <= k & n1 = k+1 & (
vs.n1 = T.(c.k) & y9 = [0, c.k] or vs.n1 = S.(c.k) & y9 = [1, c.k] & T.(c.k) <>
S.(c.k))) & n2 = 1 & (vs.1 = T.(c.len c) & u9 = [0, c.len c] or vs.1 = S.(c.len
c) & u9 = [1, c.len c] & T.(c.len c) <> S.(c.len c));
A130: 1 <= len c by A109,A110,XXREAL_0:2;
consider k1 being Element of NAT such that
A131: 1 <= k1 and
A132: n1 = k1+1 and
vs.n1 = T.(c.k1) & y9 = [0, c.k1] or vs.n1 = S.(c.k1) & y9
= [1, c.k1] & T.(c.k1) <> S.(c.k1) by A129;
k1 <= n1 by A132,NAT_1:12;
then
A133: k1 <= len c by A110,XXREAL_0:2;
c.k1 = c.len c by A105,A117,A118,A129,A132,XTUPLE_0:1;
then len c + 1 <= len c by A110,A131,A132,A133,A130,Lm2;
hence thesis by NAT_1:13;
end;
suppose
A134: n1 = 1 & (vs.1 = T.(c.len c) & y9 = [0, c.len c] or
vs.1 = S.(c.len c) & y9 = [1, c.len c] & T.(c.len c) <> S.(c.len c)) & ex k
being Element of NAT st 1 <= k & n2 = k+1 & (vs.n2 = T.(c.k) & u9 = [0, c.k] or
vs.n2 = S.(c.k) & u9 = [1, c.k] & T.(c.k) <> S.(c.k));
A135: 1 <= len c by A106,A107,XXREAL_0:2;
consider k2 being Element of NAT such that
A136: 1 <= k2 and
A137: n2 = k2+1 and
vs.n2 = T.(c.k2) & u9 = [0, c.k2] or vs.n2 = S.(c.k2) & u9
= [1, c.k2] & T.(c.k2) <> S.(c.k2) by A134;
k2 <= n2 by A137,NAT_1:12;
then
A138: k2 <= len c by A107,XXREAL_0:2;
c.k2 = c.len c by A105,A117,A118,A134,A137,XTUPLE_0:1;
then len c + 1 <= len c by A107,A136,A137,A138,A135,Lm2;
hence thesis by NAT_1:13;
end;
suppose
n1 = 1 & (vs.1 = T.(c.len c) & y9 = [0, c.len c] or
vs.1 = S.(c.len c) & y9 = [1, c.len c] & T.(c.len c) <> S.(c.len c)) & n2 = 1 &
(vs.1 = T.(c.len c) & u9 = [0, c.len c] or vs.1 = S.(c.len c) & u9 = [1, c.len
c] & T.(c.len c) <> S.(c.len c));
hence thesis by A100,A102,A119,XTUPLE_0:1;
end;
end;
end;
suppose
A139: L[x9,y9,n1] & R[z9,u9,n2];
thus x = z
proof
per cases by A139;
suppose
ex k being Element of NAT st 1 <= k & n1 = k+1 & (vs
.n1 = T.(c.k) & y9 = [0, c.k] or vs.n1 = S.(c.k) & y9 = [1, c.k] & T.(c.k) <> S
.(c.k));
then consider k being Element of NAT such that
A140: 1 <= k and
A141: n1 = k+1 and
vs.n1 = T.(c.k) & y9 = [0, c.k] or vs.n1 = S.(c.k) & y9 =
[1, c.k ] & T.(c.k) <> S.(c.k);
k <= n1 by A141,NAT_1:12;
then
A142: k <= len c by A110,XXREAL_0:2;
c.n2 = c.k by A105,A117,A118,A139,A140,A141,XTUPLE_0:1;
then n2 = k by A106,A107,A140,A142,Lm2;
hence thesis by A1,A105,A117,A106,A107,A118,A139,A141,Lm3,
XTUPLE_0:1;
end;
suppose
A143: n1 = 1 & (vs.1 = T.(c.len c) & y9 = [0, c.len c] or
vs.1 = S.(c.len c) & y9 = [1, c.len c] & T.(c.len c) <> S.(c.len c));
A144: 1 <= len c by A109,A110,XXREAL_0:2;
c.n2 = c.len c by A105,A117,A118,A139,A143,XTUPLE_0:1;
then
A145: n2 = len c by A106,A107,A144,Lm2;
vs.n2 = T.(c.n2) & vs.(n2+1) = S.(c.n2) or vs.n2 = S.(c.
n2) & vs.(n2+1) = T.(c.n2) by A1,A106,A107,Lm3;
hence x = z by A1,A105,A117,A118,A139,A143,A145,MSSCYC_1:6
,XTUPLE_0:1;
end;
end;
end;
suppose
A146: R[x9,y9,n1] & L[z9,u9,n2];
thus x = z
proof
per cases by A146;
suppose
ex k being Element of NAT st 1 <= k & n2 = k+1 & (vs
.n2 = T.(c.k) & u9 = [0, c.k] or vs.n2 = S.(c.k) & u9 = [1, c.k] & T.(c.k) <> S
.(c.k));
then consider k being Element of NAT such that
A147: 1 <= k and
A148: n2 = k+1 and
vs.n2 = T.(c.k) & u9 = [0, c.k] or vs.n2 = S.(c.k) & u9 =
[1, c.k ] & T.(c.k) <> S.(c.k);
k <= n2 by A148,NAT_1:12;
then
A149: k <= len c by A107,XXREAL_0:2;
c.n1 = c.k by A105,A117,A118,A146,A147,A148,XTUPLE_0:1;
then n1 = k by A109,A110,A147,A149,Lm2;
hence thesis by A1,A105,A117,A109,A110,A118,A146,A148,Lm3,
XTUPLE_0:1;
end;
suppose
A150: n2 = 1 & (vs.1 = T.(c.len c) & u9 = [0, c.len c] or
vs.1 = S.(c.len c) & u9 = [1, c.len c] & T.(c.len c) <> S.(c.len c));
A151: 1 <= len c by A109,A110,XXREAL_0:2;
c.n1 = c.len c by A105,A117,A118,A146,A150,XTUPLE_0:1;
then
A152: n1 = len c by A109,A110,A151,Lm2;
vs.n1 = T.(c.n1) & vs.(n1+1) = S.(c.n1) or vs.n1 = S.(c.
n1) & vs.(n1+1) = T.(c.n1) by A1,A109,A110,Lm3;
hence x = z by A1,A105,A117,A118,A146,A150,A152,MSSCYC_1:6
,XTUPLE_0:1;
end;
end;
end;
suppose
A153: R[x9,y9,n1] & R[z9,u9,n2];
then c.n1 = c.n2 by A105,A117,A118,XTUPLE_0:1;
then n1 = n2 by A109,A110,A106,A107,Lm2;
hence thesis by A100,A102,A153,XTUPLE_0:1;
end;
end;
end;
end;
then ev92,evin \/ evout are_equipotent;
then card ev92 = card (evin \/ evout) by CARD_1:5
.= card evin + card evout by A9,CARD_2:40;
then Degree(v, rc) = card 2 * card ev by A7,A6,CARD_2:46
.= 2 * card ev;
hence thesis;
end;
end;
theorem Th49: :: CycVerDeg1
for c being cyclic Path of G holds Degree(v, rng c) is even
proof
let c be cyclic Path of G;
per cases;
suppose
c is empty;
then reconsider rc = rng c as empty set;
Degree(v, rc)= 2 * 0;
hence thesis;
end;
suppose
A1: c is non empty;
consider vs being FinSequence of the carrier of G such that
A2: vs is_vertex_seq_of c by GRAPH_2:33;
thus Degree(v, rng c) is even
proof
per cases;
suppose
v in rng vs;
hence thesis by A2,Lm4;
end;
suppose
not v in rng vs;
then Degree(v, rng c) = 2 * 0 by A1,A2,Th32;
hence thesis;
end;
end;
end;
end;
theorem Th50: :: CycVerDeg2
for c being Path of G st c is non cyclic & vs is_vertex_seq_of c
holds Degree(v, rng c) is even iff v <> vs.1 & v <> vs.len vs
proof
let c be Path of G such that
A1: c is non cyclic and
A2: vs is_vertex_seq_of c;
len vs = len c +1 by A2;
then
A3: 1 <= len vs by NAT_1:11;
then 1 in dom vs & len vs in dom vs by FINSEQ_3:25;
then reconsider v1 = vs.1, v2 = vs.len vs as Vertex of G by FINSEQ_2:11;
A4: v1 <> v2 by A1,A2;
set G9 = AddNewEdge(v1, v2);
reconsider vs9 = vs as FinSequence of the carrier of G9 by Def7;
reconsider c9 = c as Path of G9 by Th37;
A5: vs9 is_vertex_seq_of c9 by A2,Th36;
reconsider v9 = v, v19 = v1, v29 = v2 as Vertex of G9 by Def7;
set v219 = <*v29, v19*>;
set vs9e = vs9^'<*v29, v19*>;
len v219 = 2 by FINSEQ_1:44;
then
A6: vs9e.len vs9e = v219.2 by FINSEQ_6:142;
set E = the carrier' of G;
set e = E;
A7: e in {E} by TARSKI:def 1;
the carrier' of G9 = (the carrier' of G) \/ {E} by Def7;
then e in the carrier' of G9 by A7,XBOOLE_0:def 3;
then reconsider ep = <*e*> as Path of G9 by Th4;
A8: rng ep = {e} by FINSEQ_1:39;
A9: not e in e;
then rng ep misses E by A8,ZFMISC_1:50;
then
A10: rng ep /\ E = {};
(the Source of G9).e = v19 & (the Target of G9).e = v29 by Th34;
then
A11: vs9.len vs9 = <*v29,v19*>.1 & <*v29,v19*> is_vertex_seq_of ep by Th11;
A12: rng c c= the carrier' of G by FINSEQ_1:def 4;
then
A13: not e in rng c by A9;
rng c9 misses rng ep
proof
assume not thesis;
then ex x being object st x in rng c9 & x in rng ep by XBOOLE_0:3;
hence contradiction by A13,A8,TARSKI:def 1;
end;
then reconsider c9e = c9^ep as Path of G9 by A5,A11,Th6;
A14: vs9e is_vertex_seq_of c9e by A5,A11,GRAPH_2:44;
vs9e.1 = vs.1 by A3,FINSEQ_6:140;
then vs9e.1 = vs9e.len vs9e by A6;
then reconsider c9e as cyclic Path of G9 by A14,MSSCYC_1:def 2;
rng c9e = rng c \/ rng ep by FINSEQ_1:31;
then
A15: e in rng c9e by A7,A8,XBOOLE_0:def 3;
A16: rng c9e /\ E = (rng c \/ rng ep) /\ E by FINSEQ_1:31
.= (rng c /\ E) \/ {} by A10,XBOOLE_1:23
.= rng c by A12,XBOOLE_1:28;
then
A17: Degree(v, rng c9e) = Degree(v, rng c) by Th31;
reconsider dv9 = Degree(v9, rng c9e) as even Element of NAT by Th49;
A18: Degree(v9, rng c9e) is even by Th49;
per cases;
suppose
v <> v1 & v <> v2;
hence thesis by A18,A17,Th48;
end;
suppose
A19: v = v1 or v = v2;
then Degree(v9, rng c9e) = Degree(v, rng c9e) +1 by A4,A15,Th47;
then Degree(v, rng c9e) = dv9 -1;
hence thesis by A16,A19,Th31;
end;
end;
reserve G for Graph,
v for Vertex of G,
vs for FinSequence of the carrier of G;
definition
let G be Graph;
func G-CycleSet -> FinSequenceSet of the carrier' of G means
:Def8:
for x being set holds x in it iff x is cyclic Path of G;
existence
proof
defpred P[set] means $1 is cyclic Path of G;
set IT = { p where p is Element of (the carrier' of G)* : P[p]};
IT is Subset of (the carrier' of G)* from DOMAIN_1:sch 7;
then
for x being object st x in IT holds x is FinSequence of (the carrier' of
G) by FINSEQ_1:def 11;
then reconsider IT as FinSequenceSet of the carrier' of G by FINSEQ_2:def 3
;
reconsider p = {} as Path of G by GRAPH_1:14;
set v = the Vertex of G;
reconsider IT as FinSequenceSet of the carrier' of G;
take IT;
let x be set;
hereby
assume x in IT;
then ex p being Element of (the carrier' of G)* st p = x & p is cyclic
Path of G;
hence x is cyclic Path of G;
end;
assume
A1: x is cyclic Path of G;
then x is Element of (the carrier' of G)* by FINSEQ_1:def 11;
hence thesis by A1;
end;
uniqueness
proof
let it1, it2 be FinSequenceSet of the carrier' of G such that
A2: for x being set holds x in it1 iff x is cyclic Path of G and
A3: for x being set holds x in it2 iff x is cyclic Path of G;
now
let x be object;
x in it1 iff x is cyclic Path of G by A2;
hence x in it1 iff x in it2 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th51:
{} in G-CycleSet
proof
reconsider p = {} as Path of G by GRAPH_1:14;
set v = the Vertex of G;
<*v*> is_vertex_seq_of p & <*v*>.1 = <*v*>.len <*v*> by FINSEQ_1:40;
then p is cyclic;
hence thesis by Def8;
end;
registration let G be Graph;
cluster G-CycleSet -> non empty;
coherence by Th51;
end;
theorem Th52:
for c being Element of G-CycleSet st v in G-VSet rng c holds {
c9 where c9 is Element of G-CycleSet : rng c9 = rng c & ex vs st vs
is_vertex_seq_of c9 & vs.1 = v} is non empty Subset of G-CycleSet
proof
let c be Element of G-CycleSet;
set Cset = { c9 where c9 is Element of G-CycleSet : rng c9 = rng c & ex vs
being FinSequence of the carrier of G st vs is_vertex_seq_of c9 & vs.1 = v};
reconsider c9 = c as cyclic Path of G by Def8;
consider vs being FinSequence of the carrier of G such that
A1: vs is_vertex_seq_of c9 by GRAPH_2:33;
A2: len vs = len c +1 by A1;
assume
A3: v in G-VSet rng c;
then
A4: ex vv being Vertex of G st vv = v & ex e being Element of the carrier' of
G st e in rng c & (vv = (the Source of G).e or vv = (the Target of G).e);
then G-VSet rng c9 = rng vs by A1,GRAPH_2:31,RELAT_1:38;
then consider n being Nat such that
A5: n in dom vs and
A6: vs.n = v by A3,FINSEQ_2:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
dom vs = Seg len vs by FINSEQ_1:def 3;
then
A7: 1 <= n & n <= len vs by A5,FINSEQ_1:1;
A8: now
per cases by A7,XXREAL_0:1;
suppose
1 = n & n = len vs;
then 0+1 = len c +1 by A1;
then c = {};
hence Cset is non empty by A4;
end;
suppose
1 = n;
then c in Cset by A1,A6;
hence Cset is non empty;
end;
suppose
n = len vs;
then vs.1 = v by A1,A6,MSSCYC_1:6;
then c in Cset by A1;
hence Cset is non empty;
end;
suppose
A9: 1 < n & n < len vs;
set vs2 = (n, len vs)-cut vs;
consider m being Element of NAT such that
A10: n = 1+m and
A11: 1 <= m by A9,FINSEQ_4:84;
set vs1 = (1, m+1)-cut vs;
A12: 1 <= m+1+1 by A9,A10,NAT_1:13;
then
A13: len vs1 + 1 = m+1+1 by A9,A10,Lm1;
then
A14: vs1.1 = vs.(1+0) by A9,A10,A12,Lm1;
reconsider c1 = (1,m)-cut c9, c2 = (n,len c)-cut c9 as Path of G by Th5;
A15: n <= len c by A2,A9,NAT_1:13;
then
A16: vs2 is_vertex_seq_of c2 by A1,A9,GRAPH_2:42;
A17: len vs2 + n = len vs +1 by A9,FINSEQ_6:def 4;
A18: now
assume len vs2 = 0;
then len vs +1 < len vs +0 by A9,A17;
hence contradiction by XREAL_1:6;
end;
then
A19: 1+0 <= len vs2 by NAT_1:13;
then consider lv2 being Nat such that
0<=lv2 and
A20: lv2<len vs2 and
A21: len vs2=lv2+1 by FINSEQ_6:127;
reconsider vs21 = vs2^'vs1 as FinSequence of the carrier of G;
A22: vs21.1 = vs2.(0+1) by A19,FINSEQ_6:140
.= vs.(n+0) by A9,A18,FINSEQ_6:def 4;
A23: m <= m+1 by NAT_1:11;
then m <= len c by A10,A15,XXREAL_0:2;
then
A24: vs1 is_vertex_seq_of c1 by A1,A11,GRAPH_2:42;
A25: vs2.len vs2 = vs.(n+lv2) by A9,A20,A21,FINSEQ_6:def 4
.= vs1.1 by A1,A17,A21,A14,MSSCYC_1:6;
now
given y being object such that
A26: y in rng c1 and
A27: y in rng c2;
consider b being Nat such that
A28: b in dom c2 and
A29: c2.b = y by A27,FINSEQ_2:10;
A30: ex l being Nat st l in dom c9 & c.l = c2.b & l+1 = n+b
& n <= l & l <= len c by A28,Th2;
consider a being Nat such that
A31: a in dom c1 and
A32: c1.a = y by A26,FINSEQ_2:10;
consider k being Nat such that
A33: k in dom c9 & c.k = c1.a and
k+1 = 1+a and
1 <= k and
A34: k <= m by A31,Th2;
k < n by A10,A34,NAT_1:13;
hence contradiction by A32,A29,A33,A30,FUNCT_1:def 4;
end;
then rng c1 misses rng c2 by XBOOLE_0:3;
then reconsider c219= c2^c1 as Path of G by A24,A16,A25,Th6;
A35: vs21 is_vertex_seq_of c219 by A24,A16,A25,GRAPH_2:44;
A36: c = c1^c2 by A10,A15,A23,FINSEQ_6:135,XXREAL_0:2;
1 < len vs1 by A11,A13,NAT_1:13;
then vs21.len vs21 = vs1.len vs1 by FINSEQ_6:142
.= vs.n by A9,A10,FINSEQ_6:138;
then reconsider c219 as cyclic Path of G by A22,A35,MSSCYC_1:def 2;
reconsider c21 = c219 as Element of G-CycleSet by Def8;
rng c21 = rng c2 \/ rng c1 by FINSEQ_1:31
.= rng c by A36,FINSEQ_1:31;
then c21 in Cset by A6,A22,A35;
hence Cset is non empty;
end;
end;
Cset c= G-CycleSet
proof
let x be object;
assume x in Cset;
then ex c9 being Element of G-CycleSet st c9 = x & rng c9 = rng c & ex vs
being FinSequence of the carrier of G st vs is_vertex_seq_of c9 & vs.1 = v;
hence thesis;
end;
hence thesis by A8;
end;
definition
let G, v;
let c be Element of G-CycleSet;
assume
A1: v in G-VSet rng c;
func Rotate(c, v) -> Element of G-CycleSet equals
:Def9:
the Element of { c9 where
c9 is Element of G-CycleSet : rng c9 = rng c & ex vs st vs is_vertex_seq_of c9
& vs.1 = v };
coherence
proof
set Rotated = { c9 where c9 is Element of G-CycleSet : rng c9 = rng c & ex
vs being FinSequence of the carrier of G st vs is_vertex_seq_of c9 & vs.1 = v};
set IT = the Element of Rotated;
Rotated is non empty by A1,Th52;
then IT in Rotated;
then ex c9 being Element of G-CycleSet st IT = c9 & rng c9 = rng c & ex vs
being FinSequence of the carrier of G st vs is_vertex_seq_of c9 & vs.1 = v;
hence thesis;
end;
end;
Lm5: for G being Graph, c being Element of G-CycleSet, v being Vertex of G st
v in G-VSet rng c holds rng Rotate(c, v) = rng c
proof
let G be Graph, c be Element of G-CycleSet, v be Vertex of G;
assume
A1: v in G-VSet rng c;
then reconsider
Rotated = { c9 where c9 is Element of G-CycleSet : rng c9 = rng c
& ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c9 & vs.1
= v} as non empty Subset of G-CycleSet by Th52;
Rotate(c, v) = the Element of Rotated by A1,Def9;
then Rotate(c, v) in Rotated;
then
ex c9 being Element of G-CycleSet st Rotate(c, v) = c9 & rng c9 = rng c &
ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c9 & vs.1 =
v;
hence thesis;
end;
definition
let G be Graph, c1, c2 be Element of G-CycleSet;
assume that
A1: G-VSet rng c1 meets G-VSet rng c2 and
A2: rng c1 misses rng c2;
func CatCycles(c1, c2) -> Element of G-CycleSet means
:Def10:
ex v being
Vertex of G st v = the Element of (G-VSet rng c1) /\ (G-VSet rng c2) &
it = Rotate(c1
, v)^Rotate(c2, v);
existence
proof
set v = the Element of (G-VSet rng c1) /\ (G-VSet rng c2);
A3: (G-VSet rng c1) /\ (G-VSet rng c2) is non empty by A1;
then
A4: v in (G-VSet rng c1) /\ (G-VSet rng c2);
A5: v in (G-VSet rng c1) by A3,XBOOLE_0:def 4;
A6: v in (G-VSet rng c2) by A3,XBOOLE_0:def 4;
reconsider v as Vertex of G by A4;
reconsider Rotated2 = { c9 where c9 is Element of G-CycleSet : rng c9 =
rng c2 & ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c9
& vs.1 = v} as non empty Subset of G-CycleSet by A6,Th52;
set r2 = Rotate(c2, v);
r2 = the Element of Rotated2 by A6,Def9;
then r2 in Rotated2;
then consider c99 being Element of G-CycleSet such that
A7: r2 = c99 and
A8: rng c99 = rng c2 and
A9: ex vs being FinSequence of the carrier of G st vs
is_vertex_seq_of c99 & vs.1 = v;
consider vs2 being FinSequence of the carrier of G such that
A10: vs2 is_vertex_seq_of c99 and
A11: vs2.1 = v by A9;
reconsider c92 = c99 as cyclic Path of G by Def8;
A12: r2 = c92 by A7;
rng c2 is non empty by A6,Th16;
then c99 is non empty by A8;
then 0+1 < len c99 +1 by XREAL_1:6;
then
A13: 1 < len vs2 by A10;
A14: vs2 is_vertex_seq_of c92 by A10;
reconsider Rotated1 = { c9 where c9 is Element of G-CycleSet : rng c9 =
rng c1 & ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c9
& vs.1 = v} as non empty Subset of G-CycleSet by A5,Th52;
set r1 = Rotate(c1, v);
r1 = the Element of Rotated1 by A5,Def9;
then r1 in Rotated1;
then consider c9 being Element of G-CycleSet such that
A15: r1 = c9 and
A16: rng c9 = rng c1 and
A17: ex vs being FinSequence of the carrier of G st vs
is_vertex_seq_of c9 & vs.1 = v;
reconsider c91 = c9 as cyclic Path of G by Def8;
consider vs1 being FinSequence of the carrier of G such that
A18: vs1 is_vertex_seq_of c9 and
A19: vs1.1 = v by A17;
vs1 is_vertex_seq_of c91 by A18;
then
A20: vs1.1 = vs1.len vs1 by MSSCYC_1:6;
set vs12 = vs1^'vs2;
len vs1 = len c9 +1 by A18;
then 1 <= len vs1 by NAT_1:11;
then
A21: vs12.1 = vs1.1 by FINSEQ_6:140
.= vs2.len vs2 by A19,A11,A14,MSSCYC_1:6
.= vs12.len vs12 by A13,FINSEQ_6:142;
A22: r1 = c91 by A15;
then reconsider c = r1^r2 as Path of G by A2,A16,A8,A18,A19,A10,A11,A20,A12
,Th6;
vs12 is_vertex_seq_of c by A18,A19,A10,A11,A20,A22,A12,GRAPH_2:44;
then c is cyclic by A21;
then reconsider c as Element of G-CycleSet by Def8;
take c;
take v;
thus thesis;
end;
correctness;
end;
theorem Th53:
for G being Graph, c1, c2 be Element of G-CycleSet st G-VSet rng
c1 meets G-VSet rng c2 & rng c1 misses rng c2 & (c1 <> {} or c2 <> {}) holds
CatCycles(c1, c2) is non empty
proof
let G be Graph, c1, c2 be Element of G-CycleSet;
assume that
A1: G-VSet rng c1 meets G-VSet rng c2 and
A2: rng c1 misses rng c2 and
A3: c1 <> {} or c2 <> {};
consider v being Vertex of G such that
A4: v = the Element of (G-VSet rng c1) /\ (G-VSet rng c2) and
A5: CatCycles(c1, c2) = Rotate(c1, v)^Rotate(c2, v) by A1,A2,Def10;
A6: (G-VSet rng c1) /\ (G-VSet rng c2) <> {} by A1;
then
A7: v in (G-VSet rng c1) by A4,XBOOLE_0:def 4;
A8: v in (G-VSet rng c2) by A4,A6,XBOOLE_0:def 4;
per cases by A3;
suppose
c1 <> {};
then rng Rotate(c1, v) <> {} by A7,Lm5;
hence thesis by A5,FINSEQ_1:35,RELAT_1:38;
end;
suppose
c2 <> {};
then rng Rotate(c2, v) <> {} by A8,Lm5;
hence thesis by A5,FINSEQ_1:35,RELAT_1:38;
end;
end;
reserve G for finite Graph,
v for Vertex of G,
vs for FinSequence of the carrier of G;
definition
let G, v;
let X be set;
assume
A1: Degree(v, X) <> 0;
func X-PathSet v -> non empty FinSequenceSet of the carrier' of G equals
:Def11:
{
c where c is Element of X* : c is Path of G & c is non empty & ex vs st vs
is_vertex_seq_of c & vs.1 = v };
coherence
proof
set e = the Element of Edges_At(v, X);
set IT = { c where c is Element of X* : c is Path of G & c is non empty &
ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c & vs.1 = v
};
A2: now
let x be object;
assume x in IT;
then ex c being Element of X* st x = c & c is Path of G & c is non empty
& ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c & vs.1 =
v;
hence x is FinSequence of the carrier' of G;
end;
A3: Edges_At(v, X) is not empty by A1,Th25;
now
per cases by A3,XBOOLE_0:def 3;
suppose
A4: e in Edges_In(v, X);
then e in X & (the Target of G).e = v by Def1;
hence
ex e9 being Element of X st e = e9 & e9 in X & e9 in the carrier'
of G & (v = (the Target of G).e9 or v = (the Source of G).e9) by A4;
end;
suppose
A5: e in Edges_Out(v, X);
then e in X & (the Source of G).e = v by Def2;
hence
ex e9 being Element of X st e = e9 & e9 in X & e9 in the carrier'
of G & (v = (the Target of G).e9 or v = (the Source of G).e9) by A5;
end;
end;
then consider e9 being Element of X such that
e = e9 and
A6: e9 in X and
A7: e9 in the carrier' of G and
A8: v = (the Target of G).e9 or v = (the Source of G).e9;
reconsider X9 = X as non empty set by A6;
reconsider e9 as Element of X9;
reconsider c = <*e9*> as Element of X* by FINSEQ_1:def 11;
A9: ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c
& vs.1 = v
proof
set s = (the Source of G).e9;
reconsider s as Vertex of G by A7,FUNCT_2:5;
set t = (the Target of G).e9;
reconsider t as Vertex of G by A7,FUNCT_2:5;
per cases by A8;
suppose
A10: v = (the Target of G).e9;
take <*t, s*>;
thus thesis by A10,Th11;
end;
suppose
A11: v = (the Source of G).e9;
take <*s, t*>;
thus thesis by A11,MSSCYC_1:4;
end;
end;
c is Path of G by A7,Th4;
then c in IT by A9;
hence thesis by A2,FINSEQ_2:def 3;
end;
end;
theorem Th54:
for p being Element of X-PathSet v, Y being finite set st Y =
the carrier' of G & Degree(v, X) <> 0 holds len p <= card Y
proof
let p be Element of X-PathSet v, Y be finite set;
assume that
A1: Y = the carrier' of G and
A2: Degree(v, X) <> 0;
A3: p in X-PathSet v;
X-PathSet v = { c where c is Element of X* : c is Path of G & c is non
empty & ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c &
vs.1 = v } by A2,Def11;
then
ex c being Element of X* st p = c & c is Path of G & c is non empty & ex
vs being FinSequence of the carrier of G st vs is_vertex_seq_of c & vs.1 = v
by A3;
then
A4: card (rng p) = len p by FINSEQ_4:62;
rng p c= Y by A1,FINSEQ_1:def 4;
hence thesis by A4,NAT_1:43;
end;
definition
let G, v;
let X be set;
assume that
A1: for v being Vertex of G holds Degree(v, X) is even and
A2: Degree(v, X) <> 0;
func X-CycleSet v -> non empty Subset of G-CycleSet equals
:Def12:
{ c where
c is Element of G-CycleSet : rng c c= X & c is non empty & ex vs st vs
is_vertex_seq_of c & vs.1 = v };
coherence
proof
reconsider E = the carrier' of G as finite set by GRAPH_1:def 11;
set XL = the set of all len p where p is Element of X-PathSet v ;
set IT = { c where c is Element of G-CycleSet : rng c c= X & c is non
empty & ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c &
vs.1 = v };
set p = the Element of X-PathSet v;
A3: len p in XL;
A4: XL c= NAT
proof
let x be object;
assume x in XL;
then ex p being Element of X-PathSet v st x = len p;
hence thesis;
end;
A5: X-PathSet v = { c where c is Element of X* : c is Path of G & c is non
empty & ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c &
vs.1 = v } by A2,Def11;
XL c= Seg card E
proof
let x be object;
assume x in XL;
then consider p being Element of X-PathSet v such that
A6: x = len p;
p in X-PathSet v;
then
ex c being Element of X* st p = c & c is Path of G & c is non empty &
ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c & vs.1 = v
by A5;
then
A7: 0+1 <= len p by NAT_1:13;
len p <= card E by A2,Th54;
hence thesis by A6,A7,FINSEQ_1:1;
end;
then reconsider XL as finite non empty Subset of NAT by A3,A4;
set maxl = max XL;
maxl in XL by XXREAL_2:def 8;
then consider p being Element of X-PathSet v such that
A8: maxl = len p;
p in X-PathSet v;
then consider c being Element of X* such that
A9: p = c and
A10: c is Path of G and
A11: c is non empty and
A12: ex vs being FinSequence of the carrier of G st vs
is_vertex_seq_of c & vs.1 = v by A5;
reconsider p as Path of G by A9,A10;
A13: rng c c= X by FINSEQ_1:def 4;
now
set T = the Target of G;
set S = the Source of G;
A14: rng p c= X by A9,FINSEQ_1:def 4;
consider vs being FinSequence of the carrier of G such that
A15: vs is_vertex_seq_of p and
A16: vs.1 = v by A9,A12;
len vs = len p +1 by A15;
then
A17: 1 <= len vs by NAT_1:11;
then len vs in dom vs by FINSEQ_3:25;
then reconsider v1 = vs.len vs as Vertex of G by FINSEQ_2:11;
assume not p is cyclic;
then
A18: Degree(v1, rng p) is odd by A15,Th50;
then rng p <> X by A1;
then rng p c< X by A14;
then ex xx being object st xx in X & not xx in rng p by XBOOLE_0:6;
then reconsider Xp = X \ rng p as non empty set by XBOOLE_0:def 5;
set e = the Element of Edges_At(v1, Xp);
Degree(v1, Xp) = Degree(v1, X) - Degree(v1, rng p) by A14,Th29;
then Degree(v1, Xp) <> 0 by A1,A18;
then
A19: Edges_At(v1, Xp) is not empty by Th25;
A20: now
per cases by A19,XBOOLE_0:def 3;
suppose
A21: e in Edges_In(v1, Xp);
then e in Xp & (the Target of G).e = v1 by Def1;
hence ex e9 being Element of Xp st e = e9 & e9 in Xp & e9 in the
carrier' of G & (v1 = (the Target of G).e9 or v1 = (the Source of G).e9) by A21
;
end;
suppose
A22: e in Edges_Out(v1, Xp);
then e in Xp & (the Source of G).e = v1 by Def2;
hence ex e9 being Element of Xp st e = e9 & e9 in Xp & e9 in the
carrier' of G & (v1 = (the Target of G).e9 or v1 = (the Source of G).e9) by A22
;
end;
end;
then reconsider ep = <*e*> as Path of G by Th4;
reconsider t = T.e,s = S.e as Vertex of G by A20,FUNCT_2:5;
now
given x being object such that
A23: x in rng ep and
A24: x in rng p;
rng ep = {e} by FINSEQ_1:38;
then x in Xp by A20,A23,TARSKI:def 1;
hence contradiction by A24,XBOOLE_0:def 5;
end;
then
A25: rng ep misses rng p by XBOOLE_0:3;
per cases by A20;
suppose
A26: v1 = T.e;
reconsider ts = <*t,s*> as FinSequence of the carrier of G;
A27: vs.len vs = ts.1 by A26;
reconsider X9 = X as non empty set by A20;
reconsider vs1 = vs^'ts as FinSequence of the carrier of G;
reconsider e9 = e as Element of X9 by A20;
A28: vs1.1 = v by A16,A17,FINSEQ_6:140;
A29: ts is_vertex_seq_of ep by Th11;
then reconsider p1 = p^ep as Path of G by A15,A25,A27,Th6;
A30: len p1 = len p + len ep by FINSEQ_1:22
.= len p +1 by FINSEQ_1:39;
reconsider p as FinSequence of X by A9;
reconsider ep = <*e9*> as FinSequence of X;
reconsider xp1 = p^ep as Element of X* by FINSEQ_1:def 11;
vs1 is_vertex_seq_of p1 by A15,A29,A27,GRAPH_2:44;
then xp1 in X-PathSet v by A5,A28;
then reconsider xp1 as Element of X-PathSet v;
len xp1 in XL;
then len p +1 <= len p +0 by A8,A30,XXREAL_2:def 8;
hence contradiction by XREAL_1:6;
end;
suppose
A31: v1 = S.e;
reconsider ts = <*s,t*> as FinSequence of the carrier of G;
A32: ts is_vertex_seq_of ep & vs.len vs = ts.1 by A31,MSSCYC_1:4
;
then reconsider p1 = p^ep as Path of G by A15,A25,Th6;
A33: len p1 = len p + len ep by FINSEQ_1:22
.= len p +1 by FINSEQ_1:39;
reconsider X9 = X as non empty set by A20;
reconsider vs1 = vs^'ts as FinSequence of the carrier of G;
reconsider e9 = e as Element of X9 by A20;
A34: vs1.1 = v by A16,A17,FINSEQ_6:140;
reconsider p as FinSequence of X by A9;
reconsider ep = <*e9*> as FinSequence of X;
reconsider xp1 = p^ep as Element of X* by FINSEQ_1:def 11;
vs1 is_vertex_seq_of p1 by A15,A32,GRAPH_2:44;
then xp1 in X-PathSet v by A5,A34;
then reconsider xp1 as Element of X-PathSet v;
len xp1 in XL;
then len p +1 <= len p +0 by A8,A33,XXREAL_2:def 8;
hence contradiction by XREAL_1:6;
end;
end;
then reconsider c as Element of G-CycleSet by A9,Def8;
A35: now
let c be object;
assume c in IT;
then ex c9 being Element of G-CycleSet st c = c9 & rng c9 c= X & c9 is
non empty & ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of
c9 & vs.1 = v;
hence c in G-CycleSet;
end;
c in IT by A11,A12,A13;
hence thesis by A35,TARSKI:def 3;
end;
end;
theorem Th55:
Degree(v, X) <> 0 & (for v holds Degree(v, X) is even) implies
for c being Element of X-CycleSet v holds c is non empty & rng c c= X & v in G
-VSet rng c
proof
assume Degree(v, X) <> 0 & for v holds Degree(v, X) is even;
then
A1: X-CycleSet v = { c9 where c9 is Element of G-CycleSet : rng c9 c= X & c9
is non empty & ex vs being FinSequence of the carrier of G st vs
is_vertex_seq_of c9 & vs.1 = v} by Def12;
let c be Element of X-CycleSet v;
c in X-CycleSet v;
then consider c9 being Element of G-CycleSet such that
A2: c = c9 and
A3: rng c9 c= X and
A4: c9 is non empty and
A5: ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of
c9 & vs.1 = v by A1;
thus c is non empty by A2,A4;
thus rng c c= X by A2,A3;
reconsider c9 as Path of G by Def8;
consider vs being FinSequence of the carrier of G such that
A6: vs is_vertex_seq_of c9 and
A7: vs.1 = v by A5;
len vs = len c9 +1 by A6;
then 1 <= len vs by NAT_1:11;
then
A8: 1 in dom vs by FINSEQ_3:25;
G-VSet rng c9 = rng vs by A4,A6,GRAPH_2:31;
hence thesis by A2,A7,A8,FUNCT_1:def 3;
end;
theorem Th56:
for G be finite connected Graph, c be Element of G-CycleSet st
rng c <> the carrier' of G & c is non empty holds {v9 where v9 is Vertex of G :
v9 in G-VSet rng c & Degree v9 <> Degree(v9, rng c)} is non empty Subset of the
carrier of G
proof
let G be finite connected Graph, c be Element of G-CycleSet;
defpred P[Vertex of G] means $1 in G-VSet rng c & Degree $1 <> Degree($1,
rng c);
set X = {v9 where v9 is Vertex of G : P[v9]};
set T = the Target of G;
set S = the Source of G;
set E = the carrier' of G;
A1: rng c c= E by FINSEQ_1:def 4;
reconsider cp = c as cyclic Path of G by Def8;
assume that
A2: rng c <> the carrier' of G and
A3: c is non empty;
consider vs being FinSequence of the carrier of G such that
A4: vs is_vertex_seq_of cp by GRAPH_2:33;
A5: G-VSet rng cp = rng vs by A3,A4,GRAPH_2:31;
now
consider x being object such that
A6: not (x in rng c iff x in E) by A2,TARSKI:2;
reconsider x as Element of E by A1,A6;
reconsider v = (the Target of G).x as Vertex of G by A1,A6,FUNCT_2:5;
per cases;
suppose
A7: v in rng vs;
Degree v <> Degree(v, rng c) by A1,A6,Th26;
hence
ex v being Vertex of G st v in rng vs & Degree v <> Degree(v, rng c
) by A7;
end;
suppose
A8: not v in rng vs;
A9: ex e being object st e in rng c by A3,XBOOLE_0:def 1;
then rng c meets E by A1,XBOOLE_0:3;
then consider v9 being Vertex of G, e being Element of E such that
A10: v9 in rng vs and
A11: ( not e in rng c)&( v9 = T.e or v9 = S.e) by A5,A8,Th19;
Degree v9 <> Degree(v9, rng c) by A1,A9,A11,Th26;
hence
ex v being Vertex of G st v in rng vs & Degree v <> Degree(v, rng c
) by A10;
end;
end;
then consider v being Vertex of G such that
A12: v in rng vs & Degree v <> Degree(v, rng c);
A13: X is Subset of the carrier of G from DOMAIN_1:sch 7;
v in X by A5,A12;
hence thesis by A13;
end;
definition
let G be finite connected Graph, c be Element of G-CycleSet;
assume that
A1: rng c <> the carrier' of G and
A2: c is non empty;
func ExtendCycle c -> Element of G-CycleSet means
:Def13:
ex c9 being
Element of G-CycleSet, v being Vertex of G st
v = the Element of {v9 where v9 is Vertex
of G : v9 in G-VSet rng c & Degree v9 <> Degree(v9, rng c)} & c9
= the Element of ((
the carrier' of G) \ rng c)-CycleSet v & it = CatCycles(c, c9);
existence
proof
set X = {v9 where v9 is Vertex of G : v9 in G-VSet rng c & Degree v9 <>
Degree(v9, rng c)};
set v = the Element of X;
X is non empty by A1,A2,Th56;
then v in X;
then ex v9 being Vertex of G st v= v9 & v9 in G-VSet rng c & Degree v9 <>
Degree(v9, rng c);
then reconsider v as Vertex of G;
set E = the carrier' of G;
reconsider E9 = E as finite set by GRAPH_1:def 11;
rng c c= E by FINSEQ_1:def 4;
then rng c c< E by A1;
then ex xx being object st xx in E & not xx in rng c by XBOOLE_0:6;
then reconsider Erc = E9 \ rng c as finite non empty set by XBOOLE_0:def 5;
set c9 = the Element of Erc-CycleSet v;
c9 in Erc-CycleSet v;
then reconsider c9 as Element of G-CycleSet;
reconsider IT = CatCycles(c, c9) as Element of G-CycleSet;
take IT;
take c9;
take v;
thus thesis;
end;
uniqueness;
end;
theorem Th57:
for G being finite connected Graph, c being Element of G
-CycleSet st rng c <> the carrier' of G & c is non empty & for v being Vertex
of G holds Degree v is even holds ExtendCycle c is non empty & card rng c <
card rng ExtendCycle c
proof
let G be finite connected Graph, c be Element of G-CycleSet;
set E = the carrier' of G;
reconsider E9 = E as finite set by GRAPH_1:def 11;
reconsider ccp = c as cyclic Path of G by Def8;
assume that
A1: rng c <> the carrier' of G and
A2: c is non empty and
A3: for v being Vertex of G holds Degree v is even;
A4: rng c c= E by FINSEQ_1:def 4;
then rng c c< the carrier' of G by A1;
then ex xx being object st xx in E & not xx in rng c by XBOOLE_0:6;
then reconsider Erc = E9 \ rng c as finite non empty set by XBOOLE_0:def 5;
reconsider X = {v9 where v9 is Vertex of G : v9 in G-VSet rng c & Degree v9
<> Degree(v9, rng c)} as non empty set by A1,A2,Th56;
consider c9 being Element of G-CycleSet, v being Vertex of G such that
A5: v = the Element of X and
A6: c9 = the Element of Erc-CycleSet v and
A7: ExtendCycle c = CatCycles(c, c9) by A1,A2,Def13;
v in X by A5;
then
A8: ex v9 being Vertex of G st v = v9 & v9 in G-VSet rng c & Degree v9 <>
Degree(v9, rng c);
A9: now
let v be Vertex of G;
A10: Degree v = Degree(v, E) & Degree v is even by A3,Th24;
Degree(v, Erc) = Degree(v, E9) - Degree(v, rng c) & Degree(v, rng ccp
) is even by A4,Th29,Th49;
hence Degree(v, Erc) is even by A10;
end;
rng c misses (E\rng c) by XBOOLE_1:79;
then
A11: rng c /\ (E\rng c) = {};
Degree(v, Erc) = Degree(v, E9) - Degree(v, rng c) by A4,Th29;
then
A12: Degree(v, Erc) <> 0 by A8,Th24;
then rng c9 c= E \ rng c by A6,A9,Th55;
then rng c /\ rng c9 = rng c /\ ((E\rng c) /\ rng c9) by XBOOLE_1:28
.= {} /\ rng c9 by A11,XBOOLE_1:16
.= {};
then
A13: rng c misses rng c9;
v in G-VSet rng c9 by A6,A9,A12,Th55;
then
A14: G-VSet rng c meets G-VSet rng c9 by A8,XBOOLE_0:3;
hence ExtendCycle c is non empty by A2,A7,A13,Th53;
consider vr being Vertex of G such that
A15: vr = the Element of (G-VSet rng c) /\ (G-VSet rng c9) and
A16: CatCycles(c, c9) = Rotate(c, vr)^Rotate(c9, vr) by A14,A13,Def10;
A17: (G-VSet rng c) /\ (G-VSet rng c9) <> {} by A14;
then vr in G-VSet rng c9 by A15,XBOOLE_0:def 4;
then
A18: rng Rotate(c9, vr) = rng c9 by Lm5;
vr in G-VSet rng c by A17,A15,XBOOLE_0:def 4;
then rng Rotate(c, vr) = rng c by Lm5;
then rng ExtendCycle c = rng c \/ rng c9 by A7,A16,A18,FINSEQ_1:31;
then
A19: card rng ExtendCycle c = card rng c + card rng c9 by A13,CARD_2:40;
c9 is non empty by A6,A9,A12,Th55;
hence thesis by A19,XREAL_1:29;
end;
begin :: Euler paths
definition
let G be Graph;
let p be Path of G;
attr p is Eulerian means
rng p = the carrier' of G;
end;
theorem Th58:
for G being connected Graph, p being Path of G, vs being
FinSequence of the carrier of G st p is Eulerian & vs is_vertex_seq_of p holds
rng vs = the carrier of G
proof
let G be connected Graph, p be Path of G, vs be FinSequence of the carrier
of G such that
A1: p is Eulerian and
A2: vs is_vertex_seq_of p and
A3: rng vs <> the carrier of G;
consider x being object such that
A4: x in rng vs & not x in the carrier of G or x in the carrier of G &
not x in rng vs by A3,TARSKI:2;
vs <> {} by A2;
then consider y being object such that
A5: y in rng vs by XBOOLE_0:def 1;
A6: rng vs c= the carrier of G by FINSEQ_1:def 4;
then consider
c being Chain of G, vs1 being FinSequence of the carrier of G such
that
A7: c is non empty and
A8: vs1 is_vertex_seq_of c & vs1.1 = x and
vs1.len vs1 = y by A4,A5,Th18;
A9: 1 <= len c by A7,NAT_1:14;
A10: rng p = the carrier' of G by A1;
reconsider c as FinSequence of the carrier' of G by MSSCYC_1:def 1;
1 in dom c by A9,FINSEQ_3:25;
then c.1 in the carrier' of G by PARTFUN1:4;
then (the Target of G).(c.1) in rng vs & (the Source of G).(c.1) in rng vs
by A2,A10,Th15;
hence contradiction by A6,A4,A8,A9,Lm3;
end;
theorem Th59: :: Cyclic Euler paths
for G being finite connected Graph holds (ex p being cyclic Path
of G st p is Eulerian) iff for v being Vertex of G holds Degree v is even
proof
let G be finite connected Graph;
set E = the carrier' of G;
hereby
given c being cyclic Path of G such that
A1: c is Eulerian;
let v be Vertex of G;
consider vs being FinSequence of the carrier of G such that
A2: vs is_vertex_seq_of c and
vs.1 = vs.(len vs) by MSSCYC_1:def 2;
rng vs = the carrier of G by A1,A2,Th58;
then
A3: Degree(v, rng c) is even by A2,Lm4;
rng c = the carrier' of G by A1;
hence Degree v is even by A3,Th24;
end;
assume
A4: for v being Vertex of G holds Degree v is even;
per cases;
suppose
A5: G is void;
{} is Element of G-CycleSet by Th51;
then reconsider ec = {} as cyclic Path of G by Def8;
take ec;
the carrier' of G is empty by A5;
hence rng ec = the carrier' of G;
end;
suppose
G is non void;
then reconsider G9 = G as non void finite connected Graph;
reconsider V = the Element of the carrier of G as Vertex of G9;
defpred P[Nat,set,set] means
ex E being Element of G9-CycleSet st E = $2 & $3 = ExtendCycle E;
the Element of E-CycleSet V in E-CycleSet V;
then reconsider ec = the Element of E-CycleSet V
as Element of G9-CycleSet;
A6: for n being Nat for x being Element of G9-CycleSet
ex y being Element of G9-CycleSet st P[n,x,y]
proof
let n;
let x be Element of G9-CycleSet;
take ExtendCycle x;
thus thesis;
end;
consider f being sequence of G9-CycleSet such that
A7: f.0 = ec & for n being Nat holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A6);
A8: now
let v be Vertex of G;
Degree v = Degree(v, E) by Th24;
hence Degree(v, E) is even by A4;
end;
Degree V = Degree(V, E) by Th24;
then
A9: Degree(V, E) <> 0 by Th33;
now
defpred P[Nat] means ex c being Element of G9-CycleSet st c
is non empty & c = f.$1 & $1 <= card rng c;
reconsider E as finite set by GRAPH_1:def 11;
assume
A10: not ex n being Nat, c being Element of G9-CycleSet
st c = f.n & rng c = the carrier' of G;
A11: for n st P[n] holds P[n+1]
proof
let n be Nat;
given c being Element of G9-CycleSet such that
A12: c is non empty and
A13: c = f.n and
A14: n <= card rng c;
reconsider r = ExtendCycle c as Element of G9-CycleSet;
take r;
rng c <> E by A10,A13;
hence r is non empty by A4,A12,Th57;
P[n,f.n,f.(n+1)] by A7;
hence r = f.(n+1) by A13;
rng c <> E by A10,A13;
then n < card rng r by A4,A12,A14,Th57,XXREAL_0:2;
hence thesis by NAT_1:13;
end;
A15: P[0]
proof
take ec;
thus ec is non empty by A8,A9,Th55;
thus ec = f.0 by A7;
thus thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A15, A11);
then consider c being Element of G-CycleSet such that
c is non empty and
c = f.(card E + 1) and
A16: card E + 1 <= card rng c;
rng c c= E by FINSEQ_1:def 4;
then card rng c <= card E by NAT_1:43;
then card E + 1 <= card E + 0 by A16,XXREAL_0:2;
hence contradiction by XREAL_1:6;
end;
then consider n being Nat, c being Element of G-CycleSet such that
c = f.n and
A17: rng c = the carrier' of G;
reconsider c as cyclic Path of G by Def8;
take c;
thus rng c = the carrier' of G by A17;
end;
end;
theorem :: Non-cyclic Euler paths
for G being finite connected Graph holds (ex p being Path of G st p is
non cyclic & p is Eulerian) iff ex v1, v2 being Vertex of G st v1 <> v2 & for v
being Vertex of G holds Degree v is even iff v<>v1 & v <> v2
proof
let G be finite connected Graph;
set V = the carrier of G, E = the carrier' of G;
A1: now
assume {E} meets E;
then consider x being object such that
A2: x in {E} and
A3: x in E by XBOOLE_0:3;
A: x = E by A2,TARSKI:def 1;
reconsider xx = x as set by TARSKI:1;
not xx in xx;
hence contradiction by A,A3;
end;
hereby
given p being Path of G such that
A4: p is non cyclic and
A5: p is Eulerian;
consider vs being FinSequence of the carrier of G such that
A6: vs is_vertex_seq_of p by GRAPH_2:33;
len vs = len p +1 by A6;
then 1 <= len vs by NAT_1:11;
then 1 in dom vs & len vs in dom vs by FINSEQ_3:25;
then reconsider v1 = vs.1, v2 = vs.len vs as Vertex of G by FINSEQ_2:11;
take v1, v2;
thus v1 <> v2 by A4,A6;
let v be Vertex of G;
Degree v = Degree(v, the carrier' of G) by Th24
.= Degree(v, rng p) by A5;
hence Degree v is even iff v<>v1 & v <> v2 by A4,A6,Th50;
end;
given v1, v2 being Vertex of G such that
A7: v1 <> v2 and
A8: for v being Vertex of G holds Degree v is even iff v<>v1 & v <> v2;
set G9 = AddNewEdge(v1, v2);
set E9 = the carrier' of G9;
A9: the carrier' of G9 = (the carrier' of G) \/ {E} by Def7;
E in {E} by TARSKI:def 1;
then
A10: E in the carrier' of G9 by A9,XBOOLE_0:def 3;
A11: E = E9/\E by A9,XBOOLE_1:21;
for v being Vertex of G9 holds Degree v is even
proof
let v9 be Vertex of G9;
reconsider v = v9 as Vertex of G by Def7;
A12: Degree v9 = Degree(v9, E9) by Th24;
A13: Degree(v, E9) = Degree(v, E) by A11,Th31;
per cases;
suppose
A14: v9 <> v1 & v9 <> v2;
then Degree v9 = Degree(v, E9) by A12,Th48
.= Degree v by A13,Th24;
hence thesis by A8,A14;
end;
suppose
A15: v = v1 or v = v2;
then reconsider dv = Degree v as odd Element of NAT by A8;
A16: dv +1 is even;
Degree v9 = Degree(v, E9) +1 by A7,A10,A12,A15,Th47
.= Degree v +1 by A13,Th24;
hence thesis by A16;
end;
end;
then consider P9 being cyclic Path of G9 such that
A17: P9 is Eulerian by Th59;
A18: rng P9 = the carrier' of G9 by A17;
then consider n being Nat such that
A19: n in dom P9 and
A20: P9.n = E by A10,FINSEQ_2:10;
consider p9 being cyclic Path of G9 such that
A21: p9.1 = P9.n and
A22: len p9 = len P9 and
A23: rng p9 = rng P9 by A19,Th10;
reconsider p = (1+1, len p9)-cut p9 as Path of G9 by Th5;
consider vs9 being FinSequence of the carrier of G9 such that
A24: vs9 is_vertex_seq_of p9 by GRAPH_2:33;
A25: now
assume E in rng p;
then consider a being Nat such that
A26: a in dom p and
A27: p.a = E by FINSEQ_2:10;
consider k being Nat such that
A28: k in dom p9 and
A29: p9.k = p.a and
k+1 = 1+1+a and
A30: 1+1 <= k and
k <= len p9 by A26,Th2;
1 in dom p9 by A28,FINSEQ_5:6,RELAT_1:38;
then k = 1 by A20,A21,A27,A28,A29,FUNCT_1:def 4;
hence contradiction by A30;
end;
A31: 1 <= n & n <= len P9 by A19,FINSEQ_3:25;
then
A32: 1 <= len P9 by XXREAL_0:2;
then reconsider p1 = (1,1)-cut p9 as Chain of G9 by A22,GRAPH_2:41;
A33: p9 = p1 ^ (1+1, len p9)-cut p9 by A31,A22,FINSEQ_6:135,XXREAL_0:2;
reconsider vs = (1+1, len vs9)-cut vs9 as FinSequence of the carrier of G9;
A34: len vs9 = len p9 +1 by A24;
now
consider c being Chain of G, vs being FinSequence of V such that
A35: c is non empty and
vs is_vertex_seq_of c and
vs.1 = v1 and
vs.len vs = v2 by A7,Th18;
reconsider c as FinSequence of the carrier' of G by MSSCYC_1:def 1;
1 in dom c by A35,FINSEQ_5:6;
then
A36: rng c c= E & c.1 in rng c by FINSEQ_1:def 4,FUNCT_1:def 3;
then
A37: c.1 in E;
c.1 in the carrier' of G9 by A9,A36,XBOOLE_0:def 3;
then consider m being Nat such that
A38: m in dom P9 and
A39: P9.m = c.1 by A18,FINSEQ_2:10;
assume
A40: len P9 = 1;
1 <= m & m <= len P9 by A38,FINSEQ_3:25;
then
A41: m =1 by A40,XXREAL_0:1;
n = 1 by A31,A40,XXREAL_0:1;
hence contradiction by A20,A37,A39,A41;
end;
then 1 < len P9 by A32,XXREAL_0:1;
then
A42: 1+1 <= len P9 by NAT_1:13;
then
A43: vs is_vertex_seq_of p by A22,A24,GRAPH_2:42;
reconsider vs as FinSequence of the carrier of G by Def7;
reconsider p as Path of G by A25,Th45;
take p;
A44: (the Source of G9).E = v1 & (the Target of G9).E = v2 by Th34;
now
1+1<=len p9 +1 by A42,A22,NAT_1:12;
then
A45: 1+1<=len vs9 +1 by A34,NAT_1:12;
then
A46: len vs +(1+1) = len p9 +(1+1) by A34,Lm1;
then 0+1 <= len vs by A31,A22,XXREAL_0:2;
then consider i being Nat such that
0<=i and
A47: i<len vs and
A48: len vs = i+1 by FINSEQ_6:127;
(len vs +1)+1 = len vs +(1+1) .= len vs9 +1 by A45,Lm1;
then
A49: len vs9 = i+(1+1) by A48;
A50: vs9.1 = vs9.len vs9 by A24,MSSCYC_1:6;
A51: vs9.1 = v1 & vs9.(1+1) = v2 or vs9.1 = v2 & vs9.(1+1) = v1 by A44,A20,A32
,A21,A22,A24,Lm3;
assume
A52: vs.1 = vs.len vs;
vs.(0+1) = vs9.(1+1+0) by A31,A22,A45,A46,Lm1;
hence contradiction by A7,A52,A45,A47,A48,A49,A50,A51,Lm1;
end;
hence p is non cyclic by A43,A25,Th46,MSSCYC_1:6;
rng <*E*> = {E} & p1 = <*E*> by
A20,A32,A21,A22,FINSEQ_1:39,FINSEQ_6:132;
then rng p9 = {E} \/ rng p & {E} misses rng p by A33,FINSEQ_1:31,FINSEQ_3:91;
hence rng p = E by A9,A18,A23,A1,XBOOLE_1:72;
end;