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:7, 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:37;
then A12:
((P1 .cut (i9,(len P1))) .reverse()) .last() = x
by GLIB_001:22;
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:25;
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:32;
set P2 = T .pathBetween (b,c);
A14:
x in P1 .vertices()
by A11, GLIB_001:87;
A15: P1 . (len P1) =
P1 .last()
.=
b
by A1, Th28
;
then
(P1 .cut (i9,(len P1))) .last() = b
by A11, GLIB_001:37;
then A16:
((P1 .cut (i9,(len P1))) .reverse()) .first() = b
by GLIB_001:22;
A17:
x = P4 . i9
by Th7;
then
x <> b
by A8, A5, A9, GLIB_001:87;
then A18:
(P1 .cut (i9,(len P1))) .reverse() is open
by A12, A16;
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:37;
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:29;
P1 .cut (i9,(len P1)) is_Walk_from x,b
by A11, A15, GLIB_001:37;
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:92;
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:7;
A23:
(P4 .cut (i9,(len P4))) .vertices() c= P4 .vertices()
by A9, GLIB_001:94;
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()) <> {}
;
then consider e being
object 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:103;
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:87;
v2br in ((P1 .cut (i9,(len P1))) .reverse()) .vertices()
by A26, A28, GLIB_001:87;
then A31:
{v1br,v2br} c= ((P1 .cut (i9,(len P1))) .reverse()) .vertices()
by A30, ZFMISC_1:32;
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:103;
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:87;
A37:
( (
v1br = v1c &
v2br = v2c ) or (
v1br = v2c &
v2br = v1c ) )
by A29, A35, GLIB_000:15;
A38:
v2c in (P4 .cut (i9,(len P4))) .vertices()
by A32, A34, GLIB_001:87;
then
{v1c,v2c} c= (P4 .cut (i9,(len P4))) .vertices()
by A36, ZFMISC_1:32;
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:22;
(
v1c = b or
v1c = x )
by A12, A16, A22, A39, XBOOLE_1:1, ZFMISC_1:22;
hence
contradiction
by A8, A5, A23, A35, A36, A38, A40, GLIB_000:18;
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:30;
then
x <> c
by A11, GLIB_001:87;
then A43:
P4 .cut (i9,(len P4)) is open
by A20, A41;
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:87;
A45:
x in P4 .vertices()
by A9, A17, GLIB_001:87;
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
object ;
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:93;
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:93;
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:93;
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:31;
hence
((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))}
by A46; verum