HELLY: Helly property for subtrees

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

proof end;

uniqueness ;
commutativity ;

end;

:: deftheorem Def1 defines maxPrefix HELLY:def 1 :

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;

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 W .cut (m,n) is V5() holds
not W is V5()

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 for Walk of G;

correctness 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 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 V5() & 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() & 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 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 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 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
len (maxPrefix (W1,W2)) is odd

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;

registration

let T be _Tree;

cluster Trail-like -> Path-like for Walk of T;

correctness

proof end;

end;

theorem Th25: :: HELLY:25

for T being _Tree
for P being Path of T st P is V5() holds
P is open by GLIB_001:def 31, GLIB_002:def 2;

registration

let T be _Tree;

cluster V5() Path-like -> open for Walk of T;

correctness 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

proof end;

uniqueness by Th27;

end;

:: deftheorem Def2 defines .pathBetween HELLY:def 2 :

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) -> V5() ;

correctness ;

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;

:: deftheorem Def3 defines MiddleVertex HELLY:def 3 :

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

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 :

:: At some point one would like to define allSubtrees of a Tree
:: The claim below does not hold when T is infinite and we consider
:: infinite families of subtrees. Example: half-line tree with
:: subtrees T_i = {j >= i}.
:: main Prop4p7:

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;