:: HELLY semantic presentation
begin
theorem :: HELLY:1
for p being non empty FinSequence holds <*(p . 1)*> ^' p = p
proof
let p be non empty FinSequence; ::_thesis: <*(p . 1)*> ^' p = p
set o = <*(p . 1)*> ^' p;
A1: (len (<*(p . 1)*> ^' p)) + 1 = (len <*(p . 1)*>) + (len p) by GRAPH_2:13;
A2: len <*(p . 1)*> = 1 by FINSEQ_1:39;
A3: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(<*(p_._1)*>_^'_p)_holds_
(<*(p_._1)*>_^'_p)_._k_=_p_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len (<*(p . 1)*> ^' p) implies (<*(p . 1)*> ^' p) . b1 = p . b1 )
assume that
A4: 1 <= k and
A5: k <= len (<*(p . 1)*> ^' p) ; ::_thesis: (<*(p . 1)*> ^' p) . b1 = p . b1
percases ( k <= len <*(p . 1)*> or k > len <*(p . 1)*> ) ;
supposeA6: k <= len <*(p . 1)*> ; ::_thesis: (<*(p . 1)*> ^' p) . b1 = p . b1
then k <= 1 by FINSEQ_1:39;
then A7: k = 1 by A4, XXREAL_0:1;
hence (<*(p . 1)*> ^' p) . k = <*(p . 1)*> . 1 by A6, GRAPH_2:14
.= p . k by A7, FINSEQ_1:40 ;
::_thesis: verum
end;
suppose k > len <*(p . 1)*> ; ::_thesis: (<*(p . 1)*> ^' p) . b1 = p . b1
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 (<*(p . 1)*> ^' p) . k = p . k by A2, A8, A9, GRAPH_2:15; ::_thesis: verum
end;
end;
end;
(len (<*(p . 1)*> ^' p)) + 1 = 1 + (len p) by A1, FINSEQ_1:39;
hence <*(p . 1)*> ^' p = p by A3, FINSEQ_1:14; ::_thesis: verum
end;
definition
let p, q be FinSequence;
func maxPrefix (p,q) -> FinSequence means :Def1: :: HELLY:def 1
( 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
ex b1 being FinSequence st
( b1 is_a_prefix_of p & b1 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 b1 ) )
proof
deffunc H1( set ) -> set = $1;
defpred S1[ set ] means ex r being FinSequence st
( r c= p & r c= q & len r = $1 );
set S = { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } ;
A1: for x being set st x in { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } holds
x is natural
proof
let x be set ; ::_thesis: ( x in { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } implies x is natural )
assume x in { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } ; ::_thesis: x is natural
then ex n being Element of NAT st
( x = n & 0 <= n & n <= len p & S1[n] ) ;
hence x is natural ; ::_thesis: verum
end;
A2: { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } is finite from FINSEQ_1:sch_6();
( {} c= p & {} c= q & len {} = 0 ) by XBOOLE_1:2;
then 0 in { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } ;
then reconsider S = { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } as non empty finite natural-membered set by A1, A2, MEMBERED:def_6;
set maxk = max S;
max S in S by XXREAL_2:def_8;
then consider K being Element of NAT such that
A3: K = max S and
0 <= K and
K <= len p and
A4: S1[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 ; ::_thesis: ( R is_a_prefix_of p & R 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 R ) )
thus R c= p by A5; ::_thesis: ( R 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 R ) )
thus R c= q by A6; ::_thesis: for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of R
let r be FinSequence; ::_thesis: ( r is_a_prefix_of p & r is_a_prefix_of q implies r is_a_prefix_of R )
assume that
A8: r c= p and
A9: r c= q ; ::_thesis: r is_a_prefix_of R
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__::_thesis:_for_x_being_set_st_x_in_dom_r_holds_
r_._x_=_R_._x
let x be set ; ::_thesis: ( x in dom r implies r . x = R . x )
assume A11: x in dom r ; ::_thesis: r . x = R . x
hence r . x = p . x by A8, GRFUNC_1:2
.= R . x by A5, A10, A11, GRFUNC_1:2 ;
::_thesis: verum
end;
hence r is_a_prefix_of R by A10, GRFUNC_1:2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence st b1 is_a_prefix_of p & b1 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 b1 ) & b2 is_a_prefix_of p & b2 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 b2 ) holds
b1 = b2
proof
let it1, it2 be FinSequence; ::_thesis: ( it1 is_a_prefix_of p & it1 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 it1 ) & it2 is_a_prefix_of p & it2 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 it2 ) implies it1 = it2 )
assume ( it1 c= p & it1 c= q & ( for r being FinSequence st r c= p & r c= q holds
r c= it1 ) & it2 c= p & it2 c= q & ( for r being FinSequence st r c= p & r c= q holds
r c= it2 ) ) ; ::_thesis: it1 = it2
then ( it1 c= it2 & it2 c= it1 ) ;
hence it1 = it2 by XBOOLE_0:def_10; ::_thesis: verum
end;
commutativity
for b1, p, q being FinSequence st b1 is_a_prefix_of p & b1 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 b1 ) holds
( b1 is_a_prefix_of q & b1 is_a_prefix_of p & ( for r being FinSequence st r is_a_prefix_of q & r is_a_prefix_of p holds
r is_a_prefix_of b1 ) ) ;
end;
:: deftheorem Def1 defines maxPrefix HELLY:def_1_:_
for p, q, b3 being FinSequence holds
( b3 = maxPrefix (p,q) iff ( b3 is_a_prefix_of p & b3 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 b3 ) ) );
theorem :: HELLY:2
for p, q being FinSequence holds
( p is_a_prefix_of q iff maxPrefix (p,q) = p )
proof
let p, q be FinSequence; ::_thesis: ( p is_a_prefix_of q iff maxPrefix (p,q) = p )
hereby ::_thesis: ( maxPrefix (p,q) = p implies p is_a_prefix_of q )
assume p c= q ; ::_thesis: maxPrefix (p,q) = p
then A1: p c= maxPrefix (p,q) by Def1;
maxPrefix (p,q) c= p by Def1;
hence maxPrefix (p,q) = p by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
assume maxPrefix (p,q) = p ; ::_thesis: p is_a_prefix_of q
hence p is_a_prefix_of q by Def1; ::_thesis: verum
end;
theorem Th3: :: HELLY:3
for p, q being FinSequence holds len (maxPrefix (p,q)) <= len p
proof
let p, q be FinSequence; ::_thesis: len (maxPrefix (p,q)) <= len p
maxPrefix (p,q) c= p by Def1;
hence len (maxPrefix (p,q)) <= len p by FINSEQ_1:63; ::_thesis: verum
end;
theorem Th4: :: HELLY:4
for p being non empty FinSequence holds <*(p . 1)*> is_a_prefix_of p
proof
let p be non empty FinSequence; ::_thesis: <*(p . 1)*> is_a_prefix_of p
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_<*(p_._1)*>_holds_
<*(p_._1)*>_._x_=_p_._x
let x be set ; ::_thesis: ( x in dom <*(p . 1)*> implies <*(p . 1)*> . x = p . x )
A2: dom <*(p . 1)*> = Seg 1 by FINSEQ_1:def_8;
assume x in dom <*(p . 1)*> ; ::_thesis: <*(p . 1)*> . x = p . x
then x = 1 by A2, FINSEQ_1:2, TARSKI:def_1;
hence <*(p . 1)*> . x = p . x by FINSEQ_1:def_8; ::_thesis: verum
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 <*(p . 1)*> is_a_prefix_of p by A1, GRFUNC_1:2; ::_thesis: verum
end;
theorem Th5: :: HELLY:5
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; ::_thesis: ( p . 1 = q . 1 implies 1 <= len (maxPrefix (p,q)) )
assume that
A1: p . 1 = q . 1 and
A2: 1 > len (maxPrefix (p,q)) ; ::_thesis: contradiction
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; ::_thesis: verum
end;
theorem Th6: :: HELLY:6
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; ::_thesis: for j being Nat st j <= len (maxPrefix (p,q)) holds
(maxPrefix (p,q)) . j = p . j
let j be Nat; ::_thesis: ( j <= len (maxPrefix (p,q)) implies (maxPrefix (p,q)) . j = p . j )
assume A1: j <= len (maxPrefix (p,q)) ; ::_thesis: (maxPrefix (p,q)) . j = p . j
A2: maxPrefix (p,q) c= p by Def1;
percases ( j = 0 or j <> 0 ) ;
supposeA3: j = 0 ; ::_thesis: (maxPrefix (p,q)) . j = p . j
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 ;
::_thesis: verum
end;
suppose j <> 0 ; ::_thesis: (maxPrefix (p,q)) . j = p . j
then 0 + 1 <= j by NAT_1:13;
then j in dom (maxPrefix (p,q)) by A1, FINSEQ_3:25;
hence (maxPrefix (p,q)) . j = p . j by A2, GRFUNC_1:2; ::_thesis: verum
end;
end;
end;
theorem Th7: :: HELLY:7
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; ::_thesis: for j being Nat st j <= len (maxPrefix (p,q)) holds
p . j = q . j
let j be Nat; ::_thesis: ( j <= len (maxPrefix (p,q)) implies p . j = q . j )
assume A1: j <= len (maxPrefix (p,q)) ; ::_thesis: p . j = q . j
thus p . j = (maxPrefix (p,q)) . j by A1, Th6
.= q . j by A1, Th6 ; ::_thesis: verum
end;
theorem Th8: :: HELLY:8
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; ::_thesis: ( not p is_a_prefix_of q iff len (maxPrefix (p,q)) < len p )
A1: maxPrefix (p,q) c= p by Def1;
hereby ::_thesis: ( len (maxPrefix (p,q)) < len p implies not p is_a_prefix_of q )
assume A2: not p c= q ; ::_thesis: len (maxPrefix (p,q)) < len p
A3: now__::_thesis:_not_len_(maxPrefix_(p,q))_=_len_p
assume len (maxPrefix (p,q)) = len p ; ::_thesis: contradiction
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; ::_thesis: verum
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; ::_thesis: verum
end;
assume that
A5: len (maxPrefix (p,q)) < len p and
A6: p c= q ; ::_thesis: contradiction
p c= maxPrefix (p,q) by A6, Def1;
hence contradiction by A5, A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th9: :: HELLY:9
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; ::_thesis: ( not p is_a_prefix_of q & not q is_a_prefix_of p implies p . ((len (maxPrefix (p,q))) + 1) <> q . ((len (maxPrefix (p,q))) + 1) )
assume 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) ; ::_thesis: contradiction
set dI = len (maxPrefix (p,q));
set mP = maxPrefix (p,q);
set lmP = (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>;
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_((maxPrefix_(p,q))_^_<*(p_._((len_(maxPrefix_(p,q)))_+_1))*>)_holds_
((maxPrefix_(p,q))_^_<*(p_._((len_(maxPrefix_(p,q)))_+_1))*>)_._x_=_q_._x
let x be set ; ::_thesis: ( x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) implies ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1 )
assume A5: x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1
reconsider n = x as Nat by A5;
A6: 1 <= n by A5, FINSEQ_3:25;
n <= len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) by A5, FINSEQ_3:25;
then A7: n <= (len (maxPrefix (p,q))) + 1 by FINSEQ_2:16;
percases ( n <= len (maxPrefix (p,q)) or n = (len (maxPrefix (p,q))) + 1 ) by A7, NAT_1:8;
supposeA8: n <= len (maxPrefix (p,q)) ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1
then n in dom (maxPrefix (p,q)) by A6, FINSEQ_3:25;
hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = (maxPrefix (p,q)) . x by FINSEQ_1:def_7
.= q . x by A8, Th6 ;
::_thesis: verum
end;
suppose n = (len (maxPrefix (p,q))) + 1 ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1
hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = q . x by A3, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
A9: now__::_thesis:_for_x_being_set_st_x_in_dom_((maxPrefix_(p,q))_^_<*(p_._((len_(maxPrefix_(p,q)))_+_1))*>)_holds_
((maxPrefix_(p,q))_^_<*(p_._((len_(maxPrefix_(p,q)))_+_1))*>)_._x_=_p_._x
let x be set ; ::_thesis: ( x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) implies ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1 )
assume A10: x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1
reconsider n = x as Nat by A10;
A11: 1 <= n by A10, FINSEQ_3:25;
n <= len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) by A10, FINSEQ_3:25;
then A12: n <= (len (maxPrefix (p,q))) + 1 by FINSEQ_2:16;
percases ( n <= len (maxPrefix (p,q)) or n = (len (maxPrefix (p,q))) + 1 ) by A12, NAT_1:8;
supposeA13: n <= len (maxPrefix (p,q)) ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1
then n in dom (maxPrefix (p,q)) by A11, FINSEQ_3:25;
hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = (maxPrefix (p,q)) . x by FINSEQ_1:def_7
.= p . x by A13, Th6 ;
::_thesis: verum
end;
suppose n = (len (maxPrefix (p,q))) + 1 ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1
hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = p . x by FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
A14: len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) = (len (maxPrefix (p,q))) + 1 by FINSEQ_2:16;
len (maxPrefix (p,q)) < len q by A2, Th8;
then len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) <= len q by A14, NAT_1:13;
then dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) c= dom q by FINSEQ_3:30;
then A15: (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*> c= q by A4, GRFUNC_1:2;
len (maxPrefix (p,q)) < len p by A1, Th8;
then len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) <= len p by A14, NAT_1:13;
then dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) c= dom p by FINSEQ_3:30;
then (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*> c= p by A9, GRFUNC_1:2;
then (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*> c= maxPrefix (p,q) by A15, Def1;
then len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) <= len (maxPrefix (p,q)) by FINSEQ_1:63;
then (len (maxPrefix (p,q))) + 1 <= len (maxPrefix (p,q)) by FINSEQ_2:16;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
begin
theorem Th10: :: HELLY:10
for G being _Graph
for W being Walk of G
for m, n being Nat holds len (W .cut (m,n)) <= len W
proof
let G be _Graph; ::_thesis: for W being Walk of G
for m, n being Nat holds len (W .cut (m,n)) <= len W
let W be Walk of G; ::_thesis: for m, n being Nat holds len (W .cut (m,n)) <= len W
let m, n be Nat; ::_thesis: len (W .cut (m,n)) <= len W
reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def_12;
percases ( ( m is odd & n is odd & m <= n & n <= len W ) or not m is odd or not n is odd or not m <= n or not n <= len W ) ;
suppose ( m is odd & n is odd & m <= n & n <= len W ) ; ::_thesis: len (W .cut (m,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 len (W .cut (m,n)) <= len W ; ::_thesis: verum
end;
suppose ( not m is odd or not n is odd or not m <= n or not n <= len W ) ; ::_thesis: len (W .cut (m,n)) <= len W
hence len (W .cut (m,n)) <= len W by GLIB_001:def_11; ::_thesis: verum
end;
end;
end;
theorem :: HELLY:11
for G being _Graph
for W being Walk of G
for m, n being Nat st not W .cut (m,n) is trivial holds
not W is trivial
proof
let G be _Graph; ::_thesis: for W being Walk of G
for m, n being Nat st not W .cut (m,n) is trivial holds
not W is trivial
let W be Walk of G; ::_thesis: for m, n being Nat st not W .cut (m,n) is trivial holds
not W is trivial
let m, n be Nat; ::_thesis: ( not W .cut (m,n) is trivial implies not W is trivial )
assume that
A1: not W .cut (m,n) is trivial and
A2: W is trivial ; ::_thesis: contradiction
reconsider W = 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 contradiction by A1; ::_thesis: verum
end;
theorem Th12: :: HELLY:12
for G being _Graph
for W being Walk of G
for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds
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; ::_thesis: for W being Walk of G
for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds
ex j being odd Nat st
( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )
let W be Walk of G; ::_thesis: for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds
ex j being odd Nat st
( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )
let m, n, i be odd Nat; ::_thesis: ( m <= n & n <= len W & i <= len (W .cut (m,n)) implies ex j being odd Nat st
( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W ) )
assume that
A1: m <= n and
A2: n <= len W and
A3: i <= len (W .cut (m,n)) ; ::_thesis: ex j being odd Nat st
( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )
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 (m + i) - 1 is odd Element of NAT by INT_1:3;
then reconsider j = (m + i) - 1 as odd Nat ;
take j ; ::_thesis: ( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )
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 ; ::_thesis: ( j = (m + i) - 1 & j <= len W )
thus j = (m + i) - 1 ; ::_thesis: j <= len W
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 j <= len W by A2, XXREAL_0:2; ::_thesis: verum
end;
registration
let G be _Graph;
cluster -> non empty for Walk of G;
correctness
coherence
for b1 being Walk of G holds not b1 is empty ;
by CARD_1:27;
end;
theorem Th13: :: HELLY:13
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; ::_thesis: for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds
W1 .vertices() c= W2 .vertices()
let W1, W2 be Walk of G; ::_thesis: ( W1 is_a_prefix_of W2 implies W1 .vertices() c= W2 .vertices() )
assume A1: W1 c= W2 ; ::_thesis: W1 .vertices() c= W2 .vertices()
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W1 .vertices() or x in W2 .vertices() )
assume x in W1 .vertices() ; ::_thesis: x in W2 .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 x in W2 .vertices() by A4, GLIB_001:87; ::_thesis: verum
end;
theorem :: HELLY:14
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; ::_thesis: for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds
W1 .edges() c= W2 .edges()
let W1, W2 be Walk of G; ::_thesis: ( W1 is_a_prefix_of W2 implies W1 .edges() c= W2 .edges() )
assume A1: W1 c= W2 ; ::_thesis: W1 .edges() c= W2 .edges()
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W1 .edges() or x in W2 .edges() )
assume x in W1 .edges() ; ::_thesis: x in W2 .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 x in W2 .edges() by A2, A5, GLIB_001:99; ::_thesis: verum
end;
theorem Th15: :: HELLY:15
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; ::_thesis: for W1, W2 being Walk of G holds W1 is_a_prefix_of W1 .append W2
let W1, W2 be Walk of G; ::_thesis: W1 is_a_prefix_of W1 .append W2
set W1a = W1 .append W2;
percases ( W1 .last() = W2 .first() or W1 .last() <> W2 .first() ) ;
suppose W1 .last() = W2 .first() ; ::_thesis: W1 is_a_prefix_of W1 .append W2
then len W1 <= len (W1 .append W2) by GLIB_001:29;
then A1: dom W1 c= dom (W1 .append W2) by FINSEQ_3:30;
for x being set st x in dom W1 holds
W1 . x = (W1 .append W2) . x by GLIB_001:32;
hence W1 is_a_prefix_of W1 .append W2 by A1, GRFUNC_1:2; ::_thesis: verum
end;
suppose W1 .last() <> W2 .first() ; ::_thesis: W1 is_a_prefix_of W1 .append W2
hence W1 is_a_prefix_of W1 .append W2 by GLIB_001:def_10; ::_thesis: verum
end;
end;
end;
theorem Th16: :: HELLY:16
for G being _Graph
for W1, W2 being Walk of G st W1 is trivial & W1 .last() = W2 .first() holds
W1 .append W2 = W2
proof
let G be _Graph; ::_thesis: for W1, W2 being Walk of G st W1 is trivial & W1 .last() = W2 .first() holds
W1 .append W2 = W2
let W1, W2 be Walk of G; ::_thesis: ( W1 is trivial & W1 .last() = W2 .first() implies W1 .append W2 = W2 )
assume that
A1: W1 is trivial and
A2: W1 .last() = W2 .first() ; ::_thesis: W1 .append W2 = W2
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__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(W1_.append_W2)_holds_
(W1_.append_W2)_._k_=_W2_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len (W1 .append W2) implies (W1 .append W2) . k = W2 . k )
assume that
A5: 1 <= k and
A6: k <= len (W1 .append W2) ; ::_thesis: (W1 .append W2) . k = W2 . k
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 ; ::_thesis: verum
end;
hence W1 .append W2 = W2 by A4, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th17: :: HELLY:17
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; ::_thesis: for W1, W2 being Trail of G st W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() holds
W1 .append W2 is Trail-like
let W1, W2 be Trail of G; ::_thesis: ( W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() implies W1 .append W2 is Trail-like )
assume that
A1: W1 .last() = W2 .first() and
A2: W1 .edges() misses W2 .edges() ; ::_thesis: W1 .append W2 is Trail-like
set W = W1 .append W2;
now__::_thesis:_for_m,_n_being_even_Element_of_NAT_st_1_<=_m_&_m_<_n_&_n_<=_len_(W1_.append_W2)_holds_
(W1_.append_W2)_._m_<>_(W1_.append_W2)_._n
let m, n be even Element of NAT ; ::_thesis: ( 1 <= m & m < n & n <= len (W1 .append W2) implies (W1 .append W2) . b1 <> (W1 .append W2) . b2 )
assume that
A3: 1 <= m and
A4: m < n and
A5: n <= len (W1 .append W2) ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
1 <= n by A3, A4, XXREAL_0:2;
then A6: n in dom (W1 .append W2) by A5, FINSEQ_3:25;
m <= len (W1 .append W2) by A4, A5, XXREAL_0:2;
then A7: m in dom (W1 .append W2) by A3, FINSEQ_3:25;
percases ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ) by A6, GLIB_001:34;
supposeA8: n in dom W1 ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
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 = (W1 .append W2) . m by GLIB_001:32;
W1 . m <> W1 . n by A3, A4, A9, GLIB_001:138;
hence (W1 .append W2) . m <> (W1 .append W2) . n by A8, A10, GLIB_001:32; ::_thesis: verum
end;
suppose ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
then consider k being Element of NAT such that
A11: k < len W2 and
A12: n = (len W1) + k ;
reconsider k = k as odd Element of NAT by A12;
A13: (W1 .append W2) . 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;
percases ( m in dom W1 or ex l being Element of NAT st
( l < len W2 & m = (len W1) + l ) ) by A7, GLIB_001:34;
supposeA16: m in dom W1 ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
then ( 1 <= m & m <= len W1 ) by FINSEQ_3:25;
then A17: W1 . m in W1 .edges() by GLIB_001:99;
(W1 .append W2) . m = W1 . m by A16, GLIB_001:32;
hence (W1 .append W2) . m <> (W1 .append W2) . n by A2, A13, A15, A17, XBOOLE_0:3; ::_thesis: verum
end;
suppose ex l being Element of NAT st
( l < len W2 & m = (len W1) + l ) ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
then consider l being Element of NAT such that
A18: l < len W2 and
A19: m = (len W1) + l ;
reconsider l = 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;
(W1 .append W2) . m = W2 . (l + 1) by A1, A18, A19, GLIB_001:33;
hence (W1 .append W2) . m <> (W1 .append W2) . n by A13, A14, A20, GLIB_001:138; ::_thesis: verum
end;
end;
end;
end;
end;
hence W1 .append W2 is Trail-like by GLIB_001:138; ::_thesis: verum
end;
theorem Th18: :: HELLY:18
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; ::_thesis: 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
let P1, P2 be Path of G; ::_thesis: ( 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())} implies P1 .append P2 is Path-like )
assume 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())} ; ::_thesis: P1 .append P2 is Path-like
thus P1 .append P2 is Trail-like by A1, A4, Th17; :: according to GLIB_001:def_28 ::_thesis: for b1, b2 being Element of NAT holds
( b2 <= b1 or not b2 <= len (P1 .append P2) or not (P1 .append P2) . b1 = (P1 .append P2) . b2 or ( b1 = 1 & b2 = len (P1 .append P2) ) )
set P = P1 .append P2;
let m, n be odd Element of NAT ; ::_thesis: ( n <= m or not n <= len (P1 .append P2) or not (P1 .append P2) . m = (P1 .append P2) . n or ( m = 1 & n = len (P1 .append P2) ) )
assume that
A7: m < n and
A8: n <= len (P1 .append P2) and
A9: (P1 .append P2) . m = (P1 .append P2) . n and
A10: ( m <> 1 or n <> len (P1 .append P2) ) ; ::_thesis: contradiction
A11: 1 <= m by ABIAN:12;
1 <= n by ABIAN:12;
then A12: n in dom (P1 .append P2) by A8, FINSEQ_3:25;
m <= len (P1 .append P2) by A7, A8, XXREAL_0:2;
then A13: m in dom (P1 .append P2) by A11, FINSEQ_3:25;
percases ( ex k being Element of NAT st
( k < len P2 & n = (len P1) + k ) or n in dom P1 ) by A12, GLIB_001:34;
suppose ex k being Element of NAT st
( k < len P2 & n = (len P1) + k ) ; ::_thesis: contradiction
then consider k being Element of NAT such that
A14: k < len P2 and
A15: n = (len P1) + k ;
A16: (P1 .append P2) . n = P2 . (k + 1) by A1, A14, A15, GLIB_001:33;
reconsider k = 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;
percases ( ex k being Element of NAT st
( k < len P2 & m = (len P1) + k ) or m in dom P1 ) by A13, GLIB_001:34;
suppose ex k being Element of NAT st
( k < len P2 & m = (len P1) + k ) ; ::_thesis: contradiction
then consider l being Element of NAT such that
A19: l < len P2 and
A20: m = (len P1) + l ;
A21: (P1 .append P2) . 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 = 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, GLIB_001:def_24; ::_thesis: verum
end;
supposeA24: m in dom P1 ; ::_thesis: contradiction
set x = P1 . m;
A25: P1 . m = (P1 .append P2) . 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: P1 . m in (P1 .vertices()) /\ (P2 .vertices()) by A9, A16, A18, A25, XBOOLE_0:def_4;
percases ( P1 . m = P1 .last() or P1 . m = P1 .first() ) by A6, A27, TARSKI:def_2;
supposeA28: P1 . m = P1 .last() ; ::_thesis: contradiction
A29: now__::_thesis:_not_m_<_len_P1
assume m < len P1 ; ::_thesis: contradiction
then P1 .first() = P1 . m by A28, GLIB_001:def_28;
hence contradiction by A2, A28, GLIB_001:def_24; ::_thesis: verum
end;
A30: now__::_thesis:_not_(2_*_0)_+_1_<_k_+_1
assume (2 * 0) + 1 < k + 1 ; ::_thesis: contradiction
then P2 .first() = P2 .last() by A1, A9, A16, A17, A25, A28, GLIB_001:def_28;
hence contradiction by A3, GLIB_001:def_24; ::_thesis: verum
end;
1 <= k + 1 by NAT_1:11;
then 1 = k + 1 by A30, XXREAL_0:1;
hence contradiction by A7, A15, A29; ::_thesis: verum
end;
supposeA31: P1 . m = P1 .first() ; ::_thesis: contradiction
then A32: P1 . m = P1 . ((2 * 0) + 1) ;
A33: now__::_thesis:_not_m_<>_1
assume m <> 1 ; ::_thesis: contradiction
then 1 < m by A11, XXREAL_0:1;
then P1 . m = P1 .last() by A26, A32, GLIB_001:def_28;
hence contradiction by A2, A31, GLIB_001:def_24; ::_thesis: verum
end;
now__::_thesis:_not_k_+_1_=_len_P2
assume k + 1 = len P2 ; ::_thesis: contradiction
then (len (P1 .append P2)) + 1 = (len P1) + (k + 1) by A1, GLIB_001:28;
hence contradiction by A10, A15, A33; ::_thesis: verum
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, GLIB_001:def_24; ::_thesis: verum
end;
end;
end;
end;
end;
supposeA35: n in dom P1 ; ::_thesis: contradiction
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 = (P1 .append P2) . 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, GLIB_001:def_24; ::_thesis: verum
end;
end;
end;
theorem Th19: :: HELLY:19
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 & P1 .append P2 is Path-like )
proof
let G be _Graph; ::_thesis: 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 & P1 .append P2 is Path-like )
let P1, P2 be Path of G; ::_thesis: ( P1 .last() = P2 .first() & P1 is open & P2 is open & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} implies ( P1 .append P2 is open & P1 .append P2 is Path-like ) )
assume that
A1: P1 .last() = P2 .first() and
A2: P1 is open and
A3: P2 is open and
A4: (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} ; ::_thesis: ( P1 .append P2 is open & P1 .append P2 is Path-like )
set P = P1 .append P2;
thus P1 .append P2 is open ::_thesis: P1 .append P2 is Path-like
proof
assume A5: (P1 .append P2) .first() = (P1 .append P2) .last() ; :: according to GLIB_001:def_24 ::_thesis: contradiction
( (P1 .append P2) .first() = P1 .first() & (P1 .append P2) .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, GLIB_001:def_24; ::_thesis: verum
end;
A6: now__::_thesis:_not_P1_.first()_in_P2_.vertices()
A7: P1 .first() in P1 .vertices() by GLIB_001:88;
assume P1 .first() in P2 .vertices() ; ::_thesis: contradiction
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, GLIB_001:def_24; ::_thesis: verum
end;
A8: P1 .edges() misses P2 .edges()
proof
assume (P1 .edges()) /\ (P2 .edges()) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being set 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;
percases ( v1 <> v2 or v1 = v2 ) ;
supposeA19: v1 <> v2 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
supposeA25: v1 = v2 ; ::_thesis: contradiction
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, GLIB_001:def_24; ::_thesis: verum
end;
end;
end;
(P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} by A4, ZFMISC_1:7;
hence P1 .append P2 is Path-like by A1, A2, A3, A8, A6, Th18; ::_thesis: verum
end;
theorem Th20: :: HELLY:20
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; ::_thesis: 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
let P1, P2 be Path of G; ::_thesis: ( 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())} implies P1 .append P2 is Cycle-like )
assume 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())} ) ; ::_thesis: P1 .append P2 is Cycle-like
set P = P1 .append P2;
( (P1 .append P2) .first() = P1 .first() & (P1 .append P2) .last() = P2 .last() ) by A1, GLIB_001:30;
hence P1 .append P2 is closed by A2, GLIB_001:def_24; :: according to GLIB_001:def_31 ::_thesis: ( P1 .append P2 is Path-like & not P1 .append P2 is trivial )
thus P1 .append P2 is Path-like by A1, A2, A3, A4, Th18; ::_thesis: not P1 .append P2 is trivial
P1 .first() <> P1 .last() by A3, GLIB_001:def_24;
then not P1 is trivial by GLIB_001:127;
then A5: len P1 >= 3 by GLIB_001:125;
len (P1 .append P2) >= len P1 by A1, GLIB_001:29;
then len (P1 .append P2) >= 3 by A5, XXREAL_0:2;
hence not P1 .append P2 is trivial by GLIB_001:125; ::_thesis: verum
end;
theorem :: HELLY:21
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; ::_thesis: 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
let W1, W2 be Walk of G; ::_thesis: 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
let k be odd Nat; ::_thesis: ( k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds
W1 . j = W2 . j ) implies for j being Nat st 1 <= j & j <= k holds
W1 . j = W2 . j )
assume 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 ; ::_thesis: for j being Nat st 1 <= j & j <= k holds
W1 . j = W2 . j
let j be Nat; ::_thesis: ( 1 <= j & j <= k implies W1 . j = W2 . j )
assume that
A4: 1 <= j and
A5: j <= k ; ::_thesis: W1 . j = W2 . j
percases ( j is odd or j is even ) ;
suppose j is odd ; ::_thesis: W1 . j = W2 . j
hence W1 . j = W2 . j by A3, A5; ::_thesis: verum
end;
suppose j is even ; ::_thesis: W1 . j = W2 . j
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 W1 . j = W2 . j by A7, A9, A8, GLIB_000:def_20; ::_thesis: verum
end;
end;
end;
theorem Th22: :: HELLY:22
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; ::_thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() holds
len (maxPrefix (W1,W2)) is odd
let W1, W2 be Walk of G; ::_thesis: ( W1 .first() = W2 .first() implies len (maxPrefix (W1,W2)) is odd )
assume that
A1: W1 .first() = W2 .first() and
A2: len (maxPrefix (W1,W2)) is even ; ::_thesis: contradiction
set dI = len (maxPrefix (W1,W2));
reconsider dIp = (len (maxPrefix (W1,W2))) - 1 as odd Element of NAT by A1, A2, Th5, INT_1:5;
A3: dIp < len (maxPrefix (W1,W2)) by XREAL_1:146;
set mP = maxPrefix (W1,W2);
set lmP = (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>;
A4: len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) = (len (maxPrefix (W1,W2))) + 1 by FINSEQ_2:16;
A5: now__::_thesis:_for_x_being_set_st_x_in_dom_((maxPrefix_(W1,W2))_^_<*(W1_._((len_(maxPrefix_(W1,W2)))_+_1))*>)_holds_
((maxPrefix_(W1,W2))_^_<*(W1_._((len_(maxPrefix_(W1,W2)))_+_1))*>)_._x_=_W1_._x
let x be set ; ::_thesis: ( x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) implies ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1 )
assume A6: x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1
reconsider n = x as Nat by A6;
A7: 1 <= n by A6, FINSEQ_3:25;
n <= len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) by A6, FINSEQ_3:25;
then A8: n <= (len (maxPrefix (W1,W2))) + 1 by FINSEQ_2:16;
percases ( n <= len (maxPrefix (W1,W2)) or n = (len (maxPrefix (W1,W2))) + 1 ) by A8, NAT_1:8;
supposeA9: n <= len (maxPrefix (W1,W2)) ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1
then n in dom (maxPrefix (W1,W2)) by A7, FINSEQ_3:25;
hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = (maxPrefix (W1,W2)) . x by FINSEQ_1:def_7
.= W1 . x by A9, Th6 ;
::_thesis: verum
end;
suppose n = (len (maxPrefix (W1,W2))) + 1 ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1
hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = W1 . x by FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
A10: len (maxPrefix (W1,W2)) = dIp + 1 ;
A11: len (maxPrefix (W1,W2)) <= len W2 by Th3;
then dIp < len W2 by XREAL_1:146, XXREAL_0:2;
then A12: W2 . (len (maxPrefix (W1,W2))) Joins W2 . dIp,W2 . (dIp + 2),G by A10, GLIB_001:def_3;
A13: len (maxPrefix (W1,W2)) <= len W1 by Th3;
then dIp < len W1 by XREAL_1:146, XXREAL_0:2;
then A14: W1 . (len (maxPrefix (W1,W2))) Joins W1 . dIp,W1 . (dIp + 2),G by A10, GLIB_001:def_3;
W1 . (len (maxPrefix (W1,W2))) = W2 . (len (maxPrefix (W1,W2))) 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__::_thesis:_for_x_being_set_st_x_in_dom_((maxPrefix_(W1,W2))_^_<*(W1_._((len_(maxPrefix_(W1,W2)))_+_1))*>)_holds_
((maxPrefix_(W1,W2))_^_<*(W1_._((len_(maxPrefix_(W1,W2)))_+_1))*>)_._x_=_W2_._x
let x be set ; ::_thesis: ( x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) implies ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1 )
assume A17: x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1
reconsider n = x as Nat by A17;
A18: 1 <= n by A17, FINSEQ_3:25;
n <= len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) by A17, FINSEQ_3:25;
then A19: n <= (len (maxPrefix (W1,W2))) + 1 by FINSEQ_2:16;
percases ( n <= len (maxPrefix (W1,W2)) or n = (len (maxPrefix (W1,W2))) + 1 ) by A19, NAT_1:8;
supposeA20: n <= len (maxPrefix (W1,W2)) ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1
then n in dom (maxPrefix (W1,W2)) by A18, FINSEQ_3:25;
hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = (maxPrefix (W1,W2)) . x by FINSEQ_1:def_7
.= W2 . x by A20, Th6 ;
::_thesis: verum
end;
supposeA21: n = (len (maxPrefix (W1,W2))) + 1 ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1
hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = W1 . ((len (maxPrefix (W1,W2))) + 1) by FINSEQ_1:42
.= W2 . x by A3, A15, A21, Th7 ;
::_thesis: verum
end;
end;
end;
len (maxPrefix (W1,W2)) < len W2 by A2, A11, XXREAL_0:1;
then len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) <= len W2 by A4, NAT_1:13;
then dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) c= dom W2 by FINSEQ_3:30;
then A22: (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*> c= W2 by A16, GRFUNC_1:2;
len (maxPrefix (W1,W2)) < len W1 by A2, A13, XXREAL_0:1;
then len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) <= len W1 by A4, NAT_1:13;
then dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) c= dom W1 by FINSEQ_3:30;
then (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*> c= W1 by A5, GRFUNC_1:2;
then (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*> c= maxPrefix (W1,W2) by A22, Def1;
then len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) <= len (maxPrefix (W1,W2)) by FINSEQ_1:63;
then (len (maxPrefix (W1,W2))) + 1 <= len (maxPrefix (W1,W2)) by FINSEQ_2:16;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
theorem Th23: :: HELLY:23
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; ::_thesis: 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
let W1, W2 be Walk of G; ::_thesis: ( W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 implies (len (maxPrefix (W1,W2))) + 2 <= len W1 )
assume ( W1 .first() = W2 .first() & not W1 c= W2 ) ; ::_thesis: (len (maxPrefix (W1,W2))) + 2 <= len W1
then ( len (maxPrefix (W1,W2)) < len W1 & len (maxPrefix (W1,W2)) is odd Nat ) by Th8, Th22;
hence (len (maxPrefix (W1,W2))) + 2 <= len W1 by CHORD:4; ::_thesis: verum
end;
theorem Th24: :: HELLY:24
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; ::_thesis: 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)
let W1, W2 be Walk of G; ::_thesis: ( W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 implies W1 . ((len (maxPrefix (W1,W2))) + 2) <> W2 . ((len (maxPrefix (W1,W2))) + 2) )
assume 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) ; ::_thesis: contradiction
set dI = len (maxPrefix (W1,W2));
A5: len (maxPrefix (W1,W2)) is odd by A1, Th22;
len (maxPrefix (W1,W2)) < len W1 by A2, Th8;
then A6: W1 . ((len (maxPrefix (W1,W2))) + 1) Joins W1 . (len (maxPrefix (W1,W2))),W1 . ((len (maxPrefix (W1,W2))) + 2),G by A5, GLIB_001:def_3;
A7: W1 . (len (maxPrefix (W1,W2))) = W2 . (len (maxPrefix (W1,W2))) by Th7;
len (maxPrefix (W1,W2)) < len W2 by A3, Th8;
then A8: W2 . ((len (maxPrefix (W1,W2))) + 1) Joins W2 . (len (maxPrefix (W1,W2))),W2 . ((len (maxPrefix (W1,W2))) + 2),G by A5, GLIB_001:def_3;
W1 . ((len (maxPrefix (W1,W2))) + 1) <> W2 . ((len (maxPrefix (W1,W2))) + 1) by A2, A3, Th9;
hence contradiction by A4, A7, A6, A8, GLIB_000:def_20; ::_thesis: verum
end;
begin
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
coherence
for b1 being Walk of T st b1 is Trail-like holds
b1 is Path-like ;
proof
let W be Walk of T; ::_thesis: ( W is Trail-like implies W is Path-like )
assume A1: W is Trail-like ; ::_thesis: W is Path-like
defpred S1[ Nat] means ( T is odd & T <= len W & ex k being odd Element of NAT st
( k < T & W . k = W . T ) );
assume not W is Path-like ; ::_thesis: contradiction
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, GLIB_001:def_28;
then A2: ex p being Nat st S1[p] ;
consider p being Nat such that
A3: S1[p] and
A4: for r being Nat st S1[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 (W .cut (k,P))) + k = P + 1 by A3, A5, GLIB_001:36;
then len (W .cut (k,P)) <> 1 by A5;
then A7: not W .cut (k,P) is trivial by GLIB_001:126;
A8: (W .cut (k,P)) .last() = W . p by A3, A5, GLIB_001:37;
A9: W .cut (k,P) is Path-like
proof
assume not W .cut (k,P) is Path-like ; ::_thesis: contradiction
then consider m, n being odd Element of NAT such that
A10: m < n and
A11: n <= len (W .cut (k,P)) and
A12: (W .cut (k,P)) . m = (W .cut (k,P)) . n and
A13: ( m <> 1 or n <> len (W .cut (k,P)) ) by A1, GLIB_001:def_28;
A14: m < len (W .cut (k,P)) by A10, A11, XXREAL_0:2;
consider kn1 being odd Nat such that
A15: (W .cut (k,P)) . n = W . kn1 and
A16: kn1 = (k + n) - 1 and
A17: kn1 <= len W by A3, A5, A11, Th12;
reconsider kn1 = kn1 as odd Element of NAT by ORDINAL1:def_12;
A18: 1 <= m by ABIAN:12;
m <= len (W .cut (k,P)) by A10, A11, XXREAL_0:2;
then consider km1 being odd Nat such that
A19: (W .cut (k,P)) . m = W . km1 and
A20: km1 = (k + m) - 1 and
A21: km1 <= len W by A3, A5, Th12;
reconsider km1 = km1 as odd Element of NAT by ORDINAL1:def_12;
percases ( n < len (W .cut (k,P)) or n = len (W .cut (k,P)) ) by A11, XXREAL_0:1;
suppose n < len (W .cut (k,P)) ; ::_thesis: contradiction
then k + n < k + (len (W .cut (k,P))) 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; ::_thesis: verum
end;
supposeA23: n = len (W .cut (k,P)) ; ::_thesis: contradiction
k + m < (len (W .cut (k,P))) + 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; ::_thesis: verum
end;
end;
end;
(W .cut (k,P)) .first() = W . k by A3, A5, GLIB_001:37;
then W .cut (k,P) is closed by A6, A8, GLIB_001:def_24;
then W .cut (k,P) is Cycle-like by A7, A9, GLIB_001:def_31;
hence contradiction by GLIB_002:def_2; ::_thesis: verum
end;
end;
theorem Th25: :: HELLY:25
for T being _Tree
for P being Path of T st not P is trivial holds
P is open
proof
let T be _Tree; ::_thesis: for P being Path of T st not P is trivial holds
P is open
let P be Path of T; ::_thesis: ( not P is trivial implies P is open )
assume ( not P is trivial & not P is open ) ; ::_thesis: contradiction
then P is Cycle-like by GLIB_001:def_31;
hence contradiction by GLIB_002:def_2; ::_thesis: verum
end;
registration
let T be _Tree;
cluster non trivial Path-like -> open for Walk of T;
correctness
coherence
for b1 being Path of T st not b1 is trivial holds
b1 is open ;
by Th25;
end;
theorem Th26: :: HELLY:26
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; ::_thesis: for P being Path of T
for i, j being odd Nat st i < j & j <= len P holds
P . i <> P . j
let P be Path of T; ::_thesis: for i, j being odd Nat st i < j & j <= len P holds
P . i <> P . j
let i, j be odd Nat; ::_thesis: ( i < j & j <= len P implies P . i <> P . j )
assume that
A1: i < j and
A2: j <= len P and
A3: P . i = P . j ; ::_thesis: contradiction
reconsider i = i, j = 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: not P is 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; ::_thesis: verum
end;
theorem Th27: :: HELLY:27
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; ::_thesis: 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
let a, b be Vertex of T; ::_thesis: for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds
P1 = P2
let P1, P2 be Path of T; ::_thesis: ( P1 is_Walk_from a,b & P2 is_Walk_from a,b implies P1 = P2 )
assume that
A1: P1 is_Walk_from a,b and
A2: P2 is_Walk_from a,b ; ::_thesis: P1 = P2
set di = len (maxPrefix (P1,P2));
A3: ( P1 .first() = a & P2 .first() = a ) by A1, A2, GLIB_001:def_23;
then reconsider di = len (maxPrefix (P1,P2)) as odd Element of NAT by Th22;
defpred S1[ Nat] means ( $1 is odd & di < $1 & $1 <= len P2 & P2 . $1 in P1 .vertices() );
assume A4: P1 <> P2 ; ::_thesis: contradiction
A5: not P2 c= P1
proof
assume A6: P2 c= P1 ; ::_thesis: contradiction
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, GLIB_001:def_23 ;
P2 . (len P2) = P2 .last()
.= b by A2, GLIB_001:def_23 ;
hence contradiction by A7, A8, A9, Th26; ::_thesis: verum
end;
A10: ex k being Nat st S1[k]
proof
take k = len P2; ::_thesis: S1[k]
thus k is odd ; ::_thesis: ( di < k & k <= len P2 & P2 . k in P1 .vertices() )
( di + 2 <= len P2 & di < di + 2 ) by A3, A5, Th23, NAT_1:19;
hence di < k by XXREAL_0:2; ::_thesis: ( k <= len P2 & P2 . k in P1 .vertices() )
thus k <= len P2 ; ::_thesis: P2 . k in P1 .vertices()
P2 . k = P2 .last()
.= b by A2, GLIB_001:def_23
.= P1 .last() by A1, GLIB_001:def_23 ;
hence P2 . k in P1 .vertices() by GLIB_001:88; ::_thesis: verum
end;
consider ei being Nat such that
A11: S1[ei] and
A12: for n being Nat st S1[n] holds
ei <= n from NAT_1:sch_5(A10);
reconsider ei = ei as odd Element of NAT by A11, ORDINAL1:def_12;
set e = P2 . ei;
set fi = P1 .find (P2 . ei);
set pde = P2 .cut (di,ei);
set pdf = P1 .cut (di,(P1 .find (P2 . ei)));
A13: P1 .find (P2 . ei) <= len P1 by A11, GLIB_001:def_19;
set rpdf = (P1 .cut (di,(P1 .find (P2 . ei)))) .reverse() ;
A14: ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() = (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices() by GLIB_001:92;
set C = (P2 .cut (di,ei)) .append ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse());
set d = P1 . di;
A15: P2 . di = P1 . di by Th7;
then A16: (P2 .cut (di,ei)) .first() = P1 . di by A11, GLIB_001:37;
A17: P2 . ei = P1 . (P1 .find (P2 . ei)) by A11, GLIB_001:def_19;
len P2 <> 1
proof
assume len P2 = 1 ; ::_thesis: contradiction
then di < 1 by A11, XXREAL_0:2;
hence contradiction by ABIAN:12; ::_thesis: verum
end;
then A18: not P2 is trivial by GLIB_001:126;
A19: di < P1 .find (P2 . ei)
proof
assume di >= P1 .find (P2 . ei) ; ::_thesis: contradiction
then ( P1 . (P1 .find (P2 . ei)) = P2 . (P1 .find (P2 . ei)) & ei > P1 .find (P2 . ei) ) by A11, Th7, XXREAL_0:2;
then ( P2 .first() = P2 . ei & P2 .last() = P2 . ei ) by A11, A17, GLIB_001:def_28;
hence contradiction by A18, GLIB_001:def_24; ::_thesis: verum
end;
then A20: not P1 .cut (di,(P1 .find (P2 . ei))) is trivial by A13, GLIB_001:131;
then A21: not P1 is trivial ;
P1 .find (P2 . ei) <= len P1 by A11, GLIB_001:def_19;
then A22: ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() c= P1 .vertices() by A19, A14, GLIB_001:94;
A23: ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) c= {(P2 . ei),(P1 . di)}
proof
assume not ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) c= {(P2 . ei),(P1 . di)} ; ::_thesis: contradiction
then consider g being set such that
A24: g in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) and
A25: not g in {(P2 . ei),(P1 . di)} by TARSKI:def_3;
g in (P2 .cut (di,ei)) .vertices() by A24, XBOOLE_0:def_4;
then consider gii being odd Element of NAT such that
A26: gii <= len (P2 .cut (di,ei)) and
A27: (P2 .cut (di,ei)) . gii = g by GLIB_001:87;
consider gi being odd Nat such that
A28: P2 . gi = (P2 .cut (di,ei)) . gii and
A29: gi = (di + gii) - 1 and
A30: gi <= len P2 by A11, A26, Th12;
reconsider gi = gi as odd Element of NAT by ORDINAL1:def_12;
A31: gii >= 1 by ABIAN:12;
A32: gi < ei
proof
A33: (len (P2 .cut (di,ei))) + di = ei + 1 by A11, GLIB_001:36;
assume A34: gi >= ei ; ::_thesis: contradiction
percases ( gi = ei or gi > ei ) by A34, XXREAL_0:1;
suppose gi = ei ; ::_thesis: contradiction
then (P2 .cut (di,ei)) . gii = (P2 .cut (di,ei)) .last() by A29, A33
.= P2 . ei by A11, GLIB_001:37 ;
hence contradiction by A25, A27, TARSKI:def_2; ::_thesis: verum
end;
suppose gi > ei ; ::_thesis: contradiction
then gi + 1 > ei + 1 by XREAL_1:6;
hence contradiction by A26, A29, A33, XREAL_1:6; ::_thesis: verum
end;
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 ; ::_thesis: contradiction
then di + gii > gi + 1 by A35, XREAL_1:8;
hence contradiction by A29; ::_thesis: verum
end;
g in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() by A24, XBOOLE_0:def_4;
hence contradiction by A12, A22, A27, A28, A30, A36, A32; ::_thesis: verum
end;
A37: (P2 .cut (di,ei)) .last() = P2 . ei by A11, GLIB_001:37;
(P1 .cut (di,(P1 .find (P2 . ei)))) .first() = P1 . di by A13, A19, GLIB_001:37;
then A38: ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .last() = P1 . di by GLIB_001:22;
(P1 .cut (di,(P1 .find (P2 . ei)))) .last() = P2 . ei by A13, A17, A19, GLIB_001:37;
then A39: ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .first() = P2 . ei by GLIB_001:22;
{(P2 . ei),(P1 . di)} c= ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices())
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(P2 . ei),(P1 . di)} or x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) )
assume A40: x in {(P2 . ei),(P1 . di)} ; ::_thesis: x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices())
percases ( x = P2 . ei or x = P1 . di ) by A40, TARSKI:def_2;
suppose x = P2 . ei ; ::_thesis: x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices())
then ( x in (P2 .cut (di,ei)) .vertices() & x in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() ) by A37, A39, GLIB_001:88;
hence x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) by XBOOLE_0:def_4; ::_thesis: verum
end;
suppose x = P1 . di ; ::_thesis: x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices())
then ( x in (P2 .cut (di,ei)) .vertices() & x in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() ) by A16, A38, GLIB_001:88;
hence x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) by XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
then A41: ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) = {(P2 . ei),(P1 . di)} by A23, XBOOLE_0:def_10;
A42: not P2 .cut (di,ei) is trivial by A11, GLIB_001:131;
then A43: not P2 is trivial ;
A44: not P1 c= P2
proof
assume A45: P1 c= P2 ; ::_thesis: contradiction
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, GLIB_001:def_23 ;
P1 . (len P1) = P1 .last()
.= b by A1, GLIB_001:def_23 ;
hence contradiction by A46, A47, A48, Th26; ::_thesis: verum
end;
A49: (P2 .cut (di,ei)) .edges() misses ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges()
proof
A50: (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices() = ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() by GLIB_001:92;
A51: (P1 .cut (di,(P1 .find (P2 . ei)))) .edges() = ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges() by GLIB_001:107;
assume ((P2 .cut (di,ei)) .edges()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges()) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being set such that
A52: x in ((P2 .cut (di,ei)) .edges()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges()) by XBOOLE_0:def_1;
x in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .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 (P1 .cut (di,(P1 .find (P2 . ei)))) and
A54: u1 = (P1 .cut (di,(P1 .find (P2 . ei)))) . m and
x = (P1 .cut (di,(P1 .find (P2 . ei)))) . (m + 1) and
A55: u2 = (P1 .cut (di,(P1 .find (P2 . ei)))) . (m + 2) and
A56: x Joins u1,u2,T by A51, GLIB_001:103;
x in (P2 .cut (di,ei)) .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 (P2 .cut (di,ei)) and
A58: v1 = (P2 .cut (di,ei)) . n and
x = (P2 .cut (di,ei)) . (n + 1) and
A59: v2 = (P2 .cut (di,ei)) . (n + 2) and
A60: x Joins v1,v2,T by GLIB_001:103;
A61: n + 0 < n + 2 by XREAL_1:8;
percases ( v1 <> v2 or v1 = v2 ) ;
supposeA62: v1 <> v2 ; ::_thesis: contradiction
A63: n + 2 = (n + 1) + 1 ;
then A64: n + 1 < len (P2 .cut (di,ei)) by A57, NAT_1:13;
then A65: (P2 .cut (di,ei)) . (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 = ni as Element of NAT by ORDINAL1:def_12;
A67: u2 in (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices() by A53, A55, GLIB_001:87;
m + 0 < m + 2 by XREAL_1:8;
then A68: m <= len (P1 .cut (di,(P1 .find (P2 . ei)))) by A53, XXREAL_0:2;
then u1 in (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices() by A54, GLIB_001:87;
then A69: {u1,u2} c= ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() by A50, A67, ZFMISC_1:32;
A70: m + 2 = (m + 1) + 1 ;
then A71: m + 1 < len (P1 .cut (di,(P1 .find (P2 . ei)))) by A53, NAT_1:13;
then A72: (P1 .cut (di,(P1 .find (P2 . ei)))) . (m + 2) = P1 . (di + (m + 1)) by A13, A19, A70, GLIB_001:36;
n <= len (P2 .cut (di,ei)) by A57, A61, XXREAL_0:2;
then A73: v1 in (P2 .cut (di,ei)) .vertices() by A58, GLIB_001:87;
v2 in (P2 .cut (di,ei)) .vertices() by A57, A59, GLIB_001:87;
then A74: {v1,v2} c= (P2 .cut (di,ei)) .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 = P2 . ei or v1 = P1 . di ) by A41, A74, A69, XBOOLE_1:19, ZFMISC_1:22;
n + 0 < n + 2 by XREAL_1:8;
then n <= len (P2 .cut (di,ei)) by A57, XXREAL_0:2;
then A77: ni < len (P2 .cut (di,ei)) by A66, NAT_1:13;
then A78: (P2 .cut (di,ei)) . n = P2 . (di + ni) by A11, A66, GLIB_001:36;
A79: P2 . (di + 2) = P2 . ei
proof
percases ( ( v1 = P2 . ei & v2 = P1 . di ) or ( v1 = P1 . di & v2 = P2 . ei ) ) by A41, A62, A75, A74, A69, A76, XBOOLE_1:19, ZFMISC_1:22;
supposeA80: ( v1 = P2 . ei & v2 = P1 . di ) ; ::_thesis: P2 . (di + 2) = P2 . ei
di + (n + 2) <= (len (P2 .cut (di,ei))) + 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() = P1 . di & P2 .last() = P1 . di ) by A15, A59, A65, A80, A81, GLIB_001:def_28;
hence P2 . (di + 2) = P2 . ei by A43, GLIB_001:def_24; ::_thesis: verum
end;
supposeA82: ( v1 = P1 . di & v2 = P2 . ei ) ; ::_thesis: P2 . (di + 2) = P2 . ei
ni = 0
proof
di + ni < (len (P2 .cut (di,ei))) + 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 ; ::_thesis: contradiction
reconsider ni = ni as even Element of NAT by A66;
di + 0 < di + ni by A84, XREAL_1:6;
then ( P2 .first() = P1 . di & P2 .last() = P1 . di ) by A15, A58, A78, A82, A83, GLIB_001:def_28;
hence contradiction by A43, GLIB_001:def_24; ::_thesis: verum
end;
hence P2 . (di + 2) = P2 . ei by A11, A59, A66, A64, A82, GLIB_001:36; ::_thesis: verum
end;
end;
end;
consider im being Nat such that
A85: m = im + 1 by NAT_1:6;
A86: ( v2 = P2 . ei or v2 = P1 . di ) by A41, A75, A74, A69, XBOOLE_1:19, ZFMISC_1:22;
reconsider im = im as Element of NAT by ORDINAL1:def_12;
A87: im < len (P1 .cut (di,(P1 .find (P2 . ei)))) by A68, A85, NAT_1:13;
then A88: (P1 .cut (di,(P1 .find (P2 . ei)))) . m = P1 . (di + im) by A13, A19, A85, GLIB_001:36;
P1 . (di + 2) = P2 . ei
proof
percases ( ( u1 = P2 . ei & u2 = P1 . di ) or ( u1 = P1 . di & u2 = P2 . ei ) ) by A60, A56, A62, A76, A86, GLIB_000:15;
supposeA89: ( u1 = P2 . ei & u2 = P1 . di ) ; ::_thesis: P1 . (di + 2) = P2 . ei
di + (m + 2) <= (len (P1 .cut (di,(P1 .find (P2 . ei))))) + di by A53, XREAL_1:6;
then ((di + m) + 1) + 1 <= (P1 .find (P2 . ei)) + 1 by A13, A19, GLIB_001:36;
then (di + m) + 1 <= P1 .find (P2 . ei) 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() = P1 . di & P1 .last() = P1 . di ) by A55, A72, A89, A90, GLIB_001:def_28;
hence P1 . (di + 2) = P2 . ei by A21, GLIB_001:def_24; ::_thesis: verum
end;
supposeA91: ( u1 = P1 . di & u2 = P2 . ei ) ; ::_thesis: P1 . (di + 2) = P2 . ei
im = 0
proof
di + im < (len (P1 .cut (di,(P1 .find (P2 . ei))))) + di by A87, XREAL_1:6;
then di + im < (P1 .find (P2 . ei)) + 1 by A13, A19, GLIB_001:36;
then di + im <= P1 .find (P2 . ei) by NAT_1:13;
then A92: di + im <= len P1 by A13, XXREAL_0:2;
assume A93: im <> 0 ; ::_thesis: contradiction
reconsider im = im as even Element of NAT by A85;
di + 0 < di + im by A93, XREAL_1:6;
then ( P1 .first() = P1 . di & P1 .last() = P1 . di ) by A54, A88, A91, A92, GLIB_001:def_28;
hence contradiction by A21, GLIB_001:def_24; ::_thesis: verum
end;
hence P1 . (di + 2) = P2 . ei by A13, A19, A55, A85, A71, A91, GLIB_001:36; ::_thesis: verum
end;
end;
end;
hence contradiction by A3, A44, A5, A79, Th24; ::_thesis: verum
end;
suppose v1 = v2 ; ::_thesis: contradiction
then ( (P2 .cut (di,ei)) .first() = v1 & (P2 .cut (di,ei)) .last() = v1 ) by A57, A58, A59, A61, GLIB_001:def_28;
hence contradiction by A42, GLIB_001:def_24; ::_thesis: verum
end;
end;
end;
not (P1 .cut (di,(P1 .find (P2 . ei)))) .reverse() is trivial by A20, GLIB_001:129;
then (P2 .cut (di,ei)) .append ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) is Cycle-like by A42, A16, A37, A39, A38, A41, A49, Th20;
hence contradiction ; ::_thesis: verum
end;
definition
let T be _Tree;
let a, b be Vertex of T;
funcT .pathBetween (a,b) -> Path of T means :Def2: :: HELLY:def 2
it is_Walk_from a,b;
existence
ex b1 being Path of T st b1 is_Walk_from a,b
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 the Path-like Subwalk of W ; ::_thesis: the Path-like Subwalk of W is_Walk_from a,b
the Path-like Subwalk of W is_Walk_from W .first() ,W .last() by GLIB_001:def_32;
then the Path-like Subwalk of W is_Walk_from a,W .last() by A1, GLIB_001:def_23;
hence the Path-like Subwalk of W is_Walk_from a,b by A1, GLIB_001:def_23; ::_thesis: verum
end;
uniqueness
for b1, b2 being Path of T st b1 is_Walk_from a,b & b2 is_Walk_from a,b holds
b1 = b2 by Th27;
end;
:: deftheorem Def2 defines .pathBetween HELLY:def_2_:_
for T being _Tree
for a, b being Vertex of T
for b4 being Path of T holds
( b4 = T .pathBetween (a,b) iff b4 is_Walk_from a,b );
theorem Th28: :: HELLY:28
for T being _Tree
for a, b being Vertex of T holds
( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b )
proof
let T be _Tree; ::_thesis: for a, b being Vertex of T holds
( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b )
let a, b be Vertex of T; ::_thesis: ( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b )
A1: T .pathBetween (a,b) is_Walk_from a,b by Def2;
hence (T .pathBetween (a,b)) .first() = a by GLIB_001:def_23; ::_thesis: (T .pathBetween (a,b)) .last() = b
thus (T .pathBetween (a,b)) .last() = b by A1, GLIB_001:def_23; ::_thesis: verum
end;
theorem Th29: :: HELLY:29
for T being _Tree
for 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; ::_thesis: for a, b being Vertex of T holds
( a in (T .pathBetween (a,b)) .vertices() & b in (T .pathBetween (a,b)) .vertices() )
let a, b be Vertex of T; ::_thesis: ( a in (T .pathBetween (a,b)) .vertices() & b in (T .pathBetween (a,b)) .vertices() )
(T .pathBetween (a,b)) .first() = a by Th28;
hence a in (T .pathBetween (a,b)) .vertices() by GLIB_001:88; ::_thesis: b in (T .pathBetween (a,b)) .vertices()
(T .pathBetween (a,b)) .last() = b by Th28;
hence b in (T .pathBetween (a,b)) .vertices() by GLIB_001:88; ::_thesis: verum
end;
registration
let T be _Tree;
let a be Vertex of T;
clusterT .pathBetween (a,a) -> closed ;
correctness
coherence
T .pathBetween (a,a) is closed ;
proof
T .pathBetween (a,a) is_Walk_from a,a by Def2;
hence T .pathBetween (a,a) is closed by GLIB_001:119; ::_thesis: verum
end;
end;
registration
let T be _Tree;
let a be Vertex of T;
clusterT .pathBetween (a,a) -> trivial ;
correctness
coherence
T .pathBetween (a,a) is trivial ;
;
end;
theorem Th30: :: HELLY:30
for T being _Tree
for a being Vertex of T holds (T .pathBetween (a,a)) .vertices() = {a}
proof
let T be _Tree; ::_thesis: for a being Vertex of T holds (T .pathBetween (a,a)) .vertices() = {a}
let a be Vertex of T; ::_thesis: (T .pathBetween (a,a)) .vertices() = {a}
set P = T .pathBetween (a,a);
consider v being Vertex of T such that
A1: T .pathBetween (a,a) = T .walkOf v by GLIB_001:128;
( a = (T .pathBetween (a,a)) .first() & (T .walkOf v) .first() = v ) by Th28, GLIB_001:13;
hence (T .pathBetween (a,a)) .vertices() = {a} by A1, GLIB_001:90; ::_thesis: verum
end;
theorem Th31: :: HELLY:31
for T being _Tree
for a, b being Vertex of T holds (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a)
proof
let T be _Tree; ::_thesis: for a, b being Vertex of T holds (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a)
let a, b be Vertex of T; ::_thesis: (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a)
set P = T .pathBetween (a,b);
T .pathBetween (a,b) is_Walk_from a,b by Def2;
then (T .pathBetween (a,b)) .reverse() is_Walk_from b,a by GLIB_001:23;
hence (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a) by Def2; ::_thesis: verum
end;
theorem Th32: :: HELLY:32
for T being _Tree
for a, b being Vertex of T holds (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices()
proof
let T be _Tree; ::_thesis: for a, b being Vertex of T holds (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices()
let a, b be Vertex of T; ::_thesis: (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices()
(T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a) by Th31;
hence (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() by GLIB_001:92; ::_thesis: verum
end;
theorem Th33: :: HELLY:33
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; ::_thesis: 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)
let a, b be Vertex of T; ::_thesis: 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)
let t be _Subtree of T; ::_thesis: for a9, b9 being Vertex of t st a = a9 & b = b9 holds
T .pathBetween (a,b) = t .pathBetween (a9,b9)
let a9, b9 be Vertex of t; ::_thesis: ( a = a9 & b = b9 implies T .pathBetween (a,b) = t .pathBetween (a9,b9) )
assume that
A1: a = a9 and
A2: b = b9 ; ::_thesis: T .pathBetween (a,b) = t .pathBetween (a9,b9)
set tp = t .pathBetween (a9,b9);
reconsider tp9 = t .pathBetween (a9,b9) as Walk of T by GLIB_001:167;
A3: t .pathBetween (a9,b9) is_Walk_from a9,b9 by Def2;
A4: tp9 .last() = (t .pathBetween (a9,b9)) .last()
.= b by A2, A3, GLIB_001:def_23 ;
tp9 .first() = (t .pathBetween (a9,b9)) .first()
.= a by A1, A3, GLIB_001:def_23 ;
then ( tp9 is Path-like & tp9 is_Walk_from a,b ) by A4, GLIB_001:176, GLIB_001:def_23;
hence T .pathBetween (a,b) = t .pathBetween (a9,b9) by Def2; ::_thesis: verum
end;
theorem Th34: :: HELLY:34
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; ::_thesis: 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
let a, b be Vertex of T; ::_thesis: 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
let t be _Subtree of T; ::_thesis: ( a in the_Vertices_of t & b in the_Vertices_of t implies (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t )
assume ( a in the_Vertices_of t & b in the_Vertices_of t ) ; ::_thesis: (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t
then reconsider a9 = a, b9 = b as Vertex of t ;
set Tp = T .pathBetween (a,b);
set tp = t .pathBetween (a9,b9);
(T .pathBetween (a,b)) .vertices() = (t .pathBetween (a9,b9)) .vertices() by Th33, GLIB_001:76;
hence (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t ; ::_thesis: verum
end;
theorem Th35: :: HELLY:35
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; ::_thesis: 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)
let P be Path of T; ::_thesis: 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)
let a, b be Vertex of T; ::_thesis: 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)
let i, j be odd Nat; ::_thesis: ( i <= j & j <= len P & P . i = a & P . j = b implies T .pathBetween (a,b) = P .cut (i,j) )
assume A1: ( i <= j & j <= len P & P . i = a & P . j = b ) ; ::_thesis: T .pathBetween (a,b) = P .cut (i,j)
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 T .pathBetween (a,b) = P .cut (i,j) by Def2; ::_thesis: verum
end;
theorem Th36: :: HELLY:36
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; ::_thesis: 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)) )
let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) )
set P = T .pathBetween (a,b);
set ci = (T .pathBetween (a,b)) .find c;
set pac = T .pathBetween (a,c);
set pcb = T .pathBetween (c,b);
hereby ::_thesis: ( T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) implies c in (T .pathBetween (a,b)) .vertices() )
A1: T .pathBetween (a,b) = (T .pathBetween (a,b)) .cut (1,(len (T .pathBetween (a,b)))) by GLIB_001:39;
A2: ( 1 <= (T .pathBetween (a,b)) .find c & 1 = (2 * 0) + 1 ) by ABIAN:12;
assume A3: c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b))
then A4: (T .pathBetween (a,b)) .find c <= len (T .pathBetween (a,b)) by GLIB_001:def_19;
A5: (T .pathBetween (a,b)) . ((T .pathBetween (a,b)) .find c) = c by A3, GLIB_001:def_19;
(T .pathBetween (a,b)) . (len (T .pathBetween (a,b))) = (T .pathBetween (a,b)) .last()
.= b by Th28 ;
then A6: T .pathBetween (c,b) = (T .pathBetween (a,b)) .cut (((T .pathBetween (a,b)) .find c),(len (T .pathBetween (a,b)))) by A4, A5, Th35;
(T .pathBetween (a,b)) . 1 = (T .pathBetween (a,b)) .first()
.= a by Th28 ;
then T .pathBetween (a,c) = (T .pathBetween (a,b)) .cut (1,((T .pathBetween (a,b)) .find c)) by A4, A2, A5, Th35;
hence T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A4, A2, A6, A1, GLIB_001:38; ::_thesis: verum
end;
assume T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) ; ::_thesis: c in (T .pathBetween (a,b)) .vertices()
then A7: (T .pathBetween (a,c)) .vertices() c= (T .pathBetween (a,b)) .vertices() by Th13, Th15;
c in (T .pathBetween (a,c)) .vertices() by Th29;
hence c in (T .pathBetween (a,b)) .vertices() by A7; ::_thesis: verum
end;
theorem Th37: :: HELLY:37
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; ::_thesis: 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) )
let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,c) is_a_prefix_of T .pathBetween (a,b) )
hereby ::_thesis: ( T .pathBetween (a,c) is_a_prefix_of T .pathBetween (a,b) implies c in (T .pathBetween (a,b)) .vertices() )
assume c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: T .pathBetween (a,c) c= T .pathBetween (a,b)
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; ::_thesis: verum
end;
assume T .pathBetween (a,c) c= T .pathBetween (a,b) ; ::_thesis: c in (T .pathBetween (a,b)) .vertices()
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 c in (T .pathBetween (a,b)) .vertices() by A1; ::_thesis: verum
end;
theorem Th38: :: HELLY:38
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; ::_thesis: 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
let P1, P2 be Path of T; ::_thesis: ( P1 .last() = P2 .first() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} implies P1 .append P2 is Path-like )
assume that
A1: P1 .last() = P2 .first() and
A2: (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} ; ::_thesis: P1 .append P2 is Path-like
percases ( P1 is trivial or P2 is trivial or ( not P1 is trivial & not P2 is trivial ) ) ;
suppose P1 is trivial ; ::_thesis: P1 .append P2 is Path-like
hence P1 .append P2 is Path-like by A1, Th16; ::_thesis: verum
end;
suppose P2 is trivial ; ::_thesis: P1 .append P2 is Path-like
hence P1 .append P2 is Path-like by GLIB_001:130; ::_thesis: verum
end;
suppose ( not P1 is trivial & not P2 is trivial ) ; ::_thesis: P1 .append P2 is Path-like
hence P1 .append P2 is Path-like by A1, A2, Th19; ::_thesis: verum
end;
end;
end;
theorem Th39: :: HELLY:39
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; ::_thesis: 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} )
let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() iff ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} )
set Pac = T .pathBetween (a,c);
set Pcb = T .pathBetween (c,b);
set Pab = T .pathBetween (a,b);
A1: (T .pathBetween (a,c)) .last() = c by Th28
.= (T .pathBetween (c,b)) .first() by Th28 ;
thus ( c in (T .pathBetween (a,b)) .vertices() implies ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} ) ::_thesis: ( ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} implies c in (T .pathBetween (a,b)) .vertices() )
proof
assume A2: c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c}
thus ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) c= {c} :: according to XBOOLE_0:def_10 ::_thesis: {c} c= ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) or x in {c} )
assume A3: x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) ; ::_thesis: x in {c}
then A4: x in (T .pathBetween (a,c)) .vertices() by XBOOLE_0:def_4;
A5: x in (T .pathBetween (c,b)) .vertices() by A3, XBOOLE_0:def_4;
A6: (T .pathBetween (c,b)) .first() = c by Th28;
A7: T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A2, Th36;
A8: ( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b ) by Th28;
A9: (T .pathBetween (a,c)) .last() = c by Th28;
percases ( T .pathBetween (a,b) is trivial or not T .pathBetween (a,b) is trivial ) ;
suppose T .pathBetween (a,b) is trivial ; ::_thesis: x in {c}
then (T .pathBetween (a,b)) .first() = (T .pathBetween (a,b)) .last() by GLIB_001:127;
then A10: (T .pathBetween (a,b)) .vertices() = {a} by A8, Th30;
x in ((T .pathBetween (a,c)) .vertices()) \/ ((T .pathBetween (c,b)) .vertices()) by A4, XBOOLE_0:def_3;
then x in (T .pathBetween (a,b)) .vertices() by A7, A9, A6, GLIB_001:93;
hence x in {c} by A2, A10, TARSKI:def_1; ::_thesis: verum
end;
supposeA11: not T .pathBetween (a,b) is trivial ; ::_thesis: x in {c}
consider n being odd Element of NAT such that
A12: n <= len (T .pathBetween (c,b)) and
A13: (T .pathBetween (c,b)) . 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 (T .pathBetween (a,c)) and
A15: (T .pathBetween (a,c)) . m = x by A4, GLIB_001:87;
A16: m <= (len (T .pathBetween (a,c))) + n1 by A14, NAT_1:12;
1 <= m by ABIAN:12;
then m in dom (T .pathBetween (a,c)) by A14, FINSEQ_3:25;
then A17: (T .pathBetween (a,b)) . m = x by A7, A15, GLIB_001:32;
(len (T .pathBetween (a,c))) + (n1 + 1) <= (len (T .pathBetween (a,c))) + (len (T .pathBetween (c,b))) by A12, XREAL_1:6;
then (((len (T .pathBetween (a,c))) + n1) + 1) - 1 <= ((len (T .pathBetween (a,c))) + (len (T .pathBetween (c,b)))) - 1 by XREAL_1:9;
then A18: (((len (T .pathBetween (a,c))) + n1) + 1) - 1 <= ((len (T .pathBetween (a,b))) + 1) - 1 by A7, A9, A6, GLIB_001:28;
A19: n1 + 1 = n ;
then n1 < len (T .pathBetween (c,b)) by A12, NAT_1:13;
then A20: (T .pathBetween (a,b)) . ((len (T .pathBetween (a,c))) + n1) = x by A7, A9, A6, A13, A19, GLIB_001:33;
percases ( m < (len (T .pathBetween (a,c))) + n1 or m = (len (T .pathBetween (a,c))) + n1 ) by A16, XXREAL_0:1;
supposeA21: m < (len (T .pathBetween (a,c))) + n1 ; ::_thesis: x in {c}
then (T .pathBetween (a,b)) .first() = x by A17, A20, A18, GLIB_001:def_28
.= (T .pathBetween (a,b)) .last() by A17, A20, A18, A21, GLIB_001:def_28 ;
hence x in {c} by A11, GLIB_001:def_24; ::_thesis: verum
end;
supposeA22: m = (len (T .pathBetween (a,c))) + n1 ; ::_thesis: x in {c}
then n1 = 0 by A14, NAT_1:16;
hence x in {c} by A9, A15, A22, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {c} or x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) )
assume x in {c} ; ::_thesis: x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())
then A23: x = c by TARSKI:def_1;
then x = (T .pathBetween (c,b)) .first() by Th28;
then A24: x in (T .pathBetween (c,b)) .vertices() by GLIB_001:88;
x = (T .pathBetween (a,c)) .last() by A23, Th28;
then x in (T .pathBetween (a,c)) .vertices() by GLIB_001:88;
hence x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) by A24, XBOOLE_0:def_4; ::_thesis: verum
end;
( (T .pathBetween (a,c)) .first() = a & (T .pathBetween (c,b)) .last() = b ) by Th28;
then A25: (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) is_Walk_from a,b by A1, GLIB_001:30;
assume ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} ; ::_thesis: c in (T .pathBetween (a,b)) .vertices()
then ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {((T .pathBetween (a,c)) .last())} by Th28;
then (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) is Path-like by A1, Th38;
then T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A25, Def2;
hence c in (T .pathBetween (a,b)) .vertices() by Th36; ::_thesis: verum
end;
theorem Th40: :: HELLY:40
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 be _Tree; ::_thesis: 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}
let a, b, c, d be Vertex of T; ::_thesis: 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}
let P1, P2 be Path of T; ::_thesis: ( 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))) implies ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d} )
assume 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))) ; ::_thesis: ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d}
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 = len (maxPrefix (P1,P2)) as odd Element of NAT by A6, Th22;
A8: di <= di + 2 by NAT_1:11;
set Pdb = T .pathBetween (d,b);
A9: (T .pathBetween (d,b)) .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 = (T .pathBetween (a,d)) .append (T .pathBetween (d,c)) by A2, Th36;
A13: (T .pathBetween (a,d)) .last() = d by Th28;
A14: (T .pathBetween (d,c)) . 1 = (T .pathBetween (d,c)) .first()
.= d by Th28 ;
A15: (T .pathBetween (d,c)) .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 = (T .pathBetween (a,d)) .append (T .pathBetween (d,b)) by A1, Th36;
A18: 1 <= di by ABIAN:12;
then T .pathBetween (a,d) = P1 .cut (((2 * 0) + 1),di) by A5, A6, A16, Th35;
then A19: (len (T .pathBetween (a,d))) + ((2 * 0) + 1) = di + 1 by A16, A18, GLIB_001:36;
A20: (T .pathBetween (d,b)) . 1 = (T .pathBetween (d,b)) .first()
.= d by Th28 ;
thus ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d} ::_thesis: verum
proof
hereby :: according to XBOOLE_0:def_10 ::_thesis: {d} c= ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices())
assume not ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) c= {d} ; ::_thesis: contradiction
then consider e being set such that
A21: e in ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) and
A22: not e in {d} by TARSKI:def_3;
A23: e in (T .pathBetween (d,b)) .vertices() by A21, XBOOLE_0:def_4;
A24: e in (T .pathBetween (d,c)) .vertices() by A21, XBOOLE_0:def_4;
reconsider e = e as Vertex of T by A21;
consider ebi being odd Element of NAT such that
A25: ebi <= len (T .pathBetween (d,b)) and
A26: e = (T .pathBetween (d,b)) . ebi by A23, GLIB_001:87;
set Pdeb = (T .pathBetween (d,b)) .cut (1,ebi);
( 1 <= ebi & (2 * 0) + 1 is odd Element of NAT ) by ABIAN:12;
then A27: (T .pathBetween (d,b)) .cut (1,ebi) is_Walk_from d,e by A20, A25, A26, GLIB_001:37;
1 < len ((T .pathBetween (d,b)) .cut (1,ebi))
proof
assume A28: 1 >= len ((T .pathBetween (d,b)) .cut (1,ebi)) ; ::_thesis: contradiction
percases ( len ((T .pathBetween (d,b)) .cut (1,ebi)) = 2 * 0 or len ((T .pathBetween (d,b)) .cut (1,ebi)) = 1 ) by A28, NAT_1:25;
suppose len ((T .pathBetween (d,b)) .cut (1,ebi)) = 2 * 0 ; ::_thesis: contradiction
hence contradiction ; ::_thesis: verum
end;
supposeA29: len ((T .pathBetween (d,b)) .cut (1,ebi)) = 1 ; ::_thesis: contradiction
A30: ((T .pathBetween (d,b)) .cut (1,ebi)) . 1 = d by A27, GLIB_001:17;
((T .pathBetween (d,b)) .cut (1,ebi)) . 1 = e by A27, A29, GLIB_001:17;
hence contradiction by A22, A30, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
then A31: ((2 * 0) + 1) + 2 <= len ((T .pathBetween (d,b)) .cut (1,ebi)) by CHORD:4;
then A32: 2 < len ((T .pathBetween (d,b)) .cut (1,ebi)) by XXREAL_0:2;
consider eci being odd Element of NAT such that
A33: eci <= len (T .pathBetween (d,c)) and
A34: e = (T .pathBetween (d,c)) . eci by A24, GLIB_001:87;
set Pdec = (T .pathBetween (d,c)) .cut (1,eci);
( 1 <= eci & (2 * 0) + 1 is odd Element of NAT ) by ABIAN:12;
then A35: (T .pathBetween (d,c)) .cut (1,eci) is_Walk_from d,e by A14, A33, A34, GLIB_001:37;
1 < len ((T .pathBetween (d,c)) .cut (1,eci))
proof
assume A36: 1 >= len ((T .pathBetween (d,c)) .cut (1,eci)) ; ::_thesis: contradiction
percases ( len ((T .pathBetween (d,c)) .cut (1,eci)) = 2 * 0 or len ((T .pathBetween (d,c)) .cut (1,eci)) = 1 ) by A36, NAT_1:25;
suppose len ((T .pathBetween (d,c)) .cut (1,eci)) = 2 * 0 ; ::_thesis: contradiction
hence contradiction ; ::_thesis: verum
end;
supposeA37: len ((T .pathBetween (d,c)) .cut (1,eci)) = 1 ; ::_thesis: contradiction
A38: ((T .pathBetween (d,c)) .cut (1,eci)) . 1 = d by A35, GLIB_001:17;
((T .pathBetween (d,c)) .cut (1,eci)) . 1 = e by A35, A37, GLIB_001:17;
hence contradiction by A22, A38, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
then A39: ((2 * 0) + 1) + 2 <= len ((T .pathBetween (d,c)) .cut (1,eci)) by CHORD:4;
then A40: 2 < len ((T .pathBetween (d,c)) .cut (1,eci)) by XXREAL_0:2;
1 + 2 in dom ((T .pathBetween (d,b)) .cut (1,ebi)) by A31, FINSEQ_3:25;
then A41: ((T .pathBetween (d,b)) .cut (1,ebi)) . (1 + 2) = (T .pathBetween (d,b)) . (1 + 2) by A25, GLIB_001:46;
len ((T .pathBetween (d,b)) .cut (1,ebi)) <= len (T .pathBetween (d,b)) by Th10;
then 2 < len (T .pathBetween (d,b)) by A32, XXREAL_0:2;
then A42: P1 . (di + 2) = (T .pathBetween (d,b)) . (1 + 2) by A9, A13, A17, A19, GLIB_001:33;
len ((T .pathBetween (d,c)) .cut (1,eci)) <= len (T .pathBetween (d,c)) by Th10;
then 2 < len (T .pathBetween (d,c)) by A40, XXREAL_0:2;
then A43: P2 . (di + 2) = (T .pathBetween (d,c)) . (1 + 2) by A15, A13, A12, A19, GLIB_001:33;
A44: 1 + 2 in dom ((T .pathBetween (d,c)) .cut (1,eci)) by A39, FINSEQ_3:25;
((T .pathBetween (d,b)) .cut (1,ebi)) . (1 + 2) = ((T .pathBetween (d,c)) .cut (1,eci)) . (1 + 2) by A27, A35, Th27;
hence contradiction by A3, A4, A6, A7, A33, A42, A41, A43, A44, Th24, GLIB_001:46; ::_thesis: verum
end;
( d in (T .pathBetween (d,b)) .vertices() & d in (T .pathBetween (d,c)) .vertices() ) by A9, A15, GLIB_001:88;
then d in ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) by XBOOLE_0:def_4;
hence {d} c= ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) by ZFMISC_1:31; ::_thesis: verum
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; ::_thesis: 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}
let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() implies (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} )
assume A1: c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c}
set P1 = T .pathBetween (a,b);
set P2 = T .pathBetween (b,c);
set P3 = T .pathBetween (c,a);
(T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() by Th32;
then ((T .pathBetween (b,c)) .vertices()) /\ ((T .pathBetween (c,a)) .vertices()) = {c} by A1, Th39;
then ((T .pathBetween (a,b)) .vertices()) /\ (((T .pathBetween (b,c)) .vertices()) /\ ((T .pathBetween (c,a)) .vertices())) = {c} by A1, ZFMISC_1:46;
hence (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} by XBOOLE_1:16; ::_thesis: verum
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; ::_thesis: 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))))}
let a, b, c be Vertex of T; ::_thesis: 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))))}
let P1, P4 be Path of T; ::_thesis: ( P1 = T .pathBetween (a,b) & P4 = T .pathBetween (a,c) & not P1 c= P4 & not P4 c= P1 implies ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))} )
assume 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 ; ::_thesis: ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))}
set P3 = T .pathBetween (c,a);
A5: (T .pathBetween (c,a)) .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 = len (maxPrefix (P1,P4)) as odd Element of NAT by Th22;
set x = P1 . i9;
A7: len (maxPrefix (P1,P4)) <= (len (maxPrefix (P1,P4))) + 2 by NAT_1:11;
A8: now__::_thesis:_not_b_in_(T_.pathBetween_(c,a))_.vertices()
assume b in (T .pathBetween (c,a)) .vertices() ; ::_thesis: contradiction
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; ::_thesis: verum
end;
(len (maxPrefix (P1,P4))) + 2 <= len P4 by A4, A6, Th23;
then A9: len (maxPrefix (P1,P4)) <= len P4 by A7, XXREAL_0:2;
A10: (len (maxPrefix (P1,P4))) + 2 <= len P1 by A3, A6, Th23;
then reconsider x = P1 . i9 as Vertex of T by A7, GLIB_001:7, XXREAL_0:2;
set P1b = P1 .cut (i9,(len P1));
set P1br = (P1 .cut (i9,(len P1))) .reverse() ;
set j = len ((P1 .cut (i9,(len P1))) .reverse());
set P4c = P4 .cut (i9,(len P4));
set Pbc = ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4)));
A11: len (maxPrefix (P1,P4)) <= len P1 by A7, A10, XXREAL_0:2;
then (P1 .cut (i9,(len P1))) .first() = P1 . i9 by GLIB_001:37;
then A12: ((P1 .cut (i9,(len P1))) .reverse()) .last() = x by GLIB_001:22;
1 <= len ((P1 .cut (i9,(len P1))) .reverse()) by CHORD:2;
then len ((P1 .cut (i9,(len P1))) .reverse()) in dom ((P1 .cut (i9,(len P1))) .reverse()) by FINSEQ_3:25;
then A13: (((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4)))) . (len ((P1 .cut (i9,(len P1))) .reverse())) = 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 (P1 .cut (i9,(len P1))) .last() = b by A11, GLIB_001:37;
then A16: ((P1 .cut (i9,(len P1))) .reverse()) .first() = b by GLIB_001:22;
A17: x = P4 . i9 by Th7;
then x <> b by A8, A5, A9, GLIB_001:87;
then A18: (P1 .cut (i9,(len P1))) .reverse() is open by A12, A16, GLIB_001:def_24;
P4 . (len P4) = P4 .last()
.= c by A2, Th28 ;
then P4 .cut (i9,(len P4)) is_Walk_from x,c by A9, A17, GLIB_001:37;
then A19: P4 .cut (i9,(len P4)) = T .pathBetween (x,c) by Def2;
then A20: (P4 .cut (i9,(len P4))) .first() = x by Th28;
then A21: len ((P1 .cut (i9,(len P1))) .reverse()) <= len (((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4)))) by A12, GLIB_001:29;
P1 .cut (i9,(len P1)) is_Walk_from x,b by A11, A15, GLIB_001:37;
then P1 .cut (i9,(len P1)) = T .pathBetween (x,b) by Def2;
then ( ((P1 .cut (i9,(len P1))) .reverse()) .vertices() = (P1 .cut (i9,(len P1))) .vertices() & ((P1 .cut (i9,(len P1))) .vertices()) /\ ((P4 .cut (i9,(len P4))) .vertices()) = {x} ) by A1, A2, A3, A4, A19, Th40, GLIB_001:92;
then A22: (((P1 .cut (i9,(len P1))) .reverse()) .vertices()) /\ ((P4 .cut (i9,(len P4))) .vertices()) c= {(((P1 .cut (i9,(len P1))) .reverse()) .first()),(((P1 .cut (i9,(len P1))) .reverse()) .last())} by A12, ZFMISC_1:7;
A23: (P4 .cut (i9,(len P4))) .vertices() c= P4 .vertices() by A9, GLIB_001:94;
A24: ((P1 .cut (i9,(len P1))) .reverse()) .edges() misses (P4 .cut (i9,(len P4))) .edges()
proof
assume not ((P1 .cut (i9,(len P1))) .reverse()) .edges() misses (P4 .cut (i9,(len P4))) .edges() ; ::_thesis: contradiction
then (((P1 .cut (i9,(len P1))) .reverse()) .edges()) /\ ((P4 .cut (i9,(len P4))) .edges()) <> {} by XBOOLE_0:def_7;
then consider e being set such that
A25: e in (((P1 .cut (i9,(len P1))) .reverse()) .edges()) /\ ((P4 .cut (i9,(len P4))) .edges()) by XBOOLE_0:def_1;
e in ((P1 .cut (i9,(len P1))) .reverse()) .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 ((P1 .cut (i9,(len P1))) .reverse()) and
A27: v1br = ((P1 .cut (i9,(len P1))) .reverse()) . n and
e = ((P1 .cut (i9,(len P1))) .reverse()) . (n + 1) and
A28: v2br = ((P1 .cut (i9,(len P1))) .reverse()) . (n + 2) and
A29: e Joins v1br,v2br,T by GLIB_001:103;
n <= n + 2 by NAT_1:11;
then n <= len ((P1 .cut (i9,(len P1))) .reverse()) by A26, XXREAL_0:2;
then A30: v1br in ((P1 .cut (i9,(len P1))) .reverse()) .vertices() by A27, GLIB_001:87;
v2br in ((P1 .cut (i9,(len P1))) .reverse()) .vertices() by A26, A28, GLIB_001:87;
then A31: {v1br,v2br} c= ((P1 .cut (i9,(len P1))) .reverse()) .vertices() by A30, ZFMISC_1:32;
e in (P4 .cut (i9,(len P4))) .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 (P4 .cut (i9,(len P4))) and
A33: v1c = (P4 .cut (i9,(len P4))) . m and
e = (P4 .cut (i9,(len P4))) . (m + 1) and
A34: v2c = (P4 .cut (i9,(len P4))) . (m + 2) and
A35: e Joins v1c,v2c,T by GLIB_001:103;
m <= m + 2 by NAT_1:11;
then m <= len (P4 .cut (i9,(len P4))) by A32, XXREAL_0:2;
then A36: v1c in (P4 .cut (i9,(len P4))) .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 (P4 .cut (i9,(len P4))) .vertices() by A32, A34, GLIB_001:87;
then {v1c,v2c} c= (P4 .cut (i9,(len P4))) .vertices() by A36, ZFMISC_1:32;
then A39: {v1c,v2c} c= (((P1 .cut (i9,(len P1))) .reverse()) .vertices()) /\ ((P4 .cut (i9,(len P4))) .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; ::_thesis: verum
end;
A41: (P4 .cut (i9,(len P4))) .last() = c by A19, Th28;
then A42: ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))) is_Walk_from b,c by A12, A20, A16, GLIB_001:30;
now__::_thesis:_not_c_in_P1_.vertices()
assume c in P1 .vertices() ; ::_thesis: contradiction
then P1 = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A1, Th36;
hence contradiction by A2, A4, Th15; ::_thesis: verum
end;
then x <> c by A11, GLIB_001:87;
then A43: P4 .cut (i9,(len P4)) is open by A20, A41, GLIB_001:def_24;
not ((P1 .cut (i9,(len P1))) .reverse()) .first() in (P4 .cut (i9,(len P4))) .vertices() by A8, A5, A23, A16;
then ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))) is Path of T by A12, A20, A18, A43, A22, A24, Th18;
then ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))) = T .pathBetween (b,c) by A42, Def2;
then A44: x in (T .pathBetween (b,c)) .vertices() by A21, A13, GLIB_001:87;
A45: x in P4 .vertices() by A9, A17, GLIB_001:87;
A46: ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) c= {x}
proof
set Pcx = T .pathBetween (c,x);
set Pxa = T .pathBetween (x,a);
set Pbx = T .pathBetween (b,x);
set Pxc = T .pathBetween (x,c);
set Pax = T .pathBetween (a,x);
set Pxb = T .pathBetween (x,b);
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) or z in {x} )
A47: (T .pathBetween (b,x)) .vertices() = (T .pathBetween (x,b)) .vertices() by Th32;
A48: (T .pathBetween (c,x)) .vertices() = (T .pathBetween (x,c)) .vertices() by Th32;
A49: (T .pathBetween (c,x)) .last() = x by Th28
.= (T .pathBetween (x,a)) .first() by Th28 ;
T .pathBetween (c,a) = (T .pathBetween (c,x)) .append (T .pathBetween (x,a)) by A5, A45, Th36;
then A50: (T .pathBetween (c,a)) .vertices() = ((T .pathBetween (c,x)) .vertices()) \/ ((T .pathBetween (x,a)) .vertices()) by A49, GLIB_001:93;
A51: (T .pathBetween (b,x)) .last() = x by Th28
.= (T .pathBetween (x,c)) .first() by Th28 ;
T .pathBetween (b,c) = (T .pathBetween (b,x)) .append (T .pathBetween (x,c)) by A44, Th36;
then A52: (T .pathBetween (b,c)) .vertices() = ((T .pathBetween (b,x)) .vertices()) \/ ((T .pathBetween (x,c)) .vertices()) by A51, GLIB_001:93;
A53: (T .pathBetween (a,x)) .last() = x by Th28
.= (T .pathBetween (x,b)) .first() by Th28 ;
P1 = (T .pathBetween (a,x)) .append (T .pathBetween (x,b)) by A1, A14, Th36;
then A54: P1 .vertices() = ((T .pathBetween (a,x)) .vertices()) \/ ((T .pathBetween (x,b)) .vertices()) by A53, GLIB_001:93;
assume A55: z in ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) ; ::_thesis: z in {x}
then A56: z in (P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices()) by XBOOLE_0:def_4;
then z in P1 .vertices() by XBOOLE_0:def_4;
then A57: ( z in (T .pathBetween (a,x)) .vertices() or z in (T .pathBetween (x,b)) .vertices() ) by A54, XBOOLE_0:def_3;
z in (T .pathBetween (c,a)) .vertices() by A55, XBOOLE_0:def_4;
then A58: ( z in (T .pathBetween (c,x)) .vertices() or z in (T .pathBetween (x,a)) .vertices() ) by A50, XBOOLE_0:def_3;
z in (T .pathBetween (b,c)) .vertices() by A56, XBOOLE_0:def_4;
then A59: ( z in (T .pathBetween (b,x)) .vertices() or z in (T .pathBetween (x,c)) .vertices() ) by A52, XBOOLE_0:def_3;
percases ( ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (b,x)) .vertices() ) or ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) or ( z in (T .pathBetween (b,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) ) by A57, A59, A58, Th32;
suppose ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (b,x)) .vertices() ) ; ::_thesis: z in {x}
then z in ((T .pathBetween (a,x)) .vertices()) /\ ((T .pathBetween (x,b)) .vertices()) by A47, XBOOLE_0:def_4;
hence z in {x} by A1, A14, Th39; ::_thesis: verum
end;
suppose ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) ; ::_thesis: z in {x}
then z in ((T .pathBetween (a,x)) .vertices()) /\ ((T .pathBetween (x,c)) .vertices()) by A48, XBOOLE_0:def_4;
hence z in {x} by A2, A45, Th39; ::_thesis: verum
end;
suppose ( z in (T .pathBetween (b,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) ; ::_thesis: z in {x}
then z in ((T .pathBetween (b,x)) .vertices()) /\ ((T .pathBetween (x,c)) .vertices()) by A48, XBOOLE_0:def_4;
hence z in {x} by A44, Th39; ::_thesis: verum
end;
end;
end;
x in (P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices()) by A14, A44, XBOOLE_0:def_4;
then x in ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) by A5, A45, XBOOLE_0:def_4;
then {x} c= ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) by ZFMISC_1:31;
hence ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))} by A46, XBOOLE_0:def_10; ::_thesis: verum
end;
definition
let T be _Tree;
let a, b, c be Vertex of T;
func MiddleVertex (a,b,c) -> Vertex of T means :Def3: :: HELLY:def 3
(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {it};
existence
ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1}
proof
defpred S1[ 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);
percases ( c in (T .pathBetween (a,b)) .vertices() or a in (T .pathBetween (b,c)) .vertices() or b in (T .pathBetween (c,a)) .vertices() or ( not c in (T .pathBetween (a,b)) .vertices() & not a in (T .pathBetween (b,c)) .vertices() & not b in (T .pathBetween (c,a)) .vertices() ) ) ;
supposeA1: ( c in (T .pathBetween (a,b)) .vertices() or a in (T .pathBetween (b,c)) .vertices() or b in (T .pathBetween (c,a)) .vertices() ) ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1}
percases ( c in (T .pathBetween (a,b)) .vertices() or a in (T .pathBetween (b,c)) .vertices() or b in (T .pathBetween (c,a)) .vertices() ) by A1;
suppose c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1}
then S1[a,b,c,c] by Lm1;
hence ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} ; ::_thesis: verum
end;
suppose a in (T .pathBetween (b,c)) .vertices() ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1}
then S1[b,c,a,a] by Lm1;
hence ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} by XBOOLE_1:16; ::_thesis: verum
end;
suppose b in (T .pathBetween (c,a)) .vertices() ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1}
then S1[c,a,b,b] by Lm1;
hence ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} by XBOOLE_1:16; ::_thesis: verum
end;
end;
end;
supposeA2: ( not c in (T .pathBetween (a,b)) .vertices() & not a in (T .pathBetween (b,c)) .vertices() & not b in (T .pathBetween (c,a)) .vertices() ) ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1}
set P4 = T .pathBetween (a,c);
set i = len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c))));
(T .pathBetween (a,b)) .last() = b by Th28;
then A3: b in (T .pathBetween (a,b)) .vertices() by GLIB_001:88;
(T .pathBetween (a,c)) .last() = c by Th28;
then c in (T .pathBetween (a,c)) .vertices() by GLIB_001:88;
then not (T .pathBetween (a,c)) .vertices() c= (T .pathBetween (a,b)) .vertices() by A2;
then A4: not T .pathBetween (a,c) c= T .pathBetween (a,b) by Th13;
(T .pathBetween (a,b)) .first() = a by Th28;
then A5: (T .pathBetween (a,b)) .first() = (T .pathBetween (a,c)) .first() by Th28;
then reconsider i9 = len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c)))) as odd Element of NAT by Th22;
set x = (T .pathBetween (a,b)) . i9;
(T .pathBetween (c,a)) .vertices() = (T .pathBetween (a,c)) .vertices() by Th32;
then A6: not (T .pathBetween (a,b)) .vertices() c= (T .pathBetween (a,c)) .vertices() by A2, A3;
then ( len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c)))) <= (len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c))))) + 2 & (len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c))))) + 2 <= len (T .pathBetween (a,b)) ) by A5, Th13, Th23, NAT_1:11;
then reconsider x = (T .pathBetween (a,b)) . i9 as Vertex of T by GLIB_001:7, XXREAL_0:2;
take x ; ::_thesis: (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {x}
not T .pathBetween (a,b) c= T .pathBetween (a,c) by A6, Th13;
hence (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {x} by A4, Lm2; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} & (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b2} holds
b1 = b2 by ZFMISC_1:3;
end;
:: deftheorem Def3 defines MiddleVertex HELLY:def_3_:_
for T being _Tree
for a, b, c, b5 being Vertex of T holds
( b5 = MiddleVertex (a,b,c) iff (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b5} );
theorem Th41: :: HELLY:41
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; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (a,c,b)
let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (a,c,b)
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()) = {(MiddleVertex (a,b,c))} & (((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())) /\ ((T .pathBetween (b,a)) .vertices()) = {(MiddleVertex (a,c,b))} ) by Def3;
then {(MiddleVertex (a,b,c))} = {(MiddleVertex (a,c,b))} by A1, A2, XBOOLE_1:16;
hence MiddleVertex (a,b,c) = MiddleVertex (a,c,b) by ZFMISC_1:3; ::_thesis: verum
end;
theorem Th42: :: HELLY:42
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; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (b,a,c)
let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (b,a,c)
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()) = {(MiddleVertex (a,b,c))} & (((T .pathBetween (b,a)) .vertices()) /\ ((T .pathBetween (a,c)) .vertices())) /\ ((T .pathBetween (c,b)) .vertices()) = {(MiddleVertex (b,a,c))} ) by Def3;
then {(MiddleVertex (a,b,c))} = {(MiddleVertex (b,a,c))} by A1, A2, XBOOLE_1:16;
hence MiddleVertex (a,b,c) = MiddleVertex (b,a,c) by ZFMISC_1:3; ::_thesis: verum
end;
theorem :: HELLY:43
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; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (b,c,a)
let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (b,c,a)
thus MiddleVertex (a,b,c) = MiddleVertex (b,a,c) by Th42
.= MiddleVertex (b,c,a) by Th41 ; ::_thesis: verum
end;
theorem Th44: :: HELLY:44
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; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (c,a,b)
let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (c,a,b)
thus MiddleVertex (a,b,c) = MiddleVertex (a,c,b) by Th41
.= MiddleVertex (c,a,b) by Th42 ; ::_thesis: verum
end;
theorem :: HELLY:45
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; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (c,b,a)
let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (c,b,a)
thus MiddleVertex (a,b,c) = MiddleVertex (c,a,b) by Th44
.= MiddleVertex (c,b,a) by Th41 ; ::_thesis: verum
end;
theorem Th46: :: HELLY:46
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; ::_thesis: for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds
MiddleVertex (a,b,c) = c
let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() implies MiddleVertex (a,b,c) = c )
assume c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: MiddleVertex (a,b,c) = c
then (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} by Lm1;
hence MiddleVertex (a,b,c) = c by Def3; ::_thesis: verum
end;
theorem :: HELLY:47
for T being _Tree
for a being Vertex of T holds MiddleVertex (a,a,a) = a
proof
let T be _Tree; ::_thesis: for a being Vertex of T holds MiddleVertex (a,a,a) = a
let a be Vertex of T; ::_thesis: MiddleVertex (a,a,a) = a
a in {a} by TARSKI:def_1;
then a in (T .pathBetween (a,a)) .vertices() by Th30;
hence MiddleVertex (a,a,a) = a by Th46; ::_thesis: verum
end;
theorem Th48: :: HELLY:48
for T being _Tree
for a, b being Vertex of T holds MiddleVertex (a,a,b) = a
proof
let T be _Tree; ::_thesis: for a, b being Vertex of T holds MiddleVertex (a,a,b) = a
let a, b be Vertex of T; ::_thesis: MiddleVertex (a,a,b) = a
(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 MiddleVertex (a,a,b) = a by A1, Th46; ::_thesis: verum
end;
theorem Th49: :: HELLY:49
for T being _Tree
for a, b being Vertex of T holds MiddleVertex (a,b,a) = a
proof
let T be _Tree; ::_thesis: for a, b being Vertex of T holds MiddleVertex (a,b,a) = a
let a, b be Vertex of T; ::_thesis: MiddleVertex (a,b,a) = a
MiddleVertex (a,a,b) = MiddleVertex (a,b,a) by Th41;
hence MiddleVertex (a,b,a) = a by Th48; ::_thesis: verum
end;
theorem :: HELLY:50
for T being _Tree
for a, b being Vertex of T holds MiddleVertex (a,b,b) = b
proof
let T be _Tree; ::_thesis: for a, b being Vertex of T holds MiddleVertex (a,b,b) = b
let a, b be Vertex of T; ::_thesis: MiddleVertex (a,b,b) = b
MiddleVertex (a,b,b) = MiddleVertex (b,a,b) by Th42;
hence MiddleVertex (a,b,b) = b by Th49; ::_thesis: verum
end;
theorem Th51: :: HELLY:51
for T being _Tree
for P1, P2 being 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; ::_thesis: for P1, P2 being 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)))
let P1, P2 be Path of T; ::_thesis: 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)))
let a, b, c be Vertex of T; ::_thesis: ( P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() implies MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) )
assume that
A1: ( P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) ) and
A2: ( not b in P2 .vertices() & not c in P1 .vertices() ) ; ::_thesis: MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2)))
( 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 MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) by A3, ZFMISC_1:3; ::_thesis: verum
end;
theorem :: HELLY:52
for T being _Tree
for P1, P2, P3, P4 being 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; ::_thesis: for P1, P2, P3, P4 being 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)))
let P1, P2, P3, P4 be Path of T; ::_thesis: 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)))
let a, b, c be Vertex of T; ::_thesis: ( 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() implies P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4))) )
assume 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() ; ::_thesis: P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4)))
now__::_thesis:_not_P4_c=_P3
assume P4 c= P3 ; ::_thesis: contradiction
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; ::_thesis: verum
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 P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4))) by A9, Th42; ::_thesis: verum
end;
theorem Th53: :: HELLY:53
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; ::_thesis: 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 <> {}
let a, b, c be Vertex of T; ::_thesis: 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 <> {}
let S be non empty set ; ::_thesis: ( ( 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 ) ) ) ) implies meet S <> {} )
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 ) ) ) ; ::_thesis: meet 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 = (T .pathBetween (a,b)) .vertices() ;
set VPac = (T .pathBetween (a,c)) .vertices() ;
set VPbc = (T .pathBetween (b,c)) .vertices() ;
set VPca = (T .pathBetween (c,a)) .vertices() ;
(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(MiddleVertex (a,b,c))} by Def3;
then A2: MiddleVertex (a,b,c) in (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) by TARSKI:def_1;
then A3: MiddleVertex (a,b,c) in ((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices()) by XBOOLE_0:def_4;
then A4: MiddleVertex (a,b,c) in (T .pathBetween (b,c)) .vertices() by XBOOLE_0:def_4;
(T .pathBetween (c,a)) .vertices() = (T .pathBetween (a,c)) .vertices() by Th32;
then A5: MiddleVertex (a,b,c) in (T .pathBetween (a,c)) .vertices() by A2, XBOOLE_0:def_4;
A6: MiddleVertex (a,b,c) in (T .pathBetween (a,b)) .vertices() by A3, XBOOLE_0:def_4;
now__::_thesis:_for_s_being_set_st_s_in_S_holds_
MiddleVertex_(a,b,c)_in_s
let s be set ; ::_thesis: ( s in S implies MiddleVertex (a,b,c) in b1 )
assume A7: s in S ; ::_thesis: MiddleVertex (a,b,c) in b1
then A8: ex t being _Subtree of T st s = the_Vertices_of t by A1;
percases ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by A1, A7;
suppose ( a in s & b in s ) ; ::_thesis: MiddleVertex (a,b,c) in b1
then (T .pathBetween (a,b)) .vertices() c= s by A8, Th34;
hence MiddleVertex (a,b,c) in s by A6; ::_thesis: verum
end;
suppose ( a in s & c in s ) ; ::_thesis: MiddleVertex (a,b,c) in b1
then (T .pathBetween (a,c)) .vertices() c= s by A8, Th34;
hence MiddleVertex (a,b,c) in s by A5; ::_thesis: verum
end;
suppose ( b in s & c in s ) ; ::_thesis: MiddleVertex (a,b,c) in b1
then (T .pathBetween (b,c)) .vertices() c= s by A8, Th34;
hence MiddleVertex (a,b,c) in s by A4; ::_thesis: verum
end;
end;
end;
hence meet S <> {} by SETFAM_1:def_1; ::_thesis: verum
end;
begin
definition
let F be set ;
attrF is with_Helly_property means :: HELLY:def 4
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;
:: deftheorem defines with_Helly_property HELLY:def_4_:_
for F being set holds
( F is with_Helly_property iff 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 <> {} );
theorem :: HELLY:54
for T being _Tree
for X being finite set st ( for x being set st x in X holds
ex t being _Subtree of T st x = the_Vertices_of t ) holds
X is with_Helly_property
proof
let T be _Tree; ::_thesis: for X being finite set st ( for x being set st x in X holds
ex t being _Subtree of T st x = the_Vertices_of t ) holds
X is with_Helly_property
let X be finite set ; ::_thesis: ( ( for x being set st x in X holds
ex t being _Subtree of T st x = the_Vertices_of t ) implies X is with_Helly_property )
assume A1: for x being set st x in X holds
ex t being _Subtree of T st x = the_Vertices_of t ; ::_thesis: X is with_Helly_property
defpred S1[ 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
S1[n] ) holds
S1[k]
proof
let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A3: for n being Nat st n < k holds
S1[n] ; ::_thesis: S1[k]
let H be non empty finite set ; ::_thesis: ( card H = k & H c= X & ( for x, y being set st x in H & y in H holds
x meets y ) implies meet H <> {} )
assume 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 ; ::_thesis: meet H <> {}
percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;
suppose k = 0 ; ::_thesis: meet H <> {}
hence meet H <> {} by A4; ::_thesis: verum
end;
suppose k = 1 ; ::_thesis: meet H <> {}
then consider x being Element of H such that
A7: H = {x} by A4, GRAPH_5:5;
x in H ;
then ex t being _Subtree of T st x = the_Vertices_of t by A1, A5;
hence meet H <> {} by A7, SETFAM_1:10; ::_thesis: verum
end;
supposeA8: k > 1 ; ::_thesis: meet H <> {}
set cH = choose H;
set A = H \ {(choose H)};
A9: card (H \ {(choose H)}) = (card H) - (card {(choose H)}) by EULER_1:4
.= k - 1 by A4, CARD_1:30 ;
k - 1 > 1 - 1 by A8, XREAL_1:9;
then reconsider A = H \ {(choose H)} as non empty finite set by A9;
A10: A c= X by A5, XBOOLE_1:1;
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 = choose A;
set B = H \ {(choose A)};
A11: choose A in A ;
then A12: card (H \ {(choose A)}) = (card H) - (card {(choose A)}) by EULER_1:4
.= k - 1 by A4, CARD_1:30 ;
set C = {(choose H),(choose A)};
A13: meet {(choose H),(choose A)} = (choose H) /\ (choose A) by SETFAM_1:11;
choose H meets choose A by A6, A11;
then reconsider mC = meet {(choose H),(choose A)} as non empty set by A13, XBOOLE_0:def_7;
k - 1 > 1 - 1 by A8, XREAL_1:9;
then reconsider B = H \ {(choose A)} as non empty finite set by A12;
A14: B c= X by A5, XBOOLE_1:1;
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 = choose mA;
set b = choose mB;
set c = choose mC;
( choose mC in mC & mC c= union {(choose H),(choose A)} ) by SETFAM_1:2;
then consider cc being set such that
A15: choose mC in cc and
A16: cc in {(choose H),(choose A)} by TARSKI:def_4;
choose H in H ;
then {(choose H),(choose A)} 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;
( choose mA in mA & mA c= union A ) by SETFAM_1:2;
then consider aa being set such that
A18: choose mA in aa and
A19: aa in A by TARSKI:def_4;
( choose mB in mB & mB c= union B ) by SETFAM_1:2;
then consider bb being set such that
A20: choose mB 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 = choose mA, b = choose mB, c = choose mC as Vertex of T by A18, A20, A22, A15, A17;
A23: choose A <> choose H by ZFMISC_1:56;
now__::_thesis:_for_s_being_set_st_s_in_H_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_)_)_)
let s be set ; ::_thesis: ( s in H implies ( 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 ) ) ) )
assume A24: s in H ; ::_thesis: ( 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 ) ) )
hence ex t being _Subtree of T st s = the_Vertices_of t by A1, A5; ::_thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )
thus ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ::_thesis: verum
proof
percases ( s = choose H or s = choose A or ( s <> choose H & s <> choose A ) ) ;
suppose s = choose H ; ::_thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )
then ( s in {(choose H),(choose A)} & s in B ) by A23, TARSKI:def_2, ZFMISC_1:56;
hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by SETFAM_1:def_1; ::_thesis: verum
end;
supposeA25: s = choose A ; ::_thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )
then s in {(choose H),(choose A)} by TARSKI:def_2;
hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by A25, SETFAM_1:def_1; ::_thesis: verum
end;
suppose ( s <> choose H & s <> choose A ) ; ::_thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )
then ( s in A & s in B ) by A24, ZFMISC_1:56;
hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
end;
hence meet H <> {} by Th53; ::_thesis: verum
end;
end;
end;
A26: for n being Nat holds S1[n] from NAT_1:sch_4(A2);
let H be non empty set ; :: according to HELLY:def_4 ::_thesis: ( H c= X & ( for x, y being set st x in H & y in H holds
x meets y ) implies meet H <> {} )
assume that
A27: H c= X and
A28: for x, y being set st x in H & y in H holds
x meets y ; ::_thesis: meet H <> {}
reconsider H9 = H as finite set by A27;
card H9 = card H9 ;
hence meet H <> {} by A26, A27, A28; ::_thesis: verum
end;