:: Helly property for subtrees
:: by Jessica Enright and Piotr Rudnicki
::
:: Received January 10, 2008
:: Copyright (c) 2008-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, XBOOLE_0, FINSEQ_1, FUNCT_1, GRAPH_2, ARYTM_3, NAT_1,
XXREAL_0, SUBSET_1, TREES_1, TARSKI, CARD_1, ORDINAL1, FINSET_1,
MEMBERED, RELAT_1, ORDINAL4, GLIB_000, GLIB_001, ABIAN, ZFMISC_1,
ARYTM_1, GRAPH_1, RCOMP_1, SETFAM_1, HELLY;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, SETFAM_1, FUNCT_1, FINSEQ_1, MEMBERED, NAT_1,
TREES_1, XXREAL_2, ABIAN, GRAPH_2, GLIB_000, GLIB_001, GLIB_002,
FINSEQ_6;
constructors DOMAIN_1, SETFAM_1, NAT_1, GRAPH_2, GLIB_001, GLIB_002, XXREAL_2,
RELSET_1, RAT_1, FINSEQ_6;
registrations FINSET_1, XREAL_0, XXREAL_0, NAT_1, INT_1, RELAT_1, FINSEQ_1,
ABIAN, MEMBERED, GLIB_000, GLIB_001, GLIB_002, XXREAL_2, CARD_1, FUNCT_1,
XBOOLE_0, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, GLIB_001;
equalities GLIB_001;
expansions TARSKI, XBOOLE_0, GLIB_001;
theorems TARSKI, NAT_1, SETFAM_1, XBOOLE_0, XBOOLE_1, GRFUNC_1, FUNCT_1,
ZFMISC_1, ORDINAL1, FINSEQ_1, FINSEQ_2, FINSEQ_3, INT_1, EULER_1, CARD_1,
XREAL_1, XXREAL_0, CHORD, ABIAN, GLIB_000, GLIB_001, GLIB_002, MSSCYC_1,
MEMBERED, GRAPH_2, XXREAL_2, FINSEQ_4, PRE_CIRC, FINSEQ_6;
schemes NAT_1, FINSEQ_1;
begin :: General preliminaries
theorem
for p being non empty FinSequence holds <*p.1*>^'p = p
proof
let p be non empty FinSequence;
set o = <*p.1*>^'p;
A1: len o +1 = len <*p.1*> + len p by FINSEQ_6:139;
A2: len <*p.1*> = 1 by FINSEQ_1:39;
A3: now
let k be Nat such that
A4: 1<=k and
A5: k <= len o;
per cases;
suppose
A6: k <= len <*p.1*>;
then k <= 1 by FINSEQ_1:39;
then
A7: k = 1 by A4,XXREAL_0:1;
hence o.k = <*p.1*>.1 by A6,FINSEQ_6:140
.= p.k by A7;
end;
suppose
k > len <*p.1*>;
then consider i being Element of NAT such that
A8: k = len <*p.1*>+i and
A9: 1 <= i by FINSEQ_4:84;
i < len p by A1,A2,A5,A8,NAT_1:13;
hence o.k = p.k by A2,A8,A9,FINSEQ_6:141;
end;
end;
len o +1 = 1 + len p by A1,FINSEQ_1:39;
hence thesis by A3,FINSEQ_1:14;
end;
definition
let p, q be FinSequence;
func maxPrefix(p,q) -> FinSequence means
:Def1:
it is_a_prefix_of p & it
is_a_prefix_of q & for r being FinSequence st r is_a_prefix_of p & r
is_a_prefix_of q holds r is_a_prefix_of it;
existence
proof
deffunc F(set) = $1;
defpred P[set] means
ex r being FinSequence st r c= p & r c= q & len r = $1;
set S = { F(k) where k is Nat : k <= len p & P[k] };
A1: for x being object st x in S holds x is natural
proof
let x be object;
assume x in S;
then ex n being Nat st x = n & n <= len p & P[n];
hence thesis;
end;
A2: S is finite from FINSEQ_1:sch 6;
{} c= p & {} c= q & len {} = 0;
then 0 in S;
then reconsider S as finite non empty natural-membered set by A1,A2,
MEMBERED:def 6;
set maxk = max S;
maxk in S by XXREAL_2:def 8;
then consider K being Nat such that
A3: K = maxk and
K <= len p and
A4: P[K];
consider R being FinSequence such that
A5: R c= p and
A6: R c= q and
A7: len R = K by A4;
take R;
thus R c= p by A5;
thus R c= q by A6;
let r be FinSequence such that
A8: r c= p and
A9: r c= q;
dom r c= dom p by A8,GRFUNC_1:2;
then len r <= len p by FINSEQ_3:30;
then len r in S by A8,A9;
then len r <= len R by A3,A7,XXREAL_2:def 8;
then
A10: dom r c= dom R by FINSEQ_3:30;
now
let x be object;
assume
A11: x in dom r;
hence r.x = p.x by A8,GRFUNC_1:2
.= R.x by A5,A10,A11,GRFUNC_1:2;
end;
hence thesis by A10,GRFUNC_1:2;
end;
uniqueness;
commutativity;
end;
theorem
for p, q being FinSequence holds p is_a_prefix_of q iff maxPrefix(p,q) = p
by Def1;
theorem Th3:
for p, q being FinSequence holds len maxPrefix(p,q)<= len p
proof
let p, q be FinSequence;
maxPrefix(p,q) c= p by Def1;
hence thesis by FINSEQ_1:63;
end;
theorem Th4:
for p being non empty FinSequence holds <*p.1*> is_a_prefix_of p
proof
let p be non empty FinSequence;
A1: now
let x be object;
A2: dom <*p.1*> = Seg 1 by FINSEQ_1:def 8;
assume x in dom <*p.1*>;
then x = 1 by A2,FINSEQ_1:2,TARSKI:def 1;
hence <*p.1*>.x = p.x;
end;
len p >= 1 by FINSEQ_1:20;
then len <*p.1*> <= len p by FINSEQ_1:39;
then dom <*p.1*> c= dom p by FINSEQ_3:30;
hence thesis by A1,GRFUNC_1:2;
end;
theorem Th5:
for p, q being non empty FinSequence st p.1 = q.1 holds 1 <= len
maxPrefix(p,q)
proof
let p, q be non empty FinSequence such that
A1: p.1 = q.1 and
A2: 1 > len maxPrefix(p,q);
A3: <*p.1*> c= p by Th4;
<*p.1*> c= q by A1,Th4;
then <*p.1*> c= maxPrefix(p,q) by A3,Def1;
then len <*p.1*> <= len maxPrefix(p,q) by FINSEQ_1:63;
hence contradiction by A2,FINSEQ_1:39;
end;
theorem Th6:
for p, q being FinSequence for j being Nat st j <= len maxPrefix(
p,q) holds maxPrefix(p,q).j = p.j
proof
let p, q be FinSequence;
let j be Nat such that
A1: j <= len maxPrefix(p,q);
A2: maxPrefix(p,q) c= p by Def1;
per cases;
suppose
A3: j = 0;
then
A4: not j in dom p by FINSEQ_3:24;
not j in dom maxPrefix(p,q) by A3,FINSEQ_3:24;
hence maxPrefix(p,q).j = 0 by FUNCT_1:def 2
.= p.j by A4,FUNCT_1:def 2;
end;
suppose
j <> 0;
then 0+1 <= j by NAT_1:13;
then j in dom maxPrefix(p,q) by A1,FINSEQ_3:25;
hence thesis by A2,GRFUNC_1:2;
end;
end;
theorem Th7:
for p, q being FinSequence for j being Nat st j <= len maxPrefix(
p,q) holds p.j = q.j
proof
let p, q be FinSequence;
let j be Nat such that
A1: j <= len maxPrefix(p,q);
thus p.j = maxPrefix(p,q).j by A1,Th6
.= q.j by A1,Th6;
end;
theorem Th8:
for p, q being FinSequence holds not p is_a_prefix_of q iff len
maxPrefix(p,q) < len p
proof
let p, q be FinSequence;
A1: maxPrefix(p,q) c= p by Def1;
hereby
assume
A2: not p c= q;
A3: now
assume len maxPrefix(p,q) = len p;
then
A4: dom maxPrefix(p,q) = dom p by FINSEQ_3:29;
maxPrefix(p,q) c= p by Def1;
then maxPrefix(p,q) = p by A4,GRFUNC_1:3;
hence contradiction by A2,Def1;
end;
maxPrefix(p,q) c= p by Def1;
then len maxPrefix(p,q) <= len p by FINSEQ_1:63;
hence len maxPrefix(p,q) < len p by A3,XXREAL_0:1;
end;
assume that
A5: len maxPrefix(p,q) < len p and
A6: p c= q;
p c= maxPrefix(p,q) by A6,Def1;
hence contradiction by A5,A1,XBOOLE_0:def 10;
end;
theorem Th9:
for p, q being FinSequence st not p is_a_prefix_of q & not q
is_a_prefix_of p holds p.(len maxPrefix(p,q) +1) <> q.(len maxPrefix(p,q) +1)
proof
let p, q be FinSequence such that
A1: not p c= q and
A2: not q c= p and
A3: p.(len maxPrefix(p,q) +1) = q.(len maxPrefix(p,q) +1);
set dI = len maxPrefix(p,q);
set mP = maxPrefix(p,q);
set lmP = mP^<*p.(dI+1)*>;
A4: now
let x be object such that
A5: x in dom lmP;
reconsider n = x as Nat by A5;
A6: 1 <= n by A5,FINSEQ_3:25;
n <= len lmP by A5,FINSEQ_3:25;
then
A7: n <= len mP + 1 by FINSEQ_2:16;
per cases by A7,NAT_1:8;
suppose
A8: n <= dI;
then n in dom mP by A6,FINSEQ_3:25;
hence lmP.x = mP.x by FINSEQ_1:def 7
.= q.x by A8,Th6;
end;
suppose
n = dI + 1;
hence lmP.x = q.x by A3,FINSEQ_1:42;
end;
end;
A9: now
let x be object such that
A10: x in dom lmP;
reconsider n = x as Nat by A10;
A11: 1 <= n by A10,FINSEQ_3:25;
n <= len lmP by A10,FINSEQ_3:25;
then
A12: n <= len mP + 1 by FINSEQ_2:16;
per cases by A12,NAT_1:8;
suppose
A13: n <= dI;
then n in dom mP by A11,FINSEQ_3:25;
hence lmP.x = mP.x by FINSEQ_1:def 7
.= p.x by A13,Th6;
end;
suppose
n = dI + 1;
hence lmP.x = p.x by FINSEQ_1:42;
end;
end;
A14: len lmP = len mP + 1 by FINSEQ_2:16;
len mP < len q by A2,Th8;
then len lmP <= len q by A14,NAT_1:13;
then dom lmP c= dom q by FINSEQ_3:30;
then
A15: lmP c= q by A4,GRFUNC_1:2;
len mP < len p by A1,Th8;
then len lmP <= len p by A14,NAT_1:13;
then dom lmP c= dom p by FINSEQ_3:30;
then lmP c= p by A9,GRFUNC_1:2;
then lmP c= mP by A15,Def1;
then len lmP <= len mP by FINSEQ_1:63;
then len mP + 1 <= len mP by FINSEQ_2:16;
hence contradiction by NAT_1:13;
end;
begin :: Graph preliminaries
theorem Th10:
for G being _Graph, W be Walk of G, m, n being Nat holds len W
.cut(m,n) <= len W
proof
let G be _Graph, W be Walk of G, m, n be Nat;
reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
m is odd & n is odd & m <= n & n <= len W;
then W.cut(m,n) = (m,n)-cut W by GLIB_001:def 11;
then len W.cut(m9,n9) <= len W by MSSCYC_1:8;
hence thesis;
end;
suppose
not (m is odd & n is odd & m <= n & n <= len W);
hence thesis by GLIB_001:def 11;
end;
end;
theorem
for G being _Graph, W being Walk of G, m, n being Nat st W.cut(m,n) is
non trivial holds W is non trivial
proof
let G be _Graph, W be Walk of G, m, n be Nat such that
A1: W.cut(m,n) is non trivial and
A2: W is trivial;
reconsider W as trivial Walk of G by A2;
reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 12;
W.cut(m9,n9) is trivial;
hence thesis by A1;
end;
theorem Th12:
for G being _Graph, W being Walk of G for m, n, i being odd Nat
st m <= n & n <= len W & i <= len W.cut(m,n) ex j being odd Nat st W.cut(m,n).i
= W.j & j = m+i-1 & j <= len W
proof
let G be _Graph, W be Walk of G;
let m, n, i being odd Nat such that
A1: m <= n and
A2: n <= len W and
A3: i <= len W.cut(m,n);
set j = m+i-1;
m >= 1 & i >= 1 by ABIAN:12;
then m+i >= 1+1 by XREAL_1:7;
then m+i-1 >= 1+1-1 by XREAL_1:9;
then j is odd Element of NAT by INT_1:3;
then reconsider j as odd Nat;
take j;
reconsider m9= m, n9 = n as odd Element of NAT by ORDINAL1:def 12;
i >= 1 by ABIAN:12;
then i-1 >= 1-1 by XREAL_1:9;
then reconsider i1 = i-1 as Element of NAT by INT_1:3;
i < len W.cut(m,n) +1 by A3,NAT_1:13;
then
A4: i1 < len W.cut(m,n) +1 -1 by XREAL_1:9;
thus W.cut(m,n).i = W.cut(m9,n9).(i1+1) .= W.(m+i1) by A1,A2,A4,GLIB_001:36
.= W.j;
thus j = m+i-1;
m+i <= len W.cut(m,n)+m by A3,XREAL_1:7;
then m9+i <= n9+1 by A1,A2,GLIB_001:36;
then m+i-1 <= n+1-1 by XREAL_1:9;
hence thesis by A2,XXREAL_0:2;
end;
registration
let G be _Graph;
cluster -> non empty for Walk of G;
correctness by CARD_1:27;
end;
theorem Th13:
for G being _Graph for W1, W2 being Walk of G st W1
is_a_prefix_of W2 holds W1.vertices() c= W2.vertices()
proof
let G be _Graph, W1, W2 be Walk of G such that
A1: W1 c= W2;
let x be object;
assume x in W1.vertices();
then consider n being odd Element of NAT such that
A2: n <= len W1 and
A3: W1.n = x by GLIB_001:87;
1 <= n by ABIAN:12;
then n in dom W1 by A2,FINSEQ_3:25;
then
A4: W2.n = x by A1,A3,GRFUNC_1:2;
len W1 <= len W2 by A1,FINSEQ_1:63;
then n <= len W2 by A2,XXREAL_0:2;
hence thesis by A4,GLIB_001:87;
end;
theorem
for G being _Graph for W1, W2 being Walk of G st W1 is_a_prefix_of W2
holds W1.edges() c= W2.edges()
proof
let G be _Graph, W1, W2 be Walk of G such that
A1: W1 c= W2;
let x be object;
assume x in W1.edges();
then consider n being even Element of NAT such that
A2: 1 <= n and
A3: n <= len W1 and
A4: W1.n = x by GLIB_001:99;
n in dom W1 by A2,A3,FINSEQ_3:25;
then
A5: W2.n = x by A1,A4,GRFUNC_1:2;
len W1 <= len W2 by A1,FINSEQ_1:63;
then n <= len W2 by A3,XXREAL_0:2;
hence thesis by A2,A5,GLIB_001:99;
end;
theorem Th15:
for G being _Graph for W1, W2 being Walk of G holds W1
is_a_prefix_of W1.append(W2)
proof
let G be _Graph, W1, W2 be Walk of G;
set W1a = W1.append(W2);
per cases;
suppose
W1.last() = W2.first();
then len W1 <= len W1a by GLIB_001:29;
then
A1: dom W1 c= dom W1a by FINSEQ_3:30;
for x being object st x in dom W1 holds W1.x = W1a.x by GLIB_001:32;
hence thesis by A1,GRFUNC_1:2;
end;
suppose
W1.last() <> W2.first();
hence thesis by GLIB_001:def 10;
end;
end;
theorem Th16:
for G being _Graph, W1,W2 being Walk of G st W1 is trivial & W1
.last() = W2.first() holds W1.append(W2) = W2
proof
let G be _Graph, W1,W2 be Walk of G such that
A1: W1 is trivial and
A2: W1.last() = W2.first();
A3: len W1 = 1 by A1,GLIB_001:126;
then
A4: len W1.append(W2) + 1 = 1 + len W2 by A2,GLIB_001:28;
now
let k be Nat such that
A5: 1 <= k and
A6: k <= len W1.append(W2);
1-1 <= k-1 by A5,XREAL_1:9;
then reconsider k1 = k-1 as Element of NAT by INT_1:3;
k-1 < k by XREAL_1:44;
then k-1 < len W2 by A4,A6,XXREAL_0:2;
then W1.append(W2).(1 + k1) = W2.(k1+1) by A2,A3,GLIB_001:33;
hence W1.append(W2).k = W2.k;
end;
hence thesis by A4,FINSEQ_1:14;
end;
theorem Th17:
for G being _Graph for W1, W2 being Trail of G st W1.last() = W2
.first() & W1.edges() misses W2.edges() holds W1.append(W2) is Trail-like
proof
let G be _Graph, W1, W2 be Trail of G such that
A1: W1.last() = W2.first() and
A2: W1.edges() misses W2.edges();
set W = W1.append(W2);
now
let m,n be even Element of NAT such that
A3: 1 <= m and
A4: m < n and
A5: n <= len W;
1 <= n by A3,A4,XXREAL_0:2;
then
A6: n in dom W by A5,FINSEQ_3:25;
m <= len W by A4,A5,XXREAL_0:2;
then
A7: m in dom W by A3,FINSEQ_3:25;
per cases by A6,GLIB_001:34;
suppose
A8: n in dom W1;
then
A9: n <= len W1 by FINSEQ_3:25;
then m <= len W1 by A4,XXREAL_0:2;
then m in dom W1 by A3,FINSEQ_3:25;
then
A10: W1.m = W.m by GLIB_001:32;
W1.m <> W1.n by A3,A4,A9,GLIB_001:138;
hence W.m <> W.n by A8,A10,GLIB_001:32;
end;
suppose
ex k being Element of NAT st k < len W2 & n = len W1 + k;
then consider k being Element of NAT such that
A11: k < len W2 and
A12: n = len W1 + k;
reconsider k as odd Element of NAT by A12;
A13: W.n = W2.(k+1) by A1,A11,A12,GLIB_001:33;
A14: k+1 <= len W2 by A11,NAT_1:13;
1 <= k+1 by NAT_1:11;
then
A15: W2.(k+1) in W2.edges() by A14,GLIB_001:99;
per cases by A7,GLIB_001:34;
suppose
A16: m in dom W1;
then 1 <= m & m <= len W1 by FINSEQ_3:25;
then
A17: W1.m in W1.edges() by GLIB_001:99;
W.m = W1.m by A16,GLIB_001:32;
hence W.m <> W.n by A2,A13,A15,A17,XBOOLE_0:3;
end;
suppose
ex l being Element of NAT st l < len W2 & m = len W1 + l;
then consider l being Element of NAT such that
A18: l < len W2 and
A19: m = len W1 + l;
reconsider l as odd Element of NAT by A19;
l < k by A4,A12,A19,XREAL_1:6;
then
A20: 1 <= l+1 & l+1 < k+1 by NAT_1:11,XREAL_1:6;
W.m = W2.(l+1) by A1,A18,A19,GLIB_001:33;
hence W.m <> W.n by A13,A14,A20,GLIB_001:138;
end;
end;
end;
hence thesis by GLIB_001:138;
end;
theorem Th18:
for G being _Graph for P1, P2 being Path of G st P1.last() = P2
.first() & P1 is open & P2 is open & P1.edges() misses P2.edges() & (P1.first()
in P2.vertices() implies P1.first() = P2.last()) & P1.vertices() /\ P2
.vertices() c= {P1.first(), P1.last()} holds P1.append(P2) is Path-like
proof
let G be _Graph, P1, P2 be Path of G such that
A1: P1.last() = P2.first() and
A2: P1 is open and
A3: P2 is open and
A4: P1.edges() misses P2.edges() and
A5: P1.first() in P2.vertices() implies P1.first() = P2.last() and
A6: P1.vertices() /\ P2.vertices() c= {P1.first(), P1.last()};
thus P1.append(P2) is Trail-like by A1,A4,Th17;
set P = P1.append(P2);
let m, n be odd Element of NAT such that
A7: m < n and
A8: n <= len P and
A9: P.m = P.n and
A10: m <> 1 or n <> len P;
A11: 1 <= m by ABIAN:12;
1 <= n by ABIAN:12;
then
A12: n in dom P by A8,FINSEQ_3:25;
m <= len P by A7,A8,XXREAL_0:2;
then
A13: m in dom P by A11,FINSEQ_3:25;
per cases by A12,GLIB_001:34;
suppose
ex k being Element of NAT st k < len P2 & n = len P1 + k;
then consider k being Element of NAT such that
A14: k < len P2 and
A15: n = len P1 + k;
A16: P.n = P2.(k+1) by A1,A14,A15,GLIB_001:33;
reconsider k as even Element of NAT by A15;
A17: k+1 <= len P2 by A14,NAT_1:13;
then
A18: P2.(k+1) in P2.vertices() by GLIB_001:87;
per cases by A13,GLIB_001:34;
suppose
ex k being Element of NAT st k < len P2 & m = len P1 + k;
then consider l being Element of NAT such that
A19: l < len P2 and
A20: m = len P1 + l;
A21: P.m = P2.(l+1) by A1,A19,A20,GLIB_001:33;
l < k by A7,A15,A20,XREAL_1:6;
then
A22: l+1 < k+1 by XREAL_1:6;
reconsider l as even Element of NAT by A20;
l+1 is odd;
then
A23: P2.last() = P2.(k+1) by A9,A16,A17,A21,A22,GLIB_001:def 28;
P2.first() = P2.(l+1) by A9,A16,A17,A21,A22,GLIB_001:def 28;
hence contradiction by A3,A9,A16,A21,A23;
end;
suppose
A24: m in dom P1;
set x = P1.m;
A25: P1.m = P.m by A24,GLIB_001:32;
A26: m <= len P1 by A24,FINSEQ_3:25;
then P1.m in P1.vertices() by GLIB_001:87;
then
A27: x in P1.vertices() /\ P2.vertices() by A9,A16,A18,A25,XBOOLE_0:def 4;
per cases by A6,A27,TARSKI:def 2;
suppose
A28: x = P1.last();
then
A29: m >= len P1 by GLIB_001:def 28,A2;
A30: 2*0+1 >= k+1 by A1,A3,A9,A16,A17,A25,A28,GLIB_001:def 28;
1 <= k+1 by NAT_1:11;
then 1 = k+1 by A30,XXREAL_0:1;
hence contradiction by A7,A15,A29;
end;
suppose
A31: x = P1.first();
then
A32: x = P1.(2*0+1);
A33: now
assume m <> 1;
then 1 < m by A11,XXREAL_0:1;
then x = P1.last() by A26,A32,GLIB_001:def 28;
hence contradiction by A2,A31;
end;
now
assume k+1 = len P2;
then len P +1 = len P1 + (k+1) by A1,GLIB_001:28;
hence contradiction by A10,A15,A33;
end;
then
A34: k+1 < len P2 by A17,XXREAL_0:1;
P2.(k+1) = P2.last() by A5,A9,A16,A18,A24,A31,GLIB_001:32;
then P2.first() = P2.last() by A34,GLIB_001:def 28;
hence contradiction by A3;
end;
end;
end;
suppose
A35: n in dom P1;
then
A36: n <= len P1 by FINSEQ_3:25;
then 1 <= m & m <= len P1 by A7,ABIAN:12,XXREAL_0:2;
then m in dom P1 by FINSEQ_3:25;
then
A37: P1.m = P.m by GLIB_001:32
.= P1.n by A9,A35,GLIB_001:32;
then m = 1 by A7,A36,GLIB_001:def 28;
then P1.first() = P1.last() by A7,A36,A37,GLIB_001:def 28;
hence contradiction by A2;
end;
end;
theorem Th19:
for G being _Graph for P1, P2 being Path of G st P1.last() = P2
.first() & P1 is open & P2 is open & P1.vertices() /\ P2.vertices() = {P1
.last()} holds P1.append(P2) is open Path-like
proof
let G be _Graph, P1, P2 be Path of G such that
A1: P1.last() = P2.first() and
A2: P1 is open and
A3: P2 is open and
A4: P1.vertices() /\ P2.vertices() = {P1.last()};
set P = P1.append(P2);
thus P is open
proof
assume
A5: P.first() = P.last();
P.first() = P1.first() & P.last() = P2.last() by A1,GLIB_001:30;
then P1.first() in P1.vertices() & P1.first() in P2.vertices() by A5,
GLIB_001:88;
then P1.first() in {P1.last()} by A4,XBOOLE_0:def 4;
then P1.first() = P1.last() by TARSKI:def 1;
hence contradiction by A2;
end;
A6: now
A7: P1.first() in P1.vertices() by GLIB_001:88;
assume P1.first() in P2.vertices();
then P1.first() in {P1.last()} by A4,A7,XBOOLE_0:def 4;
then P1.first() = P1.last() by TARSKI:def 1;
hence contradiction by A2;
end;
A8: P1.edges() misses P2.edges()
proof
assume P1.edges() /\ P2.edges() <> {};
then consider x being object such that
A9: x in P1.edges() /\ P2.edges() by XBOOLE_0:def 1;
x in P2.edges() by A9,XBOOLE_0:def 4;
then consider
u1, u2 being Vertex of G, m being odd Element of NAT such that
A10: m+2 <= len P2 and
A11: u1 = P2.m and
x = P2.(m+1) and
A12: u2 = P2.(m+2) and
A13: x Joins u1, u2, G by GLIB_001:103;
x in P1.edges() by A9,XBOOLE_0:def 4;
then consider
v1, v2 being Vertex of G, n being odd Element of NAT such that
A14: n+2 <= len P1 and
A15: v1 = P1.n and
x = P1.(n+1) and
A16: v2 = P1.(n+2) and
A17: x Joins v1, v2, G by GLIB_001:103;
A18: n+0 < n+2 by XREAL_1:8;
per cases;
suppose
A19: v1 <> v2;
n <= len P1 by A14,A18,XXREAL_0:2;
then
A20: v1 in P1.vertices() by A15,GLIB_001:87;
v2 in P1.vertices() by A14,A16,GLIB_001:87;
then
A21: {v1, v2} c= P1.vertices() by A20,ZFMISC_1:32;
m+0 < m+2 by XREAL_1:8;
then m <= len P2 by A10,XXREAL_0:2;
then
A22: u1 in P2.vertices() by A11,GLIB_001:87;
u2 in P2.vertices() by A10,A12,GLIB_001:87;
then
A23: {u1, u2} c= P2.vertices() by A22,ZFMISC_1:32;
A24: v1 = u1 & v2 = u2 or v1 = u2 & v2 = u1 by A17,A13,GLIB_000:15;
then v1 = P1.last() by A4,A21,A23,XBOOLE_1:19,ZFMISC_1:20;
hence contradiction by A4,A19,A24,A21,A23,XBOOLE_1:19,ZFMISC_1:20;
end;
suppose
A25: v1 = v2;
then P1.first() = v1 by A14,A15,A16,A18,GLIB_001:def 28
.= P1.last() by A14,A15,A16,A18,A25,GLIB_001:def 28;
hence contradiction by A2;
end;
end;
P1.vertices() /\ P2.vertices() c= {P1.first(), P1.last()} by A4,ZFMISC_1:7;
hence thesis by A1,A2,A3,A8,A6,Th18;
end;
theorem Th20:
for G being _Graph for P1, P2 being Path of G st P1.last() = P2
.first() & P2.last() = P1.first() & P1 is open & P2 is open & P1.edges() misses
P2.edges() & P1.vertices() /\ P2.vertices() = {P1.last(), P1.first()} holds P1
.append(P2) is Cycle-like
proof
let G be _Graph, P1, P2 be Path of G such that
A1: P1.last() = P2.first() and
A2: P2.last() = P1.first() and
A3: P1 is open and
A4: P2 is open & P1.edges() misses P2.edges() & P1.vertices() /\ P2
.vertices() = {P1.last(), P1.first()};
set P = P1.append(P2);
P.first() = P1.first() & P.last() = P2.last() by A1,GLIB_001:30;
hence P is closed by A2;
thus P is Path-like by A1,A2,A3,A4,Th18;
P1.first() <> P1.last() by A3;
then P1 is non trivial by GLIB_001:127;
then
A5: len P1 >= 3 by GLIB_001:125;
len P >= len P1 by A1,GLIB_001:29;
then len P >= 3 by A5,XXREAL_0:2;
hence thesis by GLIB_001:125;
end;
theorem
for G being simple _Graph for W1, W2 being Walk of G for k being odd
Nat st k <= len W1 & k <= len W2 & for j being odd Nat st j <= k holds W1.j =
W2.j holds for j being Nat st 1 <= j & j <= k holds W1.j = W2.j
proof
let G be simple _Graph, W1, W2 be Walk of G, k be odd Nat such that
A1: k <= len W1 and
A2: k <= len W2 and
A3: for j being odd Nat st j <= k holds W1.j = W2.j;
let j be Nat such that
A4: 1 <= j and
A5: j <= k;
per cases;
suppose
j is odd;
hence thesis by A3,A5;
end;
suppose
j is even;
then reconsider j9 = j as even Nat;
1-1 <= j-1 by A4,XREAL_1:9;
then reconsider j1 = j9-1 as odd Element of NAT by INT_1:3;
A6: j1 < j by XREAL_1:44;
j <= len W1 by A1,A5,XXREAL_0:2;
then j1 < len W1 by A6,XXREAL_0:2;
then
A7: W1.(j1+1) Joins W1.j1, W1.(j1+2), G by GLIB_001:def 3;
j1+1 < k by A5,XXREAL_0:1;
then j1+1+1 <= k by NAT_1:13;
then
A8: W1.(j1+2) = W2.(j1+2) by A3;
j <= len W2 by A2,A5,XXREAL_0:2;
then j1 < len W2 by A6,XXREAL_0:2;
then
A9: W2.(j1+1) Joins W2.j1, W2.(j1+2), G by GLIB_001:def 3;
W1.j1 = W2.j1 by A3,A5,A6,XXREAL_0:2;
hence thesis by A7,A9,A8,GLIB_000:def 20;
end;
end;
theorem Th22:
for G being _Graph for W1, W2 being Walk of G st W1.first() = W2
.first() holds len maxPrefix(W1,W2) is odd
proof
let G be _Graph, W1, W2 be Walk of G;
assume that
A1: W1.first() = W2.first() and
A2: len maxPrefix(W1,W2) is even;
set dI = len maxPrefix(W1,W2);
reconsider dIp = dI-1 as odd Element of NAT by A1,A2,Th5,INT_1:5;
A3: dIp < dI by XREAL_1:146;
set mP = maxPrefix(W1,W2);
set lmP = mP^<*W1.(dI+1)*>;
A4: len lmP = len mP + 1 by FINSEQ_2:16;
A5: now
let x be object such that
A6: x in dom lmP;
reconsider n = x as Nat by A6;
A7: 1 <= n by A6,FINSEQ_3:25;
n <= len lmP by A6,FINSEQ_3:25;
then
A8: n <= len mP + 1 by FINSEQ_2:16;
per cases by A8,NAT_1:8;
suppose
A9: n <= dI;
then n in dom mP by A7,FINSEQ_3:25;
hence lmP.x = mP.x by FINSEQ_1:def 7
.= W1.x by A9,Th6;
end;
suppose
n = dI + 1;
hence lmP.x = W1.x by FINSEQ_1:42;
end;
end;
A10: dI = dIp+1;
A11: dI <= len W2 by Th3;
then dIp < len W2 by XREAL_1:146,XXREAL_0:2;
then
A12: W2.dI Joins W2.dIp, W2.(dIp+2), G by A10,GLIB_001:def 3;
A13: dI <= len W1 by Th3;
then dIp < len W1 by XREAL_1:146,XXREAL_0:2;
then
A14: W1.dI Joins W1.dIp, W1.(dIp+2), G by A10,GLIB_001:def 3;
W1.dI = W2.dI by Th7;
then
A15: W1.dIp = W2.dIp & W1.(dIp+2) = W2.(dIp+2) or W1.dIp = W2.(dIp+2) & W1.(
dIp+2) = W2.dIp by A14,A12,GLIB_000:15;
A16: now
let x be object such that
A17: x in dom lmP;
reconsider n = x as Nat by A17;
A18: 1 <= n by A17,FINSEQ_3:25;
n <= len lmP by A17,FINSEQ_3:25;
then
A19: n <= len mP + 1 by FINSEQ_2:16;
per cases by A19,NAT_1:8;
suppose
A20: n <= dI;
then n in dom mP by A18,FINSEQ_3:25;
hence lmP.x = mP.x by FINSEQ_1:def 7
.= W2.x by A20,Th6;
end;
suppose
A21: n = dI + 1;
hence lmP.x = W1.(dI+1) by FINSEQ_1:42
.= W2.x by A3,A15,A21,Th7;
end;
end;
dI < len W2 by A2,A11,XXREAL_0:1;
then len lmP <= len W2 by A4,NAT_1:13;
then dom lmP c= dom W2 by FINSEQ_3:30;
then
A22: lmP c= W2 by A16,GRFUNC_1:2;
dI < len W1 by A2,A13,XXREAL_0:1;
then len lmP <= len W1 by A4,NAT_1:13;
then dom lmP c= dom W1 by FINSEQ_3:30;
then lmP c= W1 by A5,GRFUNC_1:2;
then lmP c= mP by A22,Def1;
then len lmP <= len mP by FINSEQ_1:63;
then len mP + 1 <= len mP by FINSEQ_2:16;
hence contradiction by NAT_1:13;
end;
theorem Th23:
for G being _Graph for W1, W2 being Walk of G st W1.first() = W2
.first() & not W1 is_a_prefix_of W2 holds len maxPrefix(W1,W2) +2 <= len W1
proof
let G be _Graph, W1, W2 be Walk of G;
assume W1.first() = W2.first() & not W1 c= W2;
then len maxPrefix(W1,W2) < len W1 & len maxPrefix(W1,W2) is odd Nat by Th8
,Th22;
hence thesis by CHORD:4;
end;
theorem Th24:
for G being non-multi _Graph for W1, W2 being Walk of G st W1
.first() = W2.first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1
holds W1.(len maxPrefix(W1,W2) +2) <> W2.(len maxPrefix(W1,W2) +2)
proof
let G be non-multi _Graph, W1, W2 be Walk of G such that
A1: W1.first() = W2.first() and
A2: not W1 c= W2 and
A3: not W2 c= W1 and
A4: W1.(len maxPrefix(W1,W2) +2) = W2.(len maxPrefix(W1,W2) +2);
set dI = len maxPrefix(W1,W2);
A5: dI is odd by A1,Th22;
dI < len W1 by A2,Th8;
then
A6: W1.(dI+1) Joins W1.dI,W1.(dI+2), G by A5,GLIB_001:def 3;
A7: W1.dI = W2.dI by Th7;
dI < len W2 by A3,Th8;
then
A8: W2.(dI+1) Joins W2.dI,W2.(dI+2), G by A5,GLIB_001:def 3;
W1.(dI +1) <> W2.(dI +1) by A2,A3,Th9;
hence contradiction by A4,A7,A6,A8,GLIB_000:def 20;
end;
begin :: Trees
definition
mode _Tree is Tree-like _Graph;
let G be _Graph;
mode _Subtree of G is Tree-like Subgraph of G;
end;
registration
let T be _Tree;
cluster Trail-like -> Path-like for Walk of T;
correctness
proof
let W be Walk of T such that
A1: W is Trail-like;
defpred P[Nat] means $1 is odd & $1 <= len W & ex k being odd Element of
NAT st k < $1 & W.k = W.$1;
assume not W is Path-like;
then
ex m, n being odd Element of NAT st m < n & n <= len W & W.m = W.n &( m
<> 1 or n <> len W) by A1;
then
A2: ex p being Nat st P[p];
consider p being Nat such that
A3: P[p] and
A4: for r being Nat st P[r] holds p <= r from NAT_1:sch 5(A2);
reconsider P = p as Element of NAT by ORDINAL1:def 12;
consider k being odd Element of NAT such that
A5: k < p and
p <= len W and
A6: W.k = W.p by A3;
set Wc = W.cut(k,P);
len Wc + k = P+1 by A3,A5,GLIB_001:36;
then len Wc <> 1 by A5;
then
A7: Wc is non trivial by GLIB_001:126;
A8: Wc.last() = W.p by A3,A5,GLIB_001:37;
A9: Wc is Path-like
proof
assume not thesis;
then consider m, n being odd Element of NAT such that
A10: m < n and
A11: n <= len Wc and
A12: Wc.m = Wc.n and
A13: m <> 1 or n <> len Wc by A1;
A14: m < len Wc by A10,A11,XXREAL_0:2;
consider kn1 being odd Nat such that
A15: Wc.n = W.kn1 and
A16: kn1 = k+n-1 and
A17: kn1 <= len W by A3,A5,A11,Th12;
reconsider kn1 as odd Element of NAT by ORDINAL1:def 12;
A18: 1 <= m by ABIAN:12;
m <= len Wc by A10,A11,XXREAL_0:2;
then consider km1 being odd Nat such that
A19: Wc.m = W.km1 and
A20: km1 = k+m-1 and
A21: km1 <= len W by A3,A5,Th12;
reconsider km1 as odd Element of NAT by ORDINAL1:def 12;
per cases by A11,XXREAL_0:1;
suppose
n < len Wc;
then k+n < k+len Wc by XREAL_1:6;
then k+n < p+1 by A3,A5,GLIB_001:36;
then
A22: kn1 < p by A16,XREAL_1:19;
k+m < k+n by A10,XREAL_1:6;
then km1 < kn1 by A20,A16,XREAL_1:9;
hence contradiction by A4,A12,A19,A15,A17,A22;
end;
suppose
A23: n = len Wc;
k+m < len Wc + k by A14,XREAL_1:6;
then k+m < p+1 by A3,A5,GLIB_001:36;
then
A24: km1 < p by A20,XREAL_1:19;
1 < m by A13,A18,A23,XXREAL_0:1;
then k+1 < k+m by XREAL_1:6;
then k < km1 by A20,XREAL_1:20;
hence contradiction by A4,A6,A8,A12,A19,A21,A23,A24;
end;
end;
Wc.first() = W.k by A3,A5,GLIB_001:37;
then Wc is closed by A6,A8;
then Wc is Cycle-like by A7,A9;
hence contradiction by GLIB_002:def 2;
end;
end;
theorem Th25:
for T being _Tree for P being Path of T st P is non trivial holds P is open
by GLIB_001:def 31,GLIB_002:def 2;
registration
let T be _Tree;
cluster non trivial -> open for Path of T;
correctness by Th25;
end;
theorem Th26: :: Only for _Tree as it is not true for cyclic paths
for T being _Tree for P being Path of T for i, j being odd Nat
st i < j & j <= len P holds P.i <> P.j
proof
let T be _Tree, P be Path of T, i, j be odd Nat such that
A1: i < j and
A2: j <= len P and
A3: P.i = P.j;
reconsider i, j as odd Element of NAT by ORDINAL1:def 12;
A4: i < j by A1;
then
A5: i = 1 by A2,A3,GLIB_001:def 28;
then
A6: P is non trivial by A1,A2,GLIB_001:126;
P.first() = P.last() by A2,A3,A4,A5,GLIB_001:def 28;
hence contradiction by A6,GLIB_001:def 24;
end;
theorem Th27:
for T being _Tree for a, b being Vertex of T for P1, P2 being
Path of T st P1 is_Walk_from a, b & P2 is_Walk_from a, b holds P1 = P2
proof
let T be _Tree;
let a, b be Vertex of T;
let P1, P2 be Path of T such that
A1: P1 is_Walk_from a, b and
A2: P2 is_Walk_from a, b;
set di = len maxPrefix(P1,P2);
A3: P1.first() = a & P2.first() = a by A1,A2;
then reconsider di as odd Element of NAT by Th22;
defpred P[Nat] means $1 is odd & di < $1 & $1 <= len P2 & P2.$1 in P1
.vertices();
assume
A4: P1 <> P2;
A5: not P2 c= P1
proof
assume
A6: P2 c= P1;
then len P2 <= len P1 by FINSEQ_1:63;
then
A7: len P2 < len P1 by A4,A6,FINSEQ_2:129,XXREAL_0:1;
1 <= len P2 by ABIAN:12;
then len P2 in dom P2 by FINSEQ_3:25;
then
A8: P2.len P2 = P1.len P2 by A6,GRFUNC_1:2;
A9: P1.len P1 = P1.last() .= b by A1;
P2.len P2 = P2.last() .= b by A2;
hence contradiction by A7,A8,A9,Th26;
end;
A10: ex k being Nat st P[k]
proof
take k = len P2;
thus k is odd;
di +2 <= len P2 & di < di+2 by A3,A5,Th23,NAT_1:19;
hence di < k by XXREAL_0:2;
thus k <= len P2;
P2.k = P2.last() .= b by A2
.= P1.last() by A1;
hence thesis by GLIB_001:88;
end;
consider ei being Nat such that
A11: P[ei] and
A12: for n being Nat st P[n] holds ei <= n from NAT_1:sch 5(A10);
reconsider ei as odd Element of NAT by A11,ORDINAL1:def 12;
set e = P2.ei;
set fi = P1.find(e);
set pde = P2.cut(di,ei), pdf = P1.cut(di,fi);
A13: fi <= len P1 by A11,GLIB_001:def 19;
set rpdf = pdf.reverse();
A14: rpdf.vertices() = pdf.vertices() by GLIB_001:92;
set C = pde.append(rpdf);
set d = P1.di;
A15: P2.di = P1.di by Th7;
then
A16: pde.first() = d by A11,GLIB_001:37;
A17: e = P1.fi by A11,GLIB_001:def 19;
len P2 <> 1
proof
assume len P2 = 1;
then di < 1 by A11,XXREAL_0:2;
hence contradiction by ABIAN:12;
end;
then
A18: not P2 is trivial by GLIB_001:126;
A19: di < fi
proof
assume di >= fi;
then P1.fi = P2.fi & ei > fi by A11,Th7,XXREAL_0:2;
then P2.first() = e & P2.last() = e by A11,A17,GLIB_001:def 28;
hence contradiction by A18,GLIB_001:def 24;
end;
then
A20: pdf is non trivial by A13,GLIB_001:131;
then
A21: P1 is non trivial;
fi <= len P1 by A11,GLIB_001:def 19;
then
A22: rpdf.vertices() c= P1.vertices() by A19,A14,GLIB_001:94;
A23: pde.vertices() /\ rpdf.vertices() c= {e, d}
proof
assume not thesis;
then consider g being object such that
A24: g in pde.vertices() /\ rpdf.vertices() and
A25: not g in {e, d};
g in pde.vertices() by A24,XBOOLE_0:def 4;
then consider gii being odd Element of NAT such that
A26: gii <= len pde and
A27: pde.gii = g by GLIB_001:87;
consider gi being odd Nat such that
A28: P2.gi = pde.gii and
A29: gi = di+gii-1 and
A30: gi <= len P2 by A11,A26,Th12;
reconsider gi as odd Element of NAT by ORDINAL1:def 12;
A31: gii >= 1 by ABIAN:12;
A32: gi < ei
proof
A33: len pde + di = ei+1 by A11,GLIB_001:36;
assume
A34: gi >= ei;
per cases by A34,XXREAL_0:1;
suppose
gi = ei;
then pde.gii = pde.last() by A29,A33
.= e by A11,GLIB_001:37;
hence contradiction by A25,A27,TARSKI:def 2;
end;
suppose
gi > ei;
then gi+1 > ei+1 by XREAL_1:6;
hence contradiction by A26,A29,A33,XREAL_1:6;
end;
end;
gii <> 1 by A16,A25,A27,TARSKI:def 2;
then
A35: gii > 1 by A31,XXREAL_0:1;
A36: di < gi
proof
assume di >= gi;
then di+gii > gi+1 by A35,XREAL_1:8;
hence contradiction by A29;
end;
g in rpdf.vertices() by A24,XBOOLE_0:def 4;
hence contradiction by A12,A22,A27,A28,A30,A36,A32;
end;
A37: pde.last() = e by A11,GLIB_001:37;
pdf.first() = d by A13,A19,GLIB_001:37;
then
A38: rpdf.last() = d by GLIB_001:22;
pdf.last() = e by A13,A17,A19,GLIB_001:37;
then
A39: rpdf.first() = e by GLIB_001:22;
{e, d} c= pde.vertices() /\ rpdf.vertices()
proof
let x be object;
assume
A40: x in {e, d};
per cases by A40,TARSKI:def 2;
suppose
x = e;
then x in pde.vertices() & x in rpdf.vertices() by A37,A39,GLIB_001:88;
hence thesis by XBOOLE_0:def 4;
end;
suppose
x = d;
then x in pde.vertices() & x in rpdf.vertices() by A16,A38,GLIB_001:88;
hence thesis by XBOOLE_0:def 4;
end;
end;
then
A41: pde.vertices() /\ rpdf.vertices() = {e, d} by A23;
A42: pde is non trivial by A11,GLIB_001:131;
then
A43: P2 is non trivial;
A44: not P1 c= P2
proof
assume
A45: P1 c= P2;
then len P1 <= len P2 by FINSEQ_1:63;
then
A46: len P1 < len P2 by A4,A45,FINSEQ_2:129,XXREAL_0:1;
1 <= len P1 by ABIAN:12;
then len P1 in dom P1 by FINSEQ_3:25;
then
A47: P1.len P1 = P2.len P1 by A45,GRFUNC_1:2;
A48: P2.len P2 = P2.last() .= b by A2;
P1.len P1 = P1.last() .= b by A1;
hence contradiction by A46,A47,A48,Th26;
end;
A49: pde.edges() misses rpdf.edges()
proof
A50: pdf.vertices() = rpdf.vertices() by GLIB_001:92;
A51: pdf.edges() = rpdf.edges() by GLIB_001:107;
assume pde.edges() /\ rpdf.edges() <> {};
then consider x being object such that
A52: x in pde.edges() /\ rpdf.edges() by XBOOLE_0:def 1;
x in rpdf.edges() by A52,XBOOLE_0:def 4;
then consider
u1, u2 being Vertex of T, m being odd Element of NAT such that
A53: m+2 <= len pdf and
A54: u1 = pdf.m and
x = pdf.(m+1) and
A55: u2 = pdf.(m+2) and
A56: x Joins u1, u2, T by A51,GLIB_001:103;
x in pde.edges() by A52,XBOOLE_0:def 4;
then consider
v1, v2 being Vertex of T, n being odd Element of NAT such that
A57: n+2 <= len pde and
A58: v1 = pde.n and
x = pde.(n+1) and
A59: v2 = pde.(n+2) and
A60: x Joins v1, v2, T by GLIB_001:103;
A61: n+0 < n+2 by XREAL_1:8;
per cases;
suppose
A62: v1 <> v2;
A63: n+2 = n+1+1;
then
A64: n+1 < len pde by A57,NAT_1:13;
then
A65: pde.(n+2) = P2.(di+(n+1)) by A11,A63,GLIB_001:36;
consider ni being Nat such that
A66: n = ni+1 by NAT_1:6;
reconsider ni as Element of NAT by ORDINAL1:def 12;
A67: u2 in pdf.vertices() by A53,A55,GLIB_001:87;
m+0 < m+2 by XREAL_1:8;
then
A68: m <= len pdf by A53,XXREAL_0:2;
then u1 in pdf.vertices() by A54,GLIB_001:87;
then
A69: {u1, u2} c= rpdf.vertices() by A50,A67,ZFMISC_1:32;
A70: m+2 = m+1+1;
then
A71: m+1 < len pdf by A53,NAT_1:13;
then
A72: pdf.(m+2) = P1.(di+(m+1)) by A13,A19,A70,GLIB_001:36;
n <= len pde by A57,A61,XXREAL_0:2;
then
A73: v1 in pde.vertices() by A58,GLIB_001:87;
v2 in pde.vertices() by A57,A59,GLIB_001:87;
then
A74: {v1, v2} c= pde.vertices() by A73,ZFMISC_1:32;
A75: v1 = u1 & v2 = u2 or v1 = u2 & v2 = u1 by A60,A56,GLIB_000:15;
then
A76: v1 = e or v1 = d by A41,A74,A69,XBOOLE_1:19,ZFMISC_1:22;
n+0 < n+2 by XREAL_1:8;
then n <= len pde by A57,XXREAL_0:2;
then
A77: ni < len pde by A66,NAT_1:13;
then
A78: pde.n = P2.(di+ni) by A11,A66,GLIB_001:36;
A79: P2.(di+2) = e
proof
per cases by A41,A62,A75,A74,A69,A76,XBOOLE_1:19,ZFMISC_1:22;
suppose
A80: v1 = e & v2 = d;
di+(n+2) <= len pde +di by A57,XREAL_1:6;
then di+n+1+1 <= ei+1 by A11,GLIB_001:36;
then di+n+1 <= ei by XREAL_1:6;
then
A81: di+(n+1) <= len P2 by A11,XXREAL_0:2;
di <= di+n by NAT_1:11;
then di < di+n+1 by NAT_1:13;
then P2.first() = d & P2.last() = d by A15,A59,A65,A80,A81,
GLIB_001:def 28;
hence thesis by A43,GLIB_001:def 24;
end;
suppose
A82: v1 = d & v2 = e;
ni = 0
proof
di+ni < len pde +di by A77,XREAL_1:6;
then di+ni < ei+1 by A11,GLIB_001:36;
then di+ni <= ei by NAT_1:13;
then
A83: di+ni <= len P2 by A11,XXREAL_0:2;
assume
A84: ni <> 0;
reconsider ni as even Element of NAT by A66;
di+0 < di+ni by A84,XREAL_1:6;
then P2.first() = d & P2.last() = d by A15,A58,A78,A82,A83,
GLIB_001:def 28;
hence contradiction by A43,GLIB_001:def 24;
end;
hence thesis by A11,A59,A66,A64,A82,GLIB_001:36;
end;
end;
consider im being Nat such that
A85: m = im+1 by NAT_1:6;
A86: v2 = e or v2 = d by A41,A75,A74,A69,XBOOLE_1:19,ZFMISC_1:22;
reconsider im as Element of NAT by ORDINAL1:def 12;
A87: im < len pdf by A68,A85,NAT_1:13;
then
A88: pdf.m = P1.(di+im) by A13,A19,A85,GLIB_001:36;
P1.(di+2) = e
proof
per cases by A60,A56,A62,A76,A86,GLIB_000:15;
suppose
A89: u1 = e & u2 = d;
di+(m+2) <= len pdf +di by A53,XREAL_1:6;
then di+m+1+1 <= fi+1 by A13,A19,GLIB_001:36;
then di+m+1 <= fi by XREAL_1:6;
then
A90: di+(m+1) <= len P1 by A13,XXREAL_0:2;
di <= di+m by NAT_1:11;
then di < di+m+1 by NAT_1:13;
then P1.first() = d & P1.last() = d by A55,A72,A89,A90,
GLIB_001:def 28;
hence thesis by A21,GLIB_001:def 24;
end;
suppose
A91: u1 = d & u2 = e;
im = 0
proof
di+im < len pdf +di by A87,XREAL_1:6;
then di+im < fi+1 by A13,A19,GLIB_001:36;
then di+im <= fi by NAT_1:13;
then
A92: di+im <= len P1 by A13,XXREAL_0:2;
assume
A93: im <> 0;
reconsider im as even Element of NAT by A85;
di+0 < di+im by A93,XREAL_1:6;
then P1.first() = d & P1.last() = d by A54,A88,A91,A92,
GLIB_001:def 28;
hence contradiction by A21,GLIB_001:def 24;
end;
hence thesis by A13,A19,A55,A85,A71,A91,GLIB_001:36;
end;
end;
hence contradiction by A3,A44,A5,A79,Th24;
end;
suppose
v1 = v2;
then pde.first() = v1 & pde.last() = v1 by A57,A58,A59,A61,
GLIB_001:def 28;
hence contradiction by A42,GLIB_001:def 24;
end;
end;
rpdf is non trivial by A20,GLIB_001:129;
then C is Cycle-like by A42,A16,A37,A39,A38,A41,A49,Th20;
hence contradiction;
end;
definition
let T be _Tree;
let a, b be Vertex of T;
func T.pathBetween(a,b) -> Path of T means
:Def2:
it is_Walk_from a, b;
existence
proof
consider W being Walk of T such that
A1: W is_Walk_from a,b by GLIB_002:def 1;
set P = the Path-like Subwalk of W;
take P;
P is_Walk_from W.first(), W.last() by GLIB_001:def 32;
then P is_Walk_from a, W.last() by A1;
hence thesis by A1;
end;
uniqueness by Th27;
end;
theorem Th28:
for T being _Tree, a, b being Vertex of T holds T.pathBetween(a,
b).first() = a & T.pathBetween(a,b).last() = b
proof
let T be _Tree, a, b be Vertex of T;
A1: T.pathBetween(a,b) is_Walk_from a, b by Def2;
hence T.pathBetween(a,b).first() = a;
thus thesis by A1;
end;
:: more theorems about pathBetween ?
theorem Th29:
for T being _Tree, a, b being Vertex of T holds a in T
.pathBetween(a,b).vertices() & b in T.pathBetween(a,b).vertices()
proof
let T be _Tree, a, b be Vertex of T;
T.pathBetween(a,b).first() = a by Th28;
hence a in T.pathBetween(a,b).vertices() by GLIB_001:88;
T.pathBetween(a,b).last() = b by Th28;
hence thesis by GLIB_001:88;
end;
registration
let T be _Tree, a be Vertex of T;
cluster T.pathBetween(a, a) -> closed;
correctness
by Def2,GLIB_001:119;
end;
registration
let T be _Tree, a be Vertex of T;
cluster T.pathBetween(a, a) -> trivial;
correctness;
end;
theorem Th30:
for T being _Tree, a being Vertex of T holds T.pathBetween(a,a)
.vertices() = {a}
proof
let T be _Tree, a be Vertex of T;
set P = T.pathBetween(a,a);
consider v being Vertex of T such that
A1: P = T.walkOf(v) by GLIB_001:128;
a = P.first() & T.walkOf(v).first() = v by Th28;
hence thesis by A1,GLIB_001:90;
end;
theorem Th31:
for T being _Tree, a, b being Vertex of T holds T.pathBetween(a,
b).reverse() = T.pathBetween(b,a)
proof
let T be _Tree, a, b be Vertex of T;
set P = T.pathBetween(a,b);
P is_Walk_from a, b by Def2;
then P.reverse() is_Walk_from b, a by GLIB_001:23;
hence thesis by Def2;
end;
theorem Th32:
for T being _Tree, a, b being Vertex of T holds T.pathBetween(a,
b).vertices() = T.pathBetween(b,a).vertices()
proof
let T be _Tree, a, b be Vertex of T;
T.pathBetween(a,b).reverse() = T.pathBetween(b,a) by Th31;
hence thesis by GLIB_001:92;
end;
theorem Th33:
for T being _Tree for a, b being Vertex of T for t being
_Subtree of T for a9, b9 being Vertex of t st a = a9 & b = b9 holds T
.pathBetween(a,b) = t.pathBetween(a9,b9)
proof
let T be _Tree;
let a, b be Vertex of T;
let t be _Subtree of T;
let a9, b9 be Vertex of t such that
A1: a = a9 and
A2: b = b9;
set tp = t.pathBetween(a9,b9);
reconsider tp9 = tp as Walk of T by GLIB_001:167;
A3: tp is_Walk_from a9, b9 by Def2;
A4: tp9.last() = tp.last() .= b by A2,A3;
tp9.first() = tp.first() .= a by A1,A3;
then tp9 is Path-like & tp9 is_Walk_from a, b by A4,GLIB_001:176;
hence thesis by Def2;
end;
theorem Th34:
for T being _Tree for a, b being Vertex of T for t being
_Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds T
.pathBetween(a,b).vertices() c= the_Vertices_of t
proof
let T be _Tree, a, b be Vertex of T, t be _Subtree of T;
assume a in the_Vertices_of t & b in the_Vertices_of t;
then reconsider a9 = a, b9 = b as Vertex of t;
set Tp = T.pathBetween(a,b), tp = t.pathBetween(a9,b9);
Tp.vertices() = tp.vertices() by Th33,GLIB_001:76;
hence thesis;
end;
theorem Th35:
for T being _Tree for P being Path of T for a, b being Vertex of
T for i, j being odd Nat st i <= j & j <= len P & P.i = a & P.j = b holds T
.pathBetween(a,b) = P.cut(i, j)
proof
let T be _Tree, P be Path of T, a, b be Vertex of T, i, j be odd Nat such
that
A1: i <= j & j <= len P & P.i = a & P.j = b;
reconsider i9 = i, j9 = j as odd Element of NAT by ORDINAL1:def 12;
P.cut(i9, j9) is_Walk_from a, b by A1,GLIB_001:37;
hence thesis by Def2;
end;
theorem Th36:
for T being _Tree for a, b, c being Vertex of T holds c in T
.pathBetween(a,b).vertices() iff T.pathBetween(a,b) = T.pathBetween(a,c).append
(T.pathBetween(c,b))
proof
let T be _Tree, a, b, c be Vertex of T;
set P = T.pathBetween(a,b);
set ci = P.find(c);
set pac = T.pathBetween(a,c), pcb = T.pathBetween(c,b);
hereby
A1: P = P.cut(1, len P) by GLIB_001:39;
A2: 1 <= ci & 1 = 2*0+1 by ABIAN:12;
assume
A3: c in P.vertices();
then
A4: ci <= len P by GLIB_001:def 19;
A5: P.ci = c by A3,GLIB_001:def 19;
P.len P = P.last() .= b by Th28;
then
A6: pcb = P.cut(ci, len P) by A4,A5,Th35;
P.1 = P.first() .= a by Th28;
then pac = P.cut(1,ci) by A4,A2,A5,Th35;
hence P = T.pathBetween(a,c).append(T.pathBetween(c,b)) by A4,A2,A6,A1,
GLIB_001:38;
end;
assume P = pac.append(pcb);
then
A7: pac.vertices() c= P.vertices() by Th13,Th15;
c in pac.vertices() by Th29;
hence thesis by A7;
end;
theorem Th37:
for T being _Tree for a, b, c being Vertex of T holds c in T
.pathBetween(a,b).vertices() iff T.pathBetween(a,c) is_a_prefix_of T
.pathBetween(a,b)
proof
let T be _Tree, a, b, c be Vertex of T;
hereby
assume c in T.pathBetween(a,b).vertices();
then
T.pathBetween(a,b) = T.pathBetween(a,c).append(T.pathBetween(c,b)) by Th36;
hence T.pathBetween(a,c) c= T.pathBetween(a,b) by Th15;
end;
assume T.pathBetween(a,c) c= T.pathBetween(a,b);
then
A1: T.pathBetween(a,c).vertices() c= T.pathBetween(a,b).vertices() by Th13;
c in T.pathBetween(a,c).vertices() by Th29;
hence thesis by A1;
end;
theorem Th38:
for T being _Tree for P1, P2 being Path of T st P1.last() = P2
.first() & P1.vertices() /\ P2.vertices() = {P1.last()} holds P1.append(P2) is
Path-like
proof
let T be _Tree, P1, P2 be Path of T such that
A1: P1.last() = P2.first() and
A2: P1.vertices() /\ P2.vertices() = {P1.last()};
per cases;
suppose
P1 is trivial;
hence thesis by A1,Th16;
end;
suppose
P2 is trivial;
hence thesis by GLIB_001:130;
end;
suppose
P1 is non trivial & P2 is non trivial;
hence thesis by A1,A2,Th19;
end;
end;
theorem Th39:
for T being _Tree for a, b, c being Vertex of T holds c in T
.pathBetween(a,b).vertices() iff T.pathBetween(a,c).vertices() /\ T.pathBetween
(c,b).vertices() = {c}
proof
let T be _Tree, a, b, c be Vertex of T;
set Pac = T.pathBetween(a,c), Pcb = T.pathBetween(c,b), Pab = T.pathBetween(
a,b);
A1: Pac.last() = c by Th28
.= Pcb.first() by Th28;
thus c in Pab.vertices() implies Pac.vertices() /\ Pcb.vertices() = {c}
proof
assume
A2: c in T.pathBetween(a,b).vertices();
thus Pac.vertices() /\ Pcb.vertices() c= {c}
proof
let x be object;
assume
A3: x in Pac.vertices() /\ Pcb.vertices();
then
A4: x in Pac.vertices() by XBOOLE_0:def 4;
A5: x in Pcb.vertices() by A3,XBOOLE_0:def 4;
A6: Pcb.first() = c by Th28;
A7: Pab = Pac.append(Pcb) by A2,Th36;
A8: Pab.first() = a & Pab.last() = b by Th28;
A9: Pac.last() = c by Th28;
per cases;
suppose
Pab is trivial;
then Pab.first() = Pab.last() by GLIB_001:127;
then
A10: Pab.vertices() = {a} by A8,Th30;
x in Pac.vertices() \/ Pcb.vertices() by A4,XBOOLE_0:def 3;
then x in Pab.vertices() by A7,A9,A6,GLIB_001:93;
hence thesis by A2,A10,TARSKI:def 1;
end;
suppose
A11: Pab is non trivial;
consider n being odd Element of NAT such that
A12: n <= len Pcb and
A13: Pcb.n = x by A5,GLIB_001:87;
1 <= n by ABIAN:12;
then 1-1 <= n-1 by XREAL_1:9;
then reconsider n1 = n-1 as even Element of NAT by INT_1:3;
consider m being odd Element of NAT such that
A14: m <= len Pac and
A15: Pac.m = x by A4,GLIB_001:87;
A16: m <= len Pac + n1 by A14,NAT_1:12;
1 <= m by ABIAN:12;
then m in dom Pac by A14,FINSEQ_3:25;
then
A17: Pab.m = x by A7,A15,GLIB_001:32;
len Pac + (n1+1) <= len Pac + len Pcb by A12,XREAL_1:6;
then len Pac + n1+1 -1 <= len Pac + len Pcb -1 by XREAL_1:9;
then
A18: len Pac + n1+1-1 <= len Pab +1 -1 by A7,A9,A6,GLIB_001:28;
A19: n1+1 = n;
then n1 < len Pcb by A12,NAT_1:13;
then
A20: Pab.(len Pac + n1) = x by A7,A9,A6,A13,A19,GLIB_001:33;
per cases by A16,XXREAL_0:1;
suppose
A21: m < len Pac + n1;
then Pab.first() = x by A17,A20,A18,GLIB_001:def 28
.= Pab.last() by A17,A20,A18,A21,GLIB_001:def 28;
hence thesis by A11,GLIB_001:def 24;
end;
suppose
A22: m = len Pac + n1;
then n1 = 0 by A14,NAT_1:16;
hence thesis by A9,A15,A22,TARSKI:def 1;
end;
end;
end;
let x be object;
assume x in {c};
then
A23: x = c by TARSKI:def 1;
then x = Pcb.first() by Th28;
then
A24: x in Pcb.vertices() by GLIB_001:88;
x = Pac.last() by A23,Th28;
then x in Pac.vertices() by GLIB_001:88;
hence thesis by A24,XBOOLE_0:def 4;
end;
Pac.first() = a & Pcb.last() = b by Th28;
then
A25: Pac.append(Pcb) is_Walk_from a, b by A1,GLIB_001:30;
assume Pac.vertices() /\ Pcb.vertices() = {c};
then Pac.vertices() /\ Pcb.vertices() = {Pac.last()} by Th28;
then Pac.append(Pcb) is Path-like by A1,Th38;
then Pab = Pac.append(Pcb) by A25,Def2;
hence thesis by Th36;
end;
theorem Th40:
for T being _Tree for a, b, c, d being Vertex of T for P1, P2
being Path of T st P1 = T.pathBetween(a,b) & P2 = T.pathBetween(a,c) & not P1
is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1.len maxPrefix(P1,P2)
holds (T.pathBetween(d,b)).vertices() /\ (T.pathBetween(d,c)).vertices() = {d}
proof
let T being _Tree;
let a, b, c, d being Vertex of T;
let P1, P2 being Path of T such that
A1: P1 = T.pathBetween(a,b) and
A2: P2 = T.pathBetween(a,c) and
A3: not P1 c= P2 and
A4: not P2 c= P1 and
A5: d = P1.len maxPrefix(P1,P2);
set Pad = T.pathBetween(a,d);
set di = len maxPrefix(P1,P2);
A6: P1.first() = a by A1,Th28;
A7: P2.first() = a by A2,Th28;
then reconsider di as odd Element of NAT by A6,Th22;
A8: di <= di+2 by NAT_1:11;
set Pdb = T.pathBetween(d,b);
A9: Pdb.first() = d by Th28;
set Pdc = T.pathBetween(d,c);
A10: d = P2.len maxPrefix(P1,P2) by A5,Th7;
A11: di <= di+2 by NAT_1:11;
di+2 <= len P2 by A4,A6,A7,Th23;
then di <= len P2 by A11,XXREAL_0:2;
then d in P2.vertices() by A10,GLIB_001:87;
then
A12: P2 = Pad.append(Pdc) by A2,Th36;
A13: Pad.last() = d by Th28;
A14: Pdc.1 = Pdc.first() .= d by Th28;
A15: Pdc.first() = d by Th28;
di+2 <= len P1 by A3,A6,A7,Th23;
then
A16: di <= len P1 by A8,XXREAL_0:2;
then d in P1.vertices() by A5,GLIB_001:87;
then
A17: P1 = Pad.append(Pdb) by A1,Th36;
A18: 1 <= di by ABIAN:12;
then Pad = P1.cut(2*0+1,di) by A5,A6,A16,Th35;
then
A19: len Pad + ((2*0)+1) = di + 1 by A16,A18,GLIB_001:36;
A20: Pdb.1 = Pdb.first() .= d by Th28;
thus Pdb.vertices() /\ Pdc.vertices() = {d}
proof
hereby
assume not Pdb.vertices() /\ Pdc.vertices() c= {d};
then consider e being object such that
A21: e in Pdb.vertices() /\ Pdc.vertices() and
A22: not e in {d};
A23: e in Pdb.vertices() by A21,XBOOLE_0:def 4;
A24: e in Pdc.vertices() by A21,XBOOLE_0:def 4;
reconsider e as Vertex of T by A21;
consider ebi be odd Element of NAT such that
A25: ebi <= len Pdb and
A26: e = Pdb.ebi by A23,GLIB_001:87;
set Pdeb = Pdb.cut(1,ebi);
1 <= ebi & 2*0+1 is odd Element of NAT by ABIAN:12;
then
A27: Pdeb is_Walk_from d, e by A20,A25,A26,GLIB_001:37;
1 < len Pdeb
proof
assume
A28: 1 >= len Pdeb;
per cases by A28,NAT_1:25;
suppose
len Pdeb = 2*0;
hence contradiction;
end;
suppose
A29: len Pdeb = 1;
A30: Pdeb.1 = d by A27;
Pdeb.1 = e by A27,A29;
hence contradiction by A22,A30,TARSKI:def 1;
end;
end;
then
A31: (2*0+1)+2 <= len Pdeb by CHORD:4;
then
A32: 2 < len Pdeb by XXREAL_0:2;
consider eci be odd Element of NAT such that
A33: eci <= len Pdc and
A34: e = Pdc.eci by A24,GLIB_001:87;
set Pdec = Pdc.cut(1,eci);
1 <= eci & 2*0+1 is odd Element of NAT by ABIAN:12;
then
A35: Pdec is_Walk_from d, e by A14,A33,A34,GLIB_001:37;
1 < len Pdec
proof
assume
A36: 1 >= len Pdec;
per cases by A36,NAT_1:25;
suppose
len Pdec = 2*0;
hence contradiction;
end;
suppose
A37: len Pdec = 1;
A38: Pdec.1 = d by A35;
Pdec.1 = e by A35,A37;
hence contradiction by A22,A38,TARSKI:def 1;
end;
end;
then
A39: (2*0+1)+2 <= len Pdec by CHORD:4;
then
A40: 2 < len Pdec by XXREAL_0:2;
1+2 in dom Pdeb by A31,FINSEQ_3:25;
then
A41: Pdeb.(1+2) = Pdb.(1+2) by A25,GLIB_001:46;
len Pdeb <= len Pdb by Th10;
then 2 < len Pdb by A32,XXREAL_0:2;
then
A42: P1.(di+2) = Pdb.(1+2) by A9,A13,A17,A19,GLIB_001:33;
len Pdec <= len Pdc by Th10;
then 2 < len Pdc by A40,XXREAL_0:2;
then
A43: P2.(di+2) = Pdc.(1+2) by A15,A13,A12,A19,GLIB_001:33;
A44: 1+2 in dom Pdec by A39,FINSEQ_3:25;
Pdeb.(1+2) = Pdec.(1+2) by A27,A35,Th27;
hence contradiction by A3,A4,A6,A7,A33,A42,A41,A43,A44,Th24,GLIB_001:46;
end;
d in Pdb.vertices() & d in Pdc.vertices() by A9,A15,GLIB_001:88;
then d in Pdb.vertices() /\ Pdc.vertices() by XBOOLE_0:def 4;
hence thesis by ZFMISC_1:31;
end;
end;
Lm1: for T being _Tree for a, b, c being Vertex of T st c in T.pathBetween(a,b
).vertices() holds T.pathBetween(a,b).vertices() /\ T.pathBetween(b,c)
.vertices() /\ T.pathBetween(c,a).vertices() = {c}
proof
let T be _Tree, a, b, c be Vertex of T such that
A1: c in T.pathBetween(a,b).vertices();
set P1 = T.pathBetween(a,b), P2 = T.pathBetween(b,c), P3 = T.pathBetween(c,a
);
P1.vertices() = T.pathBetween(b,a).vertices() by Th32;
then P2.vertices() /\ P3.vertices() = {c} by A1,Th39;
then P1.vertices() /\ (P2.vertices() /\ P3.vertices())={c} by A1,ZFMISC_1:46;
hence thesis by XBOOLE_1:16;
end;
Lm2: for T being _Tree for a, b, c being Vertex of T for P1, P4 being Path of
T st P1 = T.pathBetween(a,b) & P4 = T.pathBetween(a,c) & not P1 c= P4 & not P4
c= P1 holds P1.vertices() /\ T.pathBetween(b,c).vertices() /\ T.pathBetween(c,a
).vertices() = {P1.len maxPrefix(P1,P4)}
proof
let T be _Tree, a, b, c be Vertex of T, P1, P4 be Path of T such that
A1: P1 = T.pathBetween(a,b) and
A2: P4 = T.pathBetween(a,c) and
A3: not P1 c= P4 and
A4: not P4 c= P1;
set P3 = T.pathBetween(c,a);
A5: P3.vertices() = P4.vertices() by A2,Th32;
set i = len maxPrefix(P1,P4);
P1.first() = a by A1,Th28;
then
A6: P1.first() = P4.first() by A2,Th28;
then reconsider i9 = i as odd Element of NAT by Th22;
set x = P1.i9;
A7: i <= i+2 by NAT_1:11;
A8: now
assume b in P3.vertices();
then b in P4.vertices() by A2,Th32;
then P4 = T.pathBetween(a,b).append(T.pathBetween(b,c)) by A2,Th36;
hence contradiction by A1,A3,Th15;
end;
i+2 <= len P4 by A4,A6,Th23;
then
A9: i <= len P4 by A7,XXREAL_0:2;
A10: i+2 <= len P1 by A3,A6,Th23;
then reconsider x as Vertex of T by A7,GLIB_001:7,XXREAL_0:2;
set P1b = P1.cut(i9,len P1);
set P1br = P1b.reverse();
set j = len P1br;
set P4c = P4.cut(i9,len P4);
set Pbc = P1br.append(P4c);
A11: i <= len P1 by A7,A10,XXREAL_0:2;
then P1b.first() = P1.i9 by GLIB_001:37;
then
A12: P1br.last() = x by GLIB_001:22;
1 <= j by CHORD:2;
then j in dom P1br by FINSEQ_3:25;
then
A13: Pbc.j = x by A12,GLIB_001:32;
set P2 = T.pathBetween(b,c);
A14: x in P1.vertices() by A11,GLIB_001:87;
A15: P1.len P1 = P1.last() .= b by A1,Th28;
then P1b.last() = b by A11,GLIB_001:37;
then
A16: P1br.first() = b by GLIB_001:22;
A17: x = P4.i9 by Th7;
then x <> b by A8,A5,A9,GLIB_001:87;
then
A18: P1br is open by A12,A16;
P4.len P4 = P4.last() .= c by A2,Th28;
then P4c is_Walk_from x, c by A9,A17,GLIB_001:37;
then
A19: P4c = T.pathBetween(x,c) by Def2;
then
A20: P4c.first() = x by Th28;
then
A21: j <= len Pbc by A12,GLIB_001:29;
P1b is_Walk_from x, b by A11,A15,GLIB_001:37;
then P1b = T.pathBetween(x,b) by Def2;
then
P1br.vertices() = P1b.vertices() & P1b.vertices() /\ P4c.vertices() = {
x} by A1,A2,A3,A4,A19,Th40,GLIB_001:92;
then
A22: P1br.vertices() /\ P4c.vertices() c= {P1br.first(), P1br.last()} by A12,
ZFMISC_1:7;
A23: P4c.vertices() c= P4.vertices() by A9,GLIB_001:94;
A24: P1br.edges() misses P4c.edges()
proof
assume not thesis;
then P1br.edges() /\ P4c.edges() <> {};
then consider e being object such that
A25: e in P1br.edges() /\ P4c.edges() by XBOOLE_0:def 1;
e in P1br.edges() by A25,XBOOLE_0:def 4;
then consider
v1br, v2br being Vertex of T, n being odd Element of NAT such
that
A26: n+2 <= len P1br and
A27: v1br = P1br.n and
e = P1br.(n+1) and
A28: v2br = P1br.(n+2) and
A29: e Joins v1br, v2br, T by GLIB_001:103;
n <= n+2 by NAT_1:11;
then n <= len P1br by A26,XXREAL_0:2;
then
A30: v1br in P1br.vertices() by A27,GLIB_001:87;
v2br in P1br.vertices() by A26,A28,GLIB_001:87;
then
A31: {v1br, v2br} c= P1br.vertices() by A30,ZFMISC_1:32;
e in P4c.edges() by A25,XBOOLE_0:def 4;
then consider
v1c, v2c being Vertex of T, m being odd Element of NAT such that
A32: m+2 <= len P4c and
A33: v1c = P4c.m and
e = P4c.(m+1) and
A34: v2c = P4c.(m+2) and
A35: e Joins v1c, v2c, T by GLIB_001:103;
m <= m+2 by NAT_1:11;
then m <= len P4c by A32,XXREAL_0:2;
then
A36: v1c in P4c.vertices() by A33,GLIB_001:87;
A37: v1br = v1c & v2br = v2c or v1br = v2c & v2br = v1c by A29,A35,GLIB_000:15;
A38: v2c in P4c.vertices() by A32,A34,GLIB_001:87;
then {v1c, v2c} c= P4c.vertices() by A36,ZFMISC_1:32;
then
A39: {v1c, v2c} c= P1br.vertices() /\ P4c.vertices() by A37,A31,XBOOLE_1:19;
then
A40: v2c = b or v2c = x by A12,A16,A22,XBOOLE_1:1,ZFMISC_1:22;
v1c = b or v1c = x by A12,A16,A22,A39,XBOOLE_1:1,ZFMISC_1:22;
hence contradiction by A8,A5,A23,A35,A36,A38,A40,GLIB_000:18;
end;
A41: P4c.last() = c by A19,Th28;
then
A42: Pbc is_Walk_from b,c by A12,A20,A16,GLIB_001:30;
now
assume c in P1.vertices();
then P1 = T.pathBetween(a,c).append(T.pathBetween(c,b)) by A1,Th36;
hence contradiction by A2,A4,Th15;
end;
then x <> c by A11,GLIB_001:87;
then
A43: P4c is open by A20,A41;
not P1br.first() in P4c.vertices() by A8,A5,A23,A16;
then Pbc is Path of T by A12,A20,A18,A43,A22,A24,Th18;
then Pbc = P2 by A42,Def2;
then
A44: x in P2.vertices() by A21,A13,GLIB_001:87;
A45: x in P4.vertices() by A9,A17,GLIB_001:87;
A46: P1.vertices() /\ P2.vertices() /\ P3.vertices() c= {x}
proof
set Pcx = T.pathBetween(c,x), Pxa = T.pathBetween(x,a);
set Pbx = T.pathBetween(b,x), Pxc = T.pathBetween(x,c);
set Pax = T.pathBetween(a,x), Pxb = T.pathBetween(x,b);
let z be object;
A47: Pbx.vertices() = Pxb.vertices() by Th32;
A48: Pcx.vertices() = Pxc.vertices() by Th32;
A49: Pcx.last() = x by Th28
.= Pxa.first() by Th28;
P3 = Pcx.append(Pxa) by A5,A45,Th36;
then
A50: P3.vertices() = Pcx.vertices() \/ Pxa.vertices() by A49,GLIB_001:93;
A51: Pbx.last() = x by Th28
.= Pxc.first() by Th28;
P2 = Pbx.append(Pxc) by A44,Th36;
then
A52: P2.vertices() = Pbx.vertices() \/ Pxc.vertices() by A51,GLIB_001:93;
A53: Pax.last() = x by Th28
.= Pxb.first() by Th28;
P1 = Pax.append(Pxb) by A1,A14,Th36;
then
A54: P1.vertices() = Pax.vertices() \/ Pxb.vertices() by A53,GLIB_001:93;
assume
A55: z in P1.vertices() /\ P2.vertices() /\ P3.vertices();
then
A56: z in P1.vertices() /\ P2.vertices() by XBOOLE_0:def 4;
then z in P1.vertices() by XBOOLE_0:def 4;
then
A57: z in Pax.vertices() or z in Pxb.vertices() by A54,XBOOLE_0:def 3;
z in P3.vertices() by A55,XBOOLE_0:def 4;
then
A58: z in Pcx.vertices() or z in Pxa.vertices() by A50,XBOOLE_0:def 3;
z in P2.vertices() by A56,XBOOLE_0:def 4;
then
A59: z in Pbx.vertices() or z in Pxc.vertices() by A52,XBOOLE_0:def 3;
per cases by A57,A59,A58,Th32;
suppose
z in Pax.vertices() & z in Pbx.vertices();
then z in Pax.vertices() /\ Pxb.vertices() by A47,XBOOLE_0:def 4;
hence thesis by A1,A14,Th39;
end;
suppose
z in Pax.vertices() & z in Pcx.vertices();
then z in Pax.vertices() /\ Pxc.vertices() by A48,XBOOLE_0:def 4;
hence thesis by A2,A45,Th39;
end;
suppose
z in Pbx.vertices() & z in Pcx.vertices();
then z in Pbx.vertices() /\ Pxc.vertices() by A48,XBOOLE_0:def 4;
hence thesis by A44,Th39;
end;
end;
x in P1.vertices() /\ P2.vertices() by A14,A44,XBOOLE_0:def 4;
then x in P1.vertices() /\ P2.vertices() /\ P3.vertices() by A5,A45,
XBOOLE_0:def 4;
then {x} c= P1.vertices() /\ P2.vertices() /\ P3.vertices() by ZFMISC_1:31;
hence thesis by A46;
end;
definition
let T be _Tree, a, b, c be Vertex of T;
func MiddleVertex(a, b, c) -> Vertex of T means
:Def3:
T.pathBetween(a,b)
.vertices() /\ T.pathBetween(b,c).vertices() /\ T.pathBetween(c,a).vertices() =
{ it };
existence
proof
defpred P[Vertex of T,Vertex of T,Vertex of T,Vertex of T] means T
.pathBetween($1,$2).vertices() /\ (T.pathBetween($2,$3)).vertices() /\ (T
.pathBetween($3,$1)).vertices() = { $4 };
set P3 = T.pathBetween(c,a);
set P2 = T.pathBetween(b,c);
set P1 = T.pathBetween(a,b);
per cases;
suppose
A1: c in P1.vertices() or a in P2.vertices() or b in P3.vertices();
per cases by A1;
suppose
c in P1.vertices();
then P[a, b, c, c] by Lm1;
hence thesis;
end;
suppose
a in P2.vertices();
then P[b, c, a, a] by Lm1;
hence thesis by XBOOLE_1:16;
end;
suppose
b in P3.vertices();
then P[c, a, b, b] by Lm1;
hence thesis by XBOOLE_1:16;
end;
end;
suppose
A2: not c in P1.vertices() & not a in P2.vertices() & not b in P3
.vertices();
set P4 = T.pathBetween(a,c);
set i = len maxPrefix(P1,P4);
P1.last() = b by Th28;
then
A3: b in P1.vertices() by GLIB_001:88;
P4.last() = c by Th28;
then c in P4.vertices() by GLIB_001:88;
then not P4.vertices() c= P1.vertices() by A2;
then
A4: not P4 c= P1 by Th13;
P1.first() = a by Th28;
then
A5: P1.first() = P4.first() by Th28;
then reconsider i9 = i as odd Element of NAT by Th22;
set x = P1.i9;
P3.vertices() = P4.vertices() by Th32;
then
A6: not P1.vertices() c= P4.vertices() by A2,A3;
then i <= i+2 & i+2 <= len P1 by A5,Th13,Th23,NAT_1:11;
then reconsider x as Vertex of T by GLIB_001:7,XXREAL_0:2;
take x;
not P1 c= P4 by A6,Th13;
hence thesis by A4,Lm2;
end;
end;
uniqueness by ZFMISC_1:3;
end;
theorem Th41: :: PMV(a,b,c) = PMV(a,c,b)
for T being _Tree for a, b, c being Vertex of T holds
MiddleVertex(a,b,c) = MiddleVertex(a,c,b)
proof
let T be _Tree;
let a, b, c be Vertex of T;
set PMV1 = MiddleVertex(a,b,c);
set PMV2 = MiddleVertex(a,c,b);
A1: T.pathBetween(a,b).vertices() = T.pathBetween(b,a).vertices() & T
.pathBetween(b,c).vertices() = T.pathBetween(c,b).vertices() by Th32;
A2: T.pathBetween(c,a).vertices() = T.pathBetween(a,c).vertices() by Th32;
T.pathBetween(a,b).vertices() /\ T.pathBetween(b,c).vertices() /\ T
.pathBetween(c,a).vertices() = { PMV1 } & T.pathBetween(a,c).vertices() /\ T
.pathBetween(c,b).vertices() /\ T.pathBetween(b,a).vertices() = { PMV2 } by
Def3;
then {PMV1} = {PMV2} by A1,A2,XBOOLE_1:16;
hence thesis by ZFMISC_1:3;
end;
theorem Th42: :: PMV(a,b,c) = PMV(b,a,c)
for T being _Tree for a, b, c being Vertex of T holds
MiddleVertex(a,b,c) = MiddleVertex(b,a,c)
proof
let T be _Tree;
let a, b, c be Vertex of T;
set PMV1 = MiddleVertex(a,b,c);
set PMV2 = MiddleVertex(b,a,c);
A1: T.pathBetween(a,b).vertices() = T.pathBetween(b,a).vertices() & T
.pathBetween(b,c).vertices() = T.pathBetween(c,b).vertices() by Th32;
A2: T.pathBetween(c,a).vertices() = T.pathBetween(a,c).vertices() by Th32;
T.pathBetween(a,b).vertices() /\ T.pathBetween(b,c).vertices() /\ T
.pathBetween(c,a).vertices() = { PMV1 } & T.pathBetween(b,a).vertices() /\ T
.pathBetween(a,c).vertices() /\ T.pathBetween(c,b).vertices() = { PMV2 } by
Def3;
then {PMV1} = {PMV2} by A1,A2,XBOOLE_1:16;
hence thesis by ZFMISC_1:3;
end;
theorem ::PMV102: :: PMV(a,b,c) = PMV(b,c,a)
for T being _Tree for a, b, c being Vertex of T holds MiddleVertex(a,b
,c) = MiddleVertex(b,c,a)
proof
let T be _Tree;
let a, b, c be Vertex of T;
thus MiddleVertex(a,b,c) = MiddleVertex(b,a,c) by Th42
.= MiddleVertex(b,c,a) by Th41;
end;
theorem Th44: :: PMV(a,b,c) = PMV(c,a,b)
for T being _Tree for a, b, c being Vertex of T holds
MiddleVertex(a,b,c) = MiddleVertex(c,a,b)
proof
let T be _Tree;
let a, b, c be Vertex of T;
thus MiddleVertex(a,b,c) = MiddleVertex(a,c,b) by Th41
.= MiddleVertex(c,a,b) by Th42;
end;
theorem :: PMV104: :: PMV(a,b,c) = PMV(c,b,a)
for T being _Tree for a, b, c being Vertex of T holds MiddleVertex(a,b
,c) = MiddleVertex(c,b,a)
proof
let T be _Tree;
let a, b, c be Vertex of T;
thus MiddleVertex(a,b,c) = MiddleVertex(c,a,b) by Th44
.= MiddleVertex(c,b,a) by Th41;
end;
theorem Th46:
for T being _Tree for a, b, c being Vertex of T st c in T
.pathBetween(a,b).vertices() holds MiddleVertex(a,b,c) = c
proof
let T be _Tree;
let a, b, c be Vertex of T;
assume c in T.pathBetween(a,b).vertices();
then T.pathBetween(a,b).vertices() /\ T.pathBetween(b,c).vertices() /\ T
.pathBetween(c,a).vertices() = {c} by Lm1;
hence thesis by Def3;
end;
theorem :: PMV200: :: PMV(a,a,a) = a;
for T being _Tree for a being Vertex of T holds MiddleVertex(a,a,a) = a
proof
let T be _Tree;
let a be Vertex of T;
a in {a} by TARSKI:def 1;
then a in T.pathBetween(a,a).vertices() by Th30;
hence thesis by Th46;
end;
theorem Th48: :: PMV(a,a,b) = a;
for T being _Tree for a, b being Vertex of T holds MiddleVertex( a,a,b) = a
proof
let T be _Tree;
let a,b be Vertex of T;
T.pathBetween(a,b).first() = a by Th28;
then
A1: a in T.pathBetween(a,b).vertices() by GLIB_001:88;
MiddleVertex(a,a,b) = MiddleVertex(a,b,a) by Th41;
hence thesis by A1,Th46;
end;
theorem Th49: :: PMV(a,b,a) = a;
for T being _Tree for a, b being Vertex of T holds MiddleVertex( a,b,a) = a
proof
let T be _Tree;
let a,b be Vertex of T;
MiddleVertex(a,a,b) = MiddleVertex(a,b,a) by Th41;
hence thesis by Th48;
end;
theorem :: PMV203: :: PMV(a,b,b) = b;
for T being _Tree for a, b being Vertex of T holds MiddleVertex(a,b,b) = b
proof
let T be _Tree;
let a,b be Vertex of T;
MiddleVertex(a,b,b) = MiddleVertex(b,a,b) by Th42;
hence thesis by Th49;
end;
theorem Th51:
for T being _Tree for P1, P2 be Path of T for a, b, c being
Vertex of T st P1 = T.pathBetween(a,b) & P2 = T.pathBetween(a,c) & not b in P2
.vertices() & not c in P1.vertices() holds MiddleVertex(a, b, c) = P1.len
maxPrefix(P1,P2)
proof
let T be _Tree, P1, P2 be Path of T, a, b, c be Vertex of T such that
A1: P1 = T.pathBetween(a,b) & P2 = T.pathBetween(a,c) and
A2: ( not b in P2.vertices())& not c in P1.vertices();
( not P1 c= P2)& not P2 c= P1 by A1,A2,Th37;
then
A3: T.pathBetween(a,b).vertices() /\ T.pathBetween(b,c).vertices() /\ T
.pathBetween(c,a).vertices() = { P1.len maxPrefix(P1,P2) } by A1,Lm2;
T.pathBetween(a,b).vertices() /\ T.pathBetween(b,c).vertices() /\ T
.pathBetween(c,a).vertices() = { MiddleVertex(a, b, c) } by Def3;
hence thesis by A3,ZFMISC_1:3;
end;
theorem :: PMV302:
for T being _Tree for P1, P2, P3, P4 be Path of T for a, b, c being
Vertex of T st P1 = T.pathBetween(a,b) & P2 = T.pathBetween(a,c) & P3 = T
.pathBetween(b,a) & P4 = T.pathBetween(b,c) & not b in P2.vertices() & not c in
P1.vertices() & not a in P4.vertices() holds P1.len maxPrefix(P1,P2) = P3.len
maxPrefix(P3,P4)
proof
let T be _Tree, P1, P2, P3, P4 be Path of T, a, b, c be Vertex of T such
that
A1: P1 = T.pathBetween(a,b) and
A2: P2 = T.pathBetween(a,c) and
A3: P3 = T.pathBetween(b,a) and
A4: P4 = T.pathBetween(b,c) and
A5: not b in P2.vertices() and
A6: not c in P1.vertices() and
A7: not a in P4.vertices();
now
assume P4 c= P3;
then
A8: P4.vertices() c= P3.vertices() by Th13;
c in P4.vertices() by A4,Th29;
then c in P3.vertices() by A8;
hence contradiction by A1,A3,A6,Th32;
end;
then not c in P3.vertices() by A3,A4,Th37;
then
A9: MiddleVertex(b,a,c) = P3.len maxPrefix(P3,P4) by A3,A4,A7,Th51;
MiddleVertex(a,b,c) = P1.len maxPrefix(P1,P2) by A1,A2,A5,A6,Th51;
hence thesis by A9,Th42;
end;
theorem Th53:
for T being _Tree for a, b, c being Vertex of T for S being non
empty set st for s being set st s in S holds (ex t being _Subtree of T st s =
the_Vertices_of t) & (a in s & b in s or a in s & c in s or b in s & c in s)
holds meet S <> {}
proof
let T be _Tree;
let a, b, c be Vertex of T;
let S be non empty set;
assume
A1: for s being set st s in S holds (ex t being _Subtree of T st s =
the_Vertices_of t) & (a in s & b in s or a in s & c in s or b in s & c in s);
set m = MiddleVertex(a,b,c);
set Pca = T.pathBetween(c,a);
set Pbc = T.pathBetween(b,c);
set Pac = T.pathBetween(a,c);
set Pab = T.pathBetween(a,b);
set VPab = Pab.vertices();
set VPac = Pac.vertices();
set VPbc = Pbc.vertices();
set VPca = Pca.vertices();
VPab /\ VPbc /\ VPca = {m} by Def3;
then
A2: m in VPab /\ VPbc /\ VPca by TARSKI:def 1;
then
A3: m in VPab /\ VPbc by XBOOLE_0:def 4;
then
A4: m in VPbc by XBOOLE_0:def 4;
VPca = VPac by Th32;
then
A5: m in VPac by A2,XBOOLE_0:def 4;
A6: m in VPab by A3,XBOOLE_0:def 4;
now
let s be set;
assume
A7: s in S;
then
A8: ex t being _Subtree of T st s = the_Vertices_of t by A1;
per cases by A1,A7;
suppose
a in s & b in s;
then VPab c= s by A8,Th34;
hence m in s by A6;
end;
suppose
a in s & c in s;
then VPac c= s by A8,Th34;
hence m in s by A5;
end;
suppose
b in s & c in s;
then VPbc c= s by A8,Th34;
hence m in s by A4;
end;
end;
hence thesis by SETFAM_1:def 1;
end;
begin :: The Helly property
definition
let F be set;
attr F is with_Helly_property means
for H being non empty set st H c= F &
for x, y being set st x in H & y in H holds x meets y holds meet H <> {};
end;
:: At some point one would like to define allSubtrees of a Tree
:: The claim below does not hold when T is infinite and we consider
:: infinite families of subtrees. Example: half-line tree with
:: subtrees T_i = {j >= i}.
:: main Prop4p7:
::$L https://en.wikipedia.org/wiki/Helly_family#The_Helly_property The Helly family
theorem
for T being _Tree, X being finite set st for x being set st x in X ex
t being _Subtree of T st x = the_Vertices_of t holds X is with_Helly_property
proof
let T be _Tree, X be finite set such that
A1: for x being set st x in X ex t being _Subtree of T st x =
the_Vertices_of t;
defpred P[Nat] means for H being non empty finite set st card H = $1 & H c=
X & for x, y being set st x in H & y in H holds x meets y holds meet H <> {};
A2: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat such that
A3: for n being Nat st n < k holds P[n];
let H be non empty finite set such that
A4: card H = k and
A5: H c= X and
A6: for x, y being set st x in H & y in H holds x meets y;
per cases by NAT_1:25;
suppose
k = 0;
hence thesis by A4;
end;
suppose
k = 1;
then consider x being Element of H such that
A7: H = { x } by A4,PRE_CIRC:25;
ex t being _Subtree of T st x = the_Vertices_of t by A1,A5;
hence thesis by A7,SETFAM_1:10;
end;
suppose
A8: k > 1;
set cH = the Element of H;
set A = H \ {cH};
A9: card A = card H - card {cH} by EULER_1:4
.= k - 1 by A4,CARD_1:30;
k-1 > 1-1 by A8,XREAL_1:9;
then reconsider A as non empty finite set by A9;
A10: A c= X by A5;
for x, y being set st x in A & y in A holds x meets y by A6;
then reconsider mA = meet A as non empty set by A3,A9,A10,XREAL_1:44;
set cA = the Element of A;
set B = H \ {cA};
A11: cA in A;
then
A12: card B = card H - card {cA} by EULER_1:4
.= k - 1 by A4,CARD_1:30;
set C = {cH, cA};
A13: meet C = cH /\ cA by SETFAM_1:11;
cH meets cA by A6,A11;
then reconsider mC = meet C as non empty set by A13;
k-1 > 1-1 by A8,XREAL_1:9;
then reconsider B as non empty finite set by A12;
A14: B c= X by A5;
for x, y being set st x in B & y in B holds x meets y by A6;
then reconsider mB = meet B as non empty set by A3,A12,A14,XREAL_1:44;
set a = the Element of mA, b = the Element of mB,
c = the Element of mC;
c in mC & mC c= union C by SETFAM_1:2;
then consider cc being set such that
A15: c in cc and
A16: cc in C by TARSKI:def 4;
cH in H;
then C c= X by A5,A11,A10,ZFMISC_1:32;
then
A17: ex cct being _Subtree of T st cc = the_Vertices_of cct by A1,A16;
a in mA & mA c= union A by SETFAM_1:2;
then consider aa being set such that
A18: a in aa and
A19: aa in A by TARSKI:def 4;
b in mB & mB c= union B by SETFAM_1:2;
then consider bb being set such that
A20: b in bb and
A21: bb in B by TARSKI:def 4;
A22: ex bbt being _Subtree of T st bb = the_Vertices_of bbt by A1,A14,A21;
ex aat being _Subtree of T st aa = the_Vertices_of aat by A1,A10,A19;
then reconsider a, b, c as Vertex of T by A18,A20,A22,A15,A17;
A23: cA <> cH by ZFMISC_1:56;
now
let s be set;
assume
A24: s in H;
hence ex t being _Subtree of T st s = the_Vertices_of t by A1,A5;
thus a in s & b in s or a in s & c in s or b in s & c in s
proof
per cases;
suppose
s = cH;
then s in C & s in B by A23,TARSKI:def 2,ZFMISC_1:56;
hence thesis by SETFAM_1:def 1;
end;
suppose
A25: s = cA;
then s in C by TARSKI:def 2;
hence thesis by A25,SETFAM_1:def 1;
end;
suppose
s <> cH & s <> cA;
then s in A & s in B by A24,ZFMISC_1:56;
hence thesis by SETFAM_1:def 1;
end;
end;
end;
hence thesis by Th53;
end;
end;
A26: for n being Nat holds P[n] from NAT_1:sch 4 (A2);
let H be non empty set such that
A27: H c= X and
A28: for x, y being set st x in H & y in H holds x meets y;
reconsider H9 = H as finite set by A27;
card H9 = card H9;
hence thesis by A26,A27,A28;
end;