let T be _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)))}
let a, b, c be 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 P1, P4 be Path of T; ( 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
; ((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;
(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:8, 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:38;
then A12:
((P1 .cut i9,(len P1)) .reverse() ) .last() = x
by GLIB_001:23;
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:27;
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:33;
set P2 = T .pathBetween b,c;
A14:
x in P1 .vertices()
by A11, GLIB_001:88;
A15: P1 . (len P1) =
P1 .last()
.=
b
by A1, Th28
;
then
(P1 .cut i9,(len P1)) .last() = b
by A11, GLIB_001:38;
then A16:
((P1 .cut i9,(len P1)) .reverse() ) .first() = b
by GLIB_001:23;
A17:
x = P4 . i9
by Th7;
then
x <> b
by A8, A5, A9, GLIB_001:88;
then A18:
not (P1 .cut i9,(len P1)) .reverse() is closed
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:38;
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:30;
P1 .cut i9,(len P1) is_Walk_from x,b
by A11, A15, GLIB_001:38;
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:93;
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:12;
A23:
(P4 .cut i9,(len P4)) .vertices() c= P4 .vertices()
by A9, GLIB_001:95;
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()
;
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:104;
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:88;
v2br in ((P1 .cut i9,(len P1)) .reverse() ) .vertices()
by A26, A28, GLIB_001:88;
then A31:
{v1br,v2br} c= ((P1 .cut i9,(len P1)) .reverse() ) .vertices()
by A30, ZFMISC_1:38;
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:104;
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:88;
A37:
( (
v1br = v1c &
v2br = v2c ) or (
v1br = v2c &
v2br = v1c ) )
by A29, A35, GLIB_000:18;
A38:
v2c in (P4 .cut i9,(len P4)) .vertices()
by A32, A34, GLIB_001:88;
then
{v1c,v2c} c= (P4 .cut i9,(len P4)) .vertices()
by A36, ZFMISC_1:38;
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:28;
(
v1c = b or
v1c = x )
by A12, A16, A22, A39, XBOOLE_1:1, ZFMISC_1:28;
hence
contradiction
by A8, A5, A23, A35, A36, A38, A40, GLIB_000:21;
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:31;
then
x <> c
by A11, GLIB_001:88;
then A43:
not P4 .cut i9,(len P4) is closed
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:88;
A45:
x in P4 .vertices()
by A9, A17, GLIB_001:88;
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 ;
TARSKI:def 3 ( 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:94;
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:94;
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:94;
assume A55:
z in ((P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() )
;
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;
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:37;
hence
((P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {(P1 . (len (maxPrefix P1,P4)))}
by A46, XBOOLE_0:def 10; verum