:: Helly property for subtrees
:: by Jessica Enright and Piotr Rudnicki
::
:: Received January 10, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users

begin

theorem :: HELLY:1

for p being non empty FinSequence holds <*(p . 1)*> ^' p = p

proof 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 b₁ being FinSequence st
( b₁ is_a_prefix_of p & b₁ 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 b₁ ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st b₁ is_a_prefix_of p & b₁ 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 b₁ ) & b₂ is_a_prefix_of p & b₂ 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 b₂ ) holds
b₁ = b₂

proof end;

commutativity
for b₁, p, q being FinSequence st b₁ is_a_prefix_of p & b₁ 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 b₁ ) holds
( b₁ is_a_prefix_of q & b₁ 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 b₁ ) ) ;

end;

:: deftheorem Def1 defines maxPrefix HELLY:def 1 :
for p, q, b₃ being FinSequence holds
( b₃ = maxPrefix (p,q) iff ( b₃ is_a_prefix_of p & b₃ 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 b₃ ) ) );

theorem :: HELLY:2

for p, q being FinSequence holds
( p is_a_prefix_of q iff maxPrefix (p,q) = p )

proof end;

theorem Th3: :: HELLY:3

for p, q being FinSequence holds len (maxPrefix (p,q)) <= len p

proof end;

theorem Th4: :: HELLY:4

for p being non empty FinSequence holds <*(p . 1)*> is_a_prefix_of p

proof end;

theorem Th5: :: HELLY:5

for p, q being non empty FinSequence st p . 1 = q . 1 holds
1 <= len (maxPrefix (p,q))

proof 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 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 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 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 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 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 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 end;

registration

let G be _Graph;
cluster -> non empty Walk of G;
correctness
coherence
for b₁ being Walk of G holds not b₁ is empty ;
by CARD_1:47;

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 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 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 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 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 end;

theorem Th18: :: HELLY:18

for G being _Graph
for P1, P2 being Path of G st P1 .last() = P2 .first() & not P1 is closed & not P2 is closed & 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 end;

theorem Th19: :: HELLY:19

for G being _Graph
for P1, P2 being Path of G st P1 .last() = P2 .first() & not P1 is closed & not P2 is closed & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds
( not P1 .append P2 is closed & P1 .append P2 is Path-like )

proof 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() & not P1 is closed & not P2 is closed & P1 .edges() misses P2 .edges() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last()),(P1 .first())} holds
P1 .append P2 is Cycle-like

proof 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 end;

theorem Th22: :: HELLY:22

for G being _Graph
for W1, W2 being Walk of G st W1 .first() = W2 .first() holds
not len (maxPrefix (W1,W2)) is even

proof 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 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 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 Walk of T;
correctness
coherence
for b₁ being Walk of T st b₁ is Trail-like holds
b₁ is Path-like ;

proof end;

end;

theorem Th25: :: HELLY:25

for T being _Tree
for P being Path of T st not P is trivial holds
not P is closed

proof end;

registration

let T be _Tree;
cluster non trivial Path-like -> open Walk of T;
correctness
coherence
for b₁ being Path of T st not b₁ is trivial holds
not b₁ is closed ;
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 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 end;

definition

let T be _Tree;
let a, b be Vertex of T;
func T .pathBetween (a,b) -> Path of T means :Def2: :: HELLY:def 2
it is_Walk_from a,b;
existence
ex b₁ being Path of T st b₁ is_Walk_from a,b

proof end;

uniqueness
for b₁, b₂ being Path of T st b₁ is_Walk_from a,b & b₂ is_Walk_from a,b holds
b₁ = b₂ by Th27;

end;

:: deftheorem Def2 defines .pathBetween HELLY:def 2 :
for T being _Tree
for a, b being Vertex of T
for b₄ being Path of T holds
( b₄ = T .pathBetween (a,b) iff b₄ 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 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 end;

registration

let T be _Tree;
let a be Vertex of T;
cluster T .pathBetween (a,a) -> closed ;
correctness
coherence
T .pathBetween (a,a) is closed ;

proof end;

end;

registration

let T be _Tree;
let a be Vertex of T;
cluster T .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 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 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 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 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 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 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 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 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 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 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 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 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 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 b₁ being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₁}

proof end;

uniqueness
for b₁, b₂ being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₁} & (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₂} holds
b₁ = b₂ by ZFMISC_1:6;

end;

:: deftheorem Def3 defines MiddleVertex HELLY:def 3 :
for T being _Tree
for a, b, c, b₅ being Vertex of T holds
( b₅ = MiddleVertex (a,b,c) iff (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b₅} );

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 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 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 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 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 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 end;

theorem :: HELLY:47

for T being _Tree
for a being Vertex of T holds MiddleVertex (a,a,a) = a

proof end;

theorem Th48: :: HELLY:48

for T being _Tree
for a, b being Vertex of T holds MiddleVertex (a,a,b) = a

proof end;

theorem Th49: :: HELLY:49

for T being _Tree
for a, b being Vertex of T holds MiddleVertex (a,b,a) = a

proof end;

theorem :: HELLY:50

for T being _Tree
for a, b being Vertex of T holds MiddleVertex (a,b,b) = b

proof 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 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 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 end;

begin

definition

let F be set ;
attr F 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 end;