let T be _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}
let a, b, c, d be 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 P1, P2 be Path of T; ( 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)))
; ((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}
verumproof
hereby XBOOLE_0:def 10 {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}
;
contradictionthen consider e being
object such that A21:
e in ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices())
and A22:
not
e in {d}
;
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))
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))
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;
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;
verum
end;