let T be _Tree; for a, b being Vertex of T
for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds
P1 = P2
let a, b be Vertex of T; for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds
P1 = P2
let P1, P2 be Path of T; ( P1 is_Walk_from a,b & P2 is_Walk_from a,b implies P1 = P2 )
assume that
A1:
P1 is_Walk_from a,b
and
A2:
P2 is_Walk_from a,b
; P1 = P2
set di = len (maxPrefix (P1,P2));
A3:
( P1 .first() = a & P2 .first() = a )
by A1, A2;
then reconsider di = len (maxPrefix (P1,P2)) as odd Element of NAT by Th22;
defpred S1[ Nat] means ( $1 is odd & di < $1 & $1 <= len P2 & P2 . $1 in P1 .vertices() );
assume A4:
P1 <> P2
; contradiction
A5:
not P2 c= P1
A10:
ex k being Nat st S1[k]
consider ei being Nat such that
A11:
S1[ei]
and
A12:
for n being Nat st S1[n] holds
ei <= n
from NAT_1:sch 5(A10);
reconsider ei = ei as odd Element of NAT by A11, ORDINAL1:def 12;
set e = P2 . ei;
set fi = P1 .find (P2 . ei);
set pde = P2 .cut (di,ei);
set pdf = P1 .cut (di,(P1 .find (P2 . ei)));
A13:
P1 .find (P2 . ei) <= len P1
by A11, GLIB_001:def 19;
set rpdf = (P1 .cut (di,(P1 .find (P2 . ei)))) .reverse() ;
A14:
((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() = (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices()
by GLIB_001:92;
set C = (P2 .cut (di,ei)) .append ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse());
set d = P1 . di;
A15:
P2 . di = P1 . di
by Th7;
then A16:
(P2 .cut (di,ei)) .first() = P1 . di
by A11, GLIB_001:37;
A17:
P2 . ei = P1 . (P1 .find (P2 . ei))
by A11, GLIB_001:def 19;
len P2 <> 1
then A18:
P2 is trivial
by GLIB_001:126;
A19:
di < P1 .find (P2 . ei)
then A20:
P1 .cut (di,(P1 .find (P2 . ei))) is trivial
by A13, GLIB_001:131;
then A21:
P1 is trivial
;
P1 .find (P2 . ei) <= len P1
by A11, GLIB_001:def 19;
then A22:
((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() c= P1 .vertices()
by A19, A14, GLIB_001:94;
A23:
((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) c= {(P2 . ei),(P1 . di)}
proof
assume
not
((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) c= {(P2 . ei),(P1 . di)}
;
contradiction
then consider g being
object such that A24:
g in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices())
and A25:
not
g in {(P2 . ei),(P1 . di)}
;
g in (P2 .cut (di,ei)) .vertices()
by A24, XBOOLE_0:def 4;
then consider gii being
odd Element of
NAT such that A26:
gii <= len (P2 .cut (di,ei))
and A27:
(P2 .cut (di,ei)) . gii = g
by GLIB_001:87;
consider gi being
odd Nat such that A28:
P2 . gi = (P2 .cut (di,ei)) . gii
and A29:
gi = (di + gii) - 1
and A30:
gi <= len P2
by A11, A26, Th12;
reconsider gi =
gi as
odd Element of
NAT by ORDINAL1:def 12;
A31:
gii >= 1
by ABIAN:12;
A32:
gi < ei
gii <> 1
by A16, A25, A27, TARSKI:def 2;
then A35:
gii > 1
by A31, XXREAL_0:1;
A36:
di < gi
g in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()
by A24, XBOOLE_0:def 4;
hence
contradiction
by A12, A22, A27, A28, A30, A36, A32;
verum
end;
A37:
(P2 .cut (di,ei)) .last() = P2 . ei
by A11, GLIB_001:37;
(P1 .cut (di,(P1 .find (P2 . ei)))) .first() = P1 . di
by A13, A19, GLIB_001:37;
then A38:
((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .last() = P1 . di
by GLIB_001:22;
(P1 .cut (di,(P1 .find (P2 . ei)))) .last() = P2 . ei
by A13, A17, A19, GLIB_001:37;
then A39:
((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .first() = P2 . ei
by GLIB_001:22;
{(P2 . ei),(P1 . di)} c= ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices())
then A41:
((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) = {(P2 . ei),(P1 . di)}
by A23;
A42:
P2 .cut (di,ei) is trivial
by A11, GLIB_001:131;
then A43:
P2 is trivial
;
A44:
not P1 c= P2
A49:
(P2 .cut (di,ei)) .edges() misses ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges()
proof
A50:
(P1 .cut (di,(P1 .find (P2 . ei)))) .vertices() = ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()
by GLIB_001:92;
A51:
(P1 .cut (di,(P1 .find (P2 . ei)))) .edges() = ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges()
by GLIB_001:107;
assume
((P2 .cut (di,ei)) .edges()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges()) <> {}
;
XBOOLE_0:def 7 contradiction
then consider x being
object such that A52:
x in ((P2 .cut (di,ei)) .edges()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges())
by XBOOLE_0:def 1;
x in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges()
by A52, XBOOLE_0:def 4;
then consider u1,
u2 being
Vertex of
T,
m being
odd Element of
NAT such that A53:
m + 2
<= len (P1 .cut (di,(P1 .find (P2 . ei))))
and A54:
u1 = (P1 .cut (di,(P1 .find (P2 . ei)))) . m
and
x = (P1 .cut (di,(P1 .find (P2 . ei)))) . (m + 1)
and A55:
u2 = (P1 .cut (di,(P1 .find (P2 . ei)))) . (m + 2)
and A56:
x Joins u1,
u2,
T
by A51, GLIB_001:103;
x in (P2 .cut (di,ei)) .edges()
by A52, XBOOLE_0:def 4;
then consider v1,
v2 being
Vertex of
T,
n being
odd Element of
NAT such that A57:
n + 2
<= len (P2 .cut (di,ei))
and A58:
v1 = (P2 .cut (di,ei)) . n
and
x = (P2 .cut (di,ei)) . (n + 1)
and A59:
v2 = (P2 .cut (di,ei)) . (n + 2)
and A60:
x Joins v1,
v2,
T
by GLIB_001:103;
A61:
n + 0 < n + 2
by XREAL_1:8;
per cases
( v1 <> v2 or v1 = v2 )
;
suppose A62:
v1 <> v2
;
contradictionA63:
n + 2
= (n + 1) + 1
;
then A64:
n + 1
< len (P2 .cut (di,ei))
by A57, NAT_1:13;
then A65:
(P2 .cut (di,ei)) . (n + 2) = P2 . (di + (n + 1))
by A11, A63, GLIB_001:36;
consider ni being
Nat such that A66:
n = ni + 1
by NAT_1:6;
reconsider ni =
ni as
Element of
NAT by ORDINAL1:def 12;
A67:
u2 in (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices()
by A53, A55, GLIB_001:87;
m + 0 < m + 2
by XREAL_1:8;
then A68:
m <= len (P1 .cut (di,(P1 .find (P2 . ei))))
by A53, XXREAL_0:2;
then
u1 in (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices()
by A54, GLIB_001:87;
then A69:
{u1,u2} c= ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()
by A50, A67, ZFMISC_1:32;
A70:
m + 2
= (m + 1) + 1
;
then A71:
m + 1
< len (P1 .cut (di,(P1 .find (P2 . ei))))
by A53, NAT_1:13;
then A72:
(P1 .cut (di,(P1 .find (P2 . ei)))) . (m + 2) = P1 . (di + (m + 1))
by A13, A19, A70, GLIB_001:36;
n <= len (P2 .cut (di,ei))
by A57, A61, XXREAL_0:2;
then A73:
v1 in (P2 .cut (di,ei)) .vertices()
by A58, GLIB_001:87;
v2 in (P2 .cut (di,ei)) .vertices()
by A57, A59, GLIB_001:87;
then A74:
{v1,v2} c= (P2 .cut (di,ei)) .vertices()
by A73, ZFMISC_1:32;
A75:
( (
v1 = u1 &
v2 = u2 ) or (
v1 = u2 &
v2 = u1 ) )
by A60, A56, GLIB_000:15;
then A76:
(
v1 = P2 . ei or
v1 = P1 . di )
by A41, A74, A69, XBOOLE_1:19, ZFMISC_1:22;
n + 0 < n + 2
by XREAL_1:8;
then
n <= len (P2 .cut (di,ei))
by A57, XXREAL_0:2;
then A77:
ni < len (P2 .cut (di,ei))
by A66, NAT_1:13;
then A78:
(P2 .cut (di,ei)) . n = P2 . (di + ni)
by A11, A66, GLIB_001:36;
A79:
P2 . (di + 2) = P2 . ei
proof
per cases
( ( v1 = P2 . ei & v2 = P1 . di ) or ( v1 = P1 . di & v2 = P2 . ei ) )
by A41, A62, A75, A74, A69, A76, XBOOLE_1:19, ZFMISC_1:22;
suppose A80:
(
v1 = P2 . ei &
v2 = P1 . di )
;
P2 . (di + 2) = P2 . ei
di + (n + 2) <= (len (P2 .cut (di,ei))) + di
by A57, XREAL_1:6;
then
((di + n) + 1) + 1
<= ei + 1
by A11, GLIB_001:36;
then
(di + n) + 1
<= ei
by XREAL_1:6;
then A81:
di + (n + 1) <= len P2
by A11, XXREAL_0:2;
di <= di + n
by NAT_1:11;
then
di < (di + n) + 1
by NAT_1:13;
then
(
P2 .first() = P1 . di &
P2 .last() = P1 . di )
by A15, A59, A65, A80, A81, GLIB_001:def 28;
hence
P2 . (di + 2) = P2 . ei
by A43, GLIB_001:def 24;
verum end; suppose A82:
(
v1 = P1 . di &
v2 = P2 . ei )
;
P2 . (di + 2) = P2 . ei
ni = 0
proof
di + ni < (len (P2 .cut (di,ei))) + di
by A77, XREAL_1:6;
then
di + ni < ei + 1
by A11, GLIB_001:36;
then
di + ni <= ei
by NAT_1:13;
then A83:
di + ni <= len P2
by A11, XXREAL_0:2;
assume A84:
ni <> 0
;
contradiction
reconsider ni =
ni as
even Element of
NAT by A66;
di + 0 < di + ni
by A84, XREAL_1:6;
then
(
P2 .first() = P1 . di &
P2 .last() = P1 . di )
by A15, A58, A78, A82, A83, GLIB_001:def 28;
hence
contradiction
by A43, GLIB_001:def 24;
verum
end; hence
P2 . (di + 2) = P2 . ei
by A11, A59, A66, A64, A82, GLIB_001:36;
verum end;
end; consider im being
Nat such that A85:
m = im + 1
by NAT_1:6;
A86:
(
v2 = P2 . ei or
v2 = P1 . di )
by A41, A75, A74, A69, XBOOLE_1:19, ZFMISC_1:22;
reconsider im =
im as
Element of
NAT by ORDINAL1:def 12;
A87:
im < len (P1 .cut (di,(P1 .find (P2 . ei))))
by A68, A85, NAT_1:13;
then A88:
(P1 .cut (di,(P1 .find (P2 . ei)))) . m = P1 . (di + im)
by A13, A19, A85, GLIB_001:36;
P1 . (di + 2) = P2 . ei
proof
per cases
( ( u1 = P2 . ei & u2 = P1 . di ) or ( u1 = P1 . di & u2 = P2 . ei ) )
by A60, A56, A62, A76, A86, GLIB_000:15;
suppose A89:
(
u1 = P2 . ei &
u2 = P1 . di )
;
P1 . (di + 2) = P2 . ei
di + (m + 2) <= (len (P1 .cut (di,(P1 .find (P2 . ei))))) + di
by A53, XREAL_1:6;
then
((di + m) + 1) + 1
<= (P1 .find (P2 . ei)) + 1
by A13, A19, GLIB_001:36;
then
(di + m) + 1
<= P1 .find (P2 . ei)
by XREAL_1:6;
then A90:
di + (m + 1) <= len P1
by A13, XXREAL_0:2;
di <= di + m
by NAT_1:11;
then
di < (di + m) + 1
by NAT_1:13;
then
(
P1 .first() = P1 . di &
P1 .last() = P1 . di )
by A55, A72, A89, A90, GLIB_001:def 28;
hence
P1 . (di + 2) = P2 . ei
by A21, GLIB_001:def 24;
verum end; suppose A91:
(
u1 = P1 . di &
u2 = P2 . ei )
;
P1 . (di + 2) = P2 . ei
im = 0
proof
di + im < (len (P1 .cut (di,(P1 .find (P2 . ei))))) + di
by A87, XREAL_1:6;
then
di + im < (P1 .find (P2 . ei)) + 1
by A13, A19, GLIB_001:36;
then
di + im <= P1 .find (P2 . ei)
by NAT_1:13;
then A92:
di + im <= len P1
by A13, XXREAL_0:2;
assume A93:
im <> 0
;
contradiction
reconsider im =
im as
even Element of
NAT by A85;
di + 0 < di + im
by A93, XREAL_1:6;
then
(
P1 .first() = P1 . di &
P1 .last() = P1 . di )
by A54, A88, A91, A92, GLIB_001:def 28;
hence
contradiction
by A21, GLIB_001:def 24;
verum
end; hence
P1 . (di + 2) = P2 . ei
by A13, A19, A55, A85, A71, A91, GLIB_001:36;
verum end;
end; hence
contradiction
by A3, A44, A5, A79, Th24;
verum end;
end;
(P1 .cut (di,(P1 .find (P2 . ei)))) .reverse() is trivial
by A20, GLIB_001:129;
then
(P2 .cut (di,ei)) .append ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) is Cycle-like
by A42, A16, A37, A39, A38, A41, A49, Th20;
hence
contradiction
; verum