let T be _Tree; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: ((P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {(P1 . (len (maxPrefix P1,P4)))}
set P2 = T .pathBetween b,c;
set P3 = T .pathBetween c,a;
A7:
(T .pathBetween c,a) .vertices() = P4 .vertices()
by A2, Th31;
P1 .first() = a
by A1, Th27;
then A8:
P1 .first() = P4 .first()
by A2, Th27;
set i = len (maxPrefix P1,P4);
reconsider i' = len (maxPrefix P1,P4) as odd Element of NAT by A8, Th21;
A9:
len (maxPrefix P1,P4) <= (len (maxPrefix P1,P4)) + 2
by NAT_1:11;
A10:
(len (maxPrefix P1,P4)) + 2 <= len P1
by A3, A8, Th22;
then A11:
len (maxPrefix P1,P4) <= len P1
by A9, XXREAL_0:2;
(len (maxPrefix P1,P4)) + 2 <= len P4
by A4, A8, Th22;
then A12:
len (maxPrefix P1,P4) <= len P4
by A9, XXREAL_0:2;
set x = P1 . i';
reconsider x = P1 . i' as Vertex of T by A9, A10, GLIB_001:8, XXREAL_0:2;
set P1b = P1 .cut i',(len P1);
set P4c = P4 .cut i',(len P4);
A13:
(P1 .cut i',(len P1)) .first() = P1 . i'
by A11, GLIB_001:38;
A14: P1 . (len P1) =
P1 .last()
.=
b
by A1, Th27
;
then A15:
P1 .cut i',(len P1) is_Walk_from x,b
by A11, GLIB_001:38;
A16:
(P1 .cut i',(len P1)) .last() = b
by A11, A14, GLIB_001:38;
A17:
x = P4 . i'
by Th7;
then A18:
x <> b
by A6, A7, A12, GLIB_001:88;
A19:
x <> c
by A5, A11, GLIB_001:88;
P4 . (len P4) =
P4 .last()
.=
c
by A2, Th27
;
then A20:
P4 .cut i',(len P4) is_Walk_from x,c
by A12, A17, GLIB_001:38;
A21:
P1 .cut i',(len P1) = T .pathBetween x,b
by A15, Def2;
A22:
P4 .cut i',(len P4) = T .pathBetween x,c
by A20, Def2;
A23:
(P4 .cut i',(len P4)) .vertices() c= P4 .vertices()
by A12, GLIB_001:95;
set P1br = (P1 .cut i',(len P1)) .reverse() ;
set Pbc = ((P1 .cut i',(len P1)) .reverse() ) .append (P4 .cut i',(len P4));
A24:
((P1 .cut i',(len P1)) .reverse() ) .last() = x
by A13, GLIB_001:23;
A25:
(P4 .cut i',(len P4)) .first() = x
by A22, Th27;
A26:
((P1 .cut i',(len P1)) .reverse() ) .first() = b
by A16, GLIB_001:23;
A27:
(P4 .cut i',(len P4)) .last() = c
by A22, Th27;
set j = len ((P1 .cut i',(len P1)) .reverse() );
A28:
len ((P1 .cut i',(len P1)) .reverse() ) <= len (((P1 .cut i',(len P1)) .reverse() ) .append (P4 .cut i',(len P4)))
by A24, A25, GLIB_001:30;
1 <= len ((P1 .cut i',(len P1)) .reverse() )
by CHORD:2;
then
len ((P1 .cut i',(len P1)) .reverse() ) in dom ((P1 .cut i',(len P1)) .reverse() )
by FINSEQ_3:27;
then A29:
(((P1 .cut i',(len P1)) .reverse() ) .append (P4 .cut i',(len P4))) . (len ((P1 .cut i',(len P1)) .reverse() )) = x
by A24, GLIB_001:33;
A30:
not (P1 .cut i',(len P1)) .reverse() is closed
by A18, A24, A26, GLIB_001:def 24;
A31:
not P4 .cut i',(len P4) is closed
by A19, A25, A27, GLIB_001:def 24;
A32:
((P1 .cut i',(len P1)) .reverse() ) .vertices() = (P1 .cut i',(len P1)) .vertices()
by GLIB_001:93;
((P1 .cut i',(len P1)) .vertices() ) /\ ((P4 .cut i',(len P4)) .vertices() ) = {x}
by A1, A2, A3, A4, A21, A22, Th39;
then A33:
(((P1 .cut i',(len P1)) .reverse() ) .vertices() ) /\ ((P4 .cut i',(len P4)) .vertices() ) c= {(((P1 .cut i',(len P1)) .reverse() ) .first() ),(((P1 .cut i',(len P1)) .reverse() ) .last() )}
by A24, A32, ZFMISC_1:12;
A34:
not ((P1 .cut i',(len P1)) .reverse() ) .first() in (P4 .cut i',(len P4)) .vertices()
by A6, A7, A23, A26;
((P1 .cut i',(len P1)) .reverse() ) .edges() misses (P4 .cut i',(len P4)) .edges()
proof
assume
not
((P1 .cut i',(len P1)) .reverse() ) .edges() misses (P4 .cut i',(len P4)) .edges()
;
:: thesis: contradiction
then
(((P1 .cut i',(len P1)) .reverse() ) .edges() ) /\ ((P4 .cut i',(len P4)) .edges() ) <> {}
by XBOOLE_0:def 7;
then consider e being
set such that A35:
e in (((P1 .cut i',(len P1)) .reverse() ) .edges() ) /\ ((P4 .cut i',(len P4)) .edges() )
by XBOOLE_0:def 1;
A36:
e in ((P1 .cut i',(len P1)) .reverse() ) .edges()
by A35, XBOOLE_0:def 4;
A37:
e in (P4 .cut i',(len P4)) .edges()
by A35, XBOOLE_0:def 4;
consider v1br,
v2br being
Vertex of
T,
n being
odd Element of
NAT such that A38:
n + 2
<= len ((P1 .cut i',(len P1)) .reverse() )
and A39:
v1br = ((P1 .cut i',(len P1)) .reverse() ) . n
and
e = ((P1 .cut i',(len P1)) .reverse() ) . (n + 1)
and A40:
v2br = ((P1 .cut i',(len P1)) .reverse() ) . (n + 2)
and A41:
e Joins v1br,
v2br,
T
by A36, GLIB_001:104;
consider v1c,
v2c being
Vertex of
T,
m being
odd Element of
NAT such that A42:
m + 2
<= len (P4 .cut i',(len P4))
and A43:
v1c = (P4 .cut i',(len P4)) . m
and
e = (P4 .cut i',(len P4)) . (m + 1)
and A44:
v2c = (P4 .cut i',(len P4)) . (m + 2)
and A45:
e Joins v1c,
v2c,
T
by A37, GLIB_001:104;
A46:
( (
v1br = v1c &
v2br = v2c ) or (
v1br = v2c &
v2br = v1c ) )
by A41, A45, GLIB_000:18;
n <= n + 2
by NAT_1:11;
then
n <= len ((P1 .cut i',(len P1)) .reverse() )
by A38, XXREAL_0:2;
then
(
v1br in ((P1 .cut i',(len P1)) .reverse() ) .vertices() &
v2br in ((P1 .cut i',(len P1)) .reverse() ) .vertices() )
by A38, A39, A40, GLIB_001:88;
then A47:
{v1br,v2br} c= ((P1 .cut i',(len P1)) .reverse() ) .vertices()
by ZFMISC_1:38;
m <= m + 2
by NAT_1:11;
then
m <= len (P4 .cut i',(len P4))
by A42, XXREAL_0:2;
then A48:
(
v1c in (P4 .cut i',(len P4)) .vertices() &
v2c in (P4 .cut i',(len P4)) .vertices() )
by A42, A43, A44, GLIB_001:88;
then
{v1c,v2c} c= (P4 .cut i',(len P4)) .vertices()
by ZFMISC_1:38;
then
{v1c,v2c} c= (((P1 .cut i',(len P1)) .reverse() ) .vertices() ) /\ ((P4 .cut i',(len P4)) .vertices() )
by A46, A47, XBOOLE_1:19;
then
( (
v1c = b or
v1c = x ) & (
v2c = b or
v2c = x ) )
by A24, A26, A33, XBOOLE_1:1, ZFMISC_1:28;
hence
contradiction
by A6, A7, A23, A45, A48, GLIB_000:21;
:: thesis: verum
end;
then A49:
((P1 .cut i',(len P1)) .reverse() ) .append (P4 .cut i',(len P4)) is Path of T
by A24, A25, A30, A31, A33, A34, Th17;
((P1 .cut i',(len P1)) .reverse() ) .append (P4 .cut i',(len P4)) is_Walk_from b,c
by A24, A25, A26, A27, GLIB_001:31;
then A50:
((P1 .cut i',(len P1)) .reverse() ) .append (P4 .cut i',(len P4)) = T .pathBetween b,c
by A49, Def2;
A51:
x in P1 .vertices()
by A11, GLIB_001:88;
A52:
x in P4 .vertices()
by A12, A17, GLIB_001:88;
A53:
x in (T .pathBetween b,c) .vertices()
by A28, A29, A50, GLIB_001:88;
then
x in (P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )
by A51, XBOOLE_0:def 4;
then
x in ((P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() )
by A7, A52, XBOOLE_0:def 4;
then A54:
{x} c= ((P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() )
by ZFMISC_1:37;
((P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) c= {x}
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in ((P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) or z in {x} )
assume A55:
z in ((P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() )
;
:: thesis: z in {x}
then A56:
z in (P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )
by XBOOLE_0:def 4;
then A57:
z in P1 .vertices()
by XBOOLE_0:def 4;
A58:
z in (T .pathBetween b,c) .vertices()
by A56, XBOOLE_0:def 4;
A59:
z in (T .pathBetween c,a) .vertices()
by A55, XBOOLE_0:def 4;
set Pax =
T .pathBetween a,
x;
set Pxb =
T .pathBetween x,
b;
set Pbx =
T .pathBetween b,
x;
set Pxc =
T .pathBetween x,
c;
set Pcx =
T .pathBetween c,
x;
set Pxa =
T .pathBetween x,
a;
A60:
P1 = (T .pathBetween a,x) .append (T .pathBetween x,b)
by A1, A51, Th35;
A61:
T .pathBetween b,
c = (T .pathBetween b,x) .append (T .pathBetween x,c)
by A53, Th35;
A62:
T .pathBetween c,
a = (T .pathBetween c,x) .append (T .pathBetween x,a)
by A7, A52, Th35;
(T .pathBetween a,x) .last() =
x
by Th27
.=
(T .pathBetween x,b) .first()
by Th27
;
then
P1 .vertices() = ((T .pathBetween a,x) .vertices() ) \/ ((T .pathBetween x,b) .vertices() )
by A60, GLIB_001:94;
then A63:
(
z in (T .pathBetween a,x) .vertices() or
z in (T .pathBetween x,b) .vertices() )
by A57, XBOOLE_0:def 3;
(T .pathBetween b,x) .last() =
x
by Th27
.=
(T .pathBetween x,c) .first()
by Th27
;
then
(T .pathBetween b,c) .vertices() = ((T .pathBetween b,x) .vertices() ) \/ ((T .pathBetween x,c) .vertices() )
by A61, GLIB_001:94;
then A64:
(
z in (T .pathBetween b,x) .vertices() or
z in (T .pathBetween x,c) .vertices() )
by A58, XBOOLE_0:def 3;
(T .pathBetween c,x) .last() =
x
by Th27
.=
(T .pathBetween x,a) .first()
by Th27
;
then
(T .pathBetween c,a) .vertices() = ((T .pathBetween c,x) .vertices() ) \/ ((T .pathBetween x,a) .vertices() )
by A62, GLIB_001:94;
then A65:
(
z in (T .pathBetween c,x) .vertices() or
z in (T .pathBetween x,a) .vertices() )
by A59, XBOOLE_0:def 3;
A66:
(T .pathBetween b,x) .vertices() = (T .pathBetween x,b) .vertices()
by Th31;
A67:
(T .pathBetween c,x) .vertices() = (T .pathBetween x,c) .vertices()
by Th31;
end;
hence
((P1 .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {(P1 . (len (maxPrefix P1,P4)))}
by A54, XBOOLE_0:def 10; :: thesis: verum