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}
A6:
P1 .first() = a
by A1, Th27;
A7:
P2 .first() = a
by A2, Th27;
set di = len (maxPrefix P1,P2);
reconsider di = len (maxPrefix P1,P2) as odd Element of NAT by A6, A7, Th21;
A8:
d = P2 . (len (maxPrefix P1,P2))
by A5, Th7;
A9:
di + 2 <= len P1
by A3, A6, A7, Th22;
di <= di + 2
by NAT_1:11;
then A10:
di <= len P1
by A9, XXREAL_0:2;
A11:
di + 2 <= len P2
by A4, A6, A7, Th22;
di <= di + 2
by NAT_1:11;
then A12:
di <= len P2
by A11, XXREAL_0:2;
A13:
1 <= di
by HEYTING3:1;
set Pdb = T .pathBetween d,b;
A14:
(T .pathBetween d,b) .first() = d
by Th27;
A15: (T .pathBetween d,b) . 1 =
(T .pathBetween d,b) .first()
.=
d
by Th27
;
set Pdc = T .pathBetween d,c;
A16:
(T .pathBetween d,c) .first() = d
by Th27;
A17: (T .pathBetween d,c) . 1 =
(T .pathBetween d,c) .first()
.=
d
by Th27
;
set Pad = T .pathBetween a,d;
A18:
(T .pathBetween a,d) .last() = d
by Th27;
d in P1 .vertices()
by A5, A10, GLIB_001:88;
then A19:
P1 = (T .pathBetween a,d) .append (T .pathBetween d,b)
by A1, Th35;
d in P2 .vertices()
by A8, A12, GLIB_001:88;
then A20:
P2 = (T .pathBetween a,d) .append (T .pathBetween d,c)
by A2, Th35;
T .pathBetween a,d = P1 .cut ((2 * 0 ) + 1),di
by A5, A6, A10, A13, Th34;
then A21:
(len (T .pathBetween a,d)) + ((2 * 0 ) + 1) = di + 1
by A10, A13, GLIB_001:37;
thus
((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) = {d}
:: thesis: verumproof
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: contradictionthen consider e being
set such that A22:
e in ((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() )
and A23:
not
e in {d}
by TARSKI:def 3;
A24:
e in (T .pathBetween d,b) .vertices()
by A22, XBOOLE_0:def 4;
A25:
e in (T .pathBetween d,c) .vertices()
by A22, XBOOLE_0:def 4;
reconsider e =
e as
Vertex of
T by A22;
consider ebi being
odd Element of
NAT such that A26:
ebi <= len (T .pathBetween d,b)
and A27:
e = (T .pathBetween d,b) . ebi
by A24, GLIB_001:88;
A28:
1
<= ebi
by HEYTING3:1;
consider eci being
odd Element of
NAT such that A29:
eci <= len (T .pathBetween d,c)
and A30:
e = (T .pathBetween d,c) . eci
by A25, GLIB_001:88;
A31:
1
<= eci
by HEYTING3:1;
set Pdeb =
(T .pathBetween d,b) .cut 1,
ebi;
set Pdec =
(T .pathBetween d,c) .cut 1,
eci;
(2 * 0 ) + 1 is
odd Element of
NAT
;
then A32:
(T .pathBetween d,b) .cut 1,
ebi is_Walk_from d,
e
by A15, A26, A27, A28, GLIB_001:38;
(2 * 0 ) + 1 is
odd Element of
NAT
;
then A33:
(T .pathBetween d,c) .cut 1,
eci is_Walk_from d,
e
by A17, A29, A30, A31, GLIB_001:38;
1
< len ((T .pathBetween d,b) .cut 1,ebi)
then A35:
((2 * 0 ) + 1) + 2
<= len ((T .pathBetween d,b) .cut 1,ebi)
by CHORD:4;
1
< len ((T .pathBetween d,c) .cut 1,eci)
then A37:
((2 * 0 ) + 1) + 2
<= len ((T .pathBetween d,c) .cut 1,eci)
by CHORD:4;
A38:
((T .pathBetween d,b) .cut 1,ebi) . (1 + 2) = ((T .pathBetween d,c) .cut 1,eci) . (1 + 2)
by A32, A33, Th26;
A39:
len ((T .pathBetween d,b) .cut 1,ebi) <= len (T .pathBetween d,b)
by Th10;
2
< len ((T .pathBetween d,b) .cut 1,ebi)
by A35, XXREAL_0:2;
then
2
< len (T .pathBetween d,b)
by A39, XXREAL_0:2;
then A40:
P1 . (di + 2) = (T .pathBetween d,b) . (1 + 2)
by A14, A18, A19, A21, GLIB_001:34;
1
+ 2
in dom ((T .pathBetween d,b) .cut 1,ebi)
by A35, FINSEQ_3:27;
then A41:
((T .pathBetween d,b) .cut 1,ebi) . (1 + 2) = (T .pathBetween d,b) . (1 + 2)
by A26, GLIB_001:47;
A42:
len ((T .pathBetween d,c) .cut 1,eci) <= len (T .pathBetween d,c)
by Th10;
2
< len ((T .pathBetween d,c) .cut 1,eci)
by A37, XXREAL_0:2;
then
2
< len (T .pathBetween d,c)
by A42, XXREAL_0:2;
then A43:
P2 . (di + 2) = (T .pathBetween d,c) . (1 + 2)
by A16, A18, A20, A21, GLIB_001:34;
1
+ 2
in dom ((T .pathBetween d,c) .cut 1,eci)
by A37, FINSEQ_3:27;
hence
contradiction
by A3, A4, A6, A7, A29, A38, A40, A41, A43, Th23, GLIB_001:47;
:: thesis: verum
end;
(
d in (T .pathBetween d,b) .vertices() &
d in (T .pathBetween d,c) .vertices() )
by A14, A16, GLIB_001:89;
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:37;
:: thesis: verum
end;