let T be _Tree; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: P1 = P2
A3:
P1 .first() = a
by A1, GLIB_001:def 23;
A4:
P2 .first() = a
by A2, GLIB_001:def 23;
assume A5:
P1 <> P2
; :: thesis: contradiction
A6:
not P1 c= P2
A12:
not P2 c= P1
set di = len (maxPrefix P1,P2);
reconsider di = len (maxPrefix P1,P2) as odd Element of NAT by A3, A4, Th21;
set d = P1 . di;
defpred S1[ Nat] means ( not $1 is even & di < $1 & $1 <= len P2 & P2 . $1 in P1 .vertices() );
A18:
ex k being Nat st S1[k]
consider ei being Nat such that
A20:
S1[ei]
and
A21:
for n being Nat st S1[n] holds
ei <= n
from NAT_1:sch 5(A18);
reconsider ei = ei as odd Element of NAT by A20, ORDINAL1:def 13;
set e = P2 . ei;
set fi = P1 .find (P2 . ei);
A22:
P1 .find (P2 . ei) <= len P1
by A20, GLIB_001:def 19;
A23:
P2 . ei = P1 . (P1 .find (P2 . ei))
by A20, GLIB_001:def 19;
len P2 <> 1
then A24:
not P2 is trivial
by GLIB_001:127;
A25:
di < P1 .find (P2 . ei)
set pde = P2 .cut di,ei;
set pdf = P1 .cut di,(P1 .find (P2 . ei));
A28:
not P2 .cut di,ei is trivial
by A20, GLIB_001:132;
then A29:
not P2 .cut di,ei is closed
;
A30:
P2 . di = P1 . di
by Th7;
then A31:
(P2 .cut di,ei) .first() = P1 . di
by A20, GLIB_001:38;
A32:
(P2 .cut di,ei) .last() = P2 . ei
by A20, GLIB_001:38;
set rpdf = (P1 .cut di,(P1 .find (P2 . ei))) .reverse() ;
A33:
not P1 .cut di,(P1 .find (P2 . ei)) is trivial
by A22, A25, GLIB_001:132;
then
not (P1 .cut di,(P1 .find (P2 . ei))) .reverse() is trivial
by GLIB_001:130;
then A34:
not (P1 .cut di,(P1 .find (P2 . ei))) .reverse() is closed
;
not P1 is trivial
by A33;
then A35:
not P1 is closed
;
not P2 is trivial
by A28;
then A36:
not P2 is closed
;
(P1 .cut di,(P1 .find (P2 . ei))) .last() = P2 . ei
by A22, A23, A25, GLIB_001:38;
then A37:
((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .first() = P2 . ei
by GLIB_001:23;
(P1 .cut di,(P1 .find (P2 . ei))) .first() = P1 . di
by A22, A25, GLIB_001:38;
then A38:
((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .last() = P1 . di
by GLIB_001:23;
A39:
P1 .find (P2 . ei) <= len P1
by A20, GLIB_001:def 19;
((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices() = (P1 .cut di,(P1 .find (P2 . ei))) .vertices()
by GLIB_001:93;
then A40:
((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices() c= P1 .vertices()
by A25, A39, GLIB_001:95;
set C = (P2 .cut di,ei) .append ((P1 .cut di,(P1 .find (P2 . ei))) .reverse() );
A41:
((P2 .cut di,ei) .vertices() ) /\ (((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices() ) = {(P2 . ei),(P1 . di)}
proof
thus
((P2 .cut di,ei) .vertices() ) /\ (((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices() ) c= {(P2 . ei),(P1 . di)}
:: according to XBOOLE_0:def 10 :: thesis: {(P2 . ei),(P1 . di)} c= ((P2 .cut di,ei) .vertices() ) /\ (((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices() )proof
assume
not
((P2 .cut di,ei) .vertices() ) /\ (((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices() ) c= {(P2 . ei),(P1 . di)}
;
:: thesis: contradiction
then consider g being
set such that A42:
g in ((P2 .cut di,ei) .vertices() ) /\ (((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices() )
and A43:
not
g in {(P2 . ei),(P1 . di)}
by TARSKI:def 3;
g in (P2 .cut di,ei) .vertices()
by A42, XBOOLE_0:def 4;
then consider gii being
odd Element of
NAT such that A44:
gii <= len (P2 .cut di,ei)
and A45:
(P2 .cut di,ei) . gii = g
by GLIB_001:88;
consider gi being
odd Nat such that A46:
P2 . gi = (P2 .cut di,ei) . gii
and A47:
gi = (di + gii) - 1
and A48:
gi <= len P2
by A20, A44, Th12;
reconsider gi =
gi as
odd Element of
NAT by ORDINAL1:def 13;
A49:
gii <> 1
by A31, A43, A45, TARSKI:def 2;
gii >= 1
by HEYTING3:1;
then A50:
gii > 1
by A49, XXREAL_0:1;
A51:
di < gi
A52:
gi < ei
g in ((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices()
by A42, XBOOLE_0:def 4;
hence
contradiction
by A21, A40, A45, A46, A48, A51, A52;
:: thesis: verum
end;
thus
{(P2 . ei),(P1 . di)} c= ((P2 .cut di,ei) .vertices() ) /\ (((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices() )
:: thesis: verum
end;
(P2 .cut di,ei) .edges() misses ((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .edges()
proof
assume
((P2 .cut di,ei) .edges() ) /\ (((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .edges() ) <> {}
;
:: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being
set such that A56:
x in ((P2 .cut di,ei) .edges() ) /\ (((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .edges() )
by XBOOLE_0:def 1;
A57:
x in (P2 .cut di,ei) .edges()
by A56, XBOOLE_0:def 4;
A58:
x in ((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .edges()
by A56, XBOOLE_0:def 4;
A59:
(P1 .cut di,(P1 .find (P2 . ei))) .edges() = ((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .edges()
by GLIB_001:108;
A60:
(P1 .cut di,(P1 .find (P2 . ei))) .vertices() = ((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices()
by GLIB_001:93;
consider v1,
v2 being
Vertex of
T,
n being
odd Element of
NAT such that A61:
n + 2
<= len (P2 .cut di,ei)
and A62:
v1 = (P2 .cut di,ei) . n
and
x = (P2 .cut di,ei) . (n + 1)
and A63:
v2 = (P2 .cut di,ei) . (n + 2)
and A64:
x Joins v1,
v2,
T
by A57, GLIB_001:104;
consider u1,
u2 being
Vertex of
T,
m being
odd Element of
NAT such that A65:
m + 2
<= len (P1 .cut di,(P1 .find (P2 . ei)))
and A66:
u1 = (P1 .cut di,(P1 .find (P2 . ei))) . m
and
x = (P1 .cut di,(P1 .find (P2 . ei))) . (m + 1)
and A67:
u2 = (P1 .cut di,(P1 .find (P2 . ei))) . (m + 2)
and A68:
x Joins u1,
u2,
T
by A58, A59, GLIB_001:104;
A69:
n + 0 < n + 2
by XREAL_1:10;
per cases
( v1 <> v2 or v1 = v2 )
;
suppose A70:
v1 <> v2
;
:: thesis: contradiction
n <= len (P2 .cut di,ei)
by A61, A69, XXREAL_0:2;
then A71:
v1 in (P2 .cut di,ei) .vertices()
by A62, GLIB_001:88;
A72:
v2 in (P2 .cut di,ei) .vertices()
by A61, A63, GLIB_001:88;
n + 0 < n + 2
by XREAL_1:10;
then A73:
n <= len (P2 .cut di,ei)
by A61, XXREAL_0:2;
m + 0 < m + 2
by XREAL_1:10;
then A74:
m <= len (P1 .cut di,(P1 .find (P2 . ei)))
by A65, XXREAL_0:2;
then A75:
u1 in (P1 .cut di,(P1 .find (P2 . ei))) .vertices()
by A66, GLIB_001:88;
A76:
u2 in (P1 .cut di,(P1 .find (P2 . ei))) .vertices()
by A65, A67, GLIB_001:88;
A77:
( (
v1 = u1 &
v2 = u2 ) or (
v1 = u2 &
v2 = u1 ) )
by A64, A68, GLIB_000:18;
A78:
{v1,v2} c= (P2 .cut di,ei) .vertices()
by A71, A72, ZFMISC_1:38;
{u1,u2} c= ((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) .vertices()
by A60, A75, A76, ZFMISC_1:38;
then A79:
( (
v1 = P2 . ei or
v1 = P1 . di ) & (
v2 = P2 . ei or
v2 = P1 . di ) )
by A41, A77, A78, XBOOLE_1:19, ZFMISC_1:28;
1
<= m
by HEYTING3:1;
then consider im being
Nat such that A80:
m = im + 1
by NAT_1:6;
reconsider im =
im as
Element of
NAT by ORDINAL1:def 13;
A81:
im < len (P1 .cut di,(P1 .find (P2 . ei)))
by A74, A80, NAT_1:13;
then A82:
(P1 .cut di,(P1 .find (P2 . ei))) . m = P1 . (di + im)
by A22, A25, A80, GLIB_001:37;
A83:
m + 2
= (m + 1) + 1
;
then A84:
m + 1
< len (P1 .cut di,(P1 .find (P2 . ei)))
by A65, NAT_1:13;
then A85:
(P1 .cut di,(P1 .find (P2 . ei))) . (m + 2) = P1 . (di + (m + 1))
by A22, A25, A83, GLIB_001:37;
1
<= n
by HEYTING3:1;
then consider ni being
Nat such that A86:
n = ni + 1
by NAT_1:6;
reconsider ni =
ni as
Element of
NAT by ORDINAL1:def 13;
A87:
ni < len (P2 .cut di,ei)
by A73, A86, NAT_1:13;
then A88:
(P2 .cut di,ei) . n = P2 . (di + ni)
by A20, A86, GLIB_001:37;
A89:
n + 2
= (n + 1) + 1
;
then A90:
n + 1
< len (P2 .cut di,ei)
by A61, NAT_1:13;
then A91:
(P2 .cut di,ei) . (n + 2) = P2 . (di + (n + 1))
by A20, A89, GLIB_001:37;
A92:
P1 . (di + 2) = P2 . ei
proof
per cases
( ( u1 = P2 . ei & u2 = P1 . di ) or ( u1 = P1 . di & u2 = P2 . ei ) )
by A64, A68, A70, A79, GLIB_000:18;
suppose A93:
(
u1 = P2 . ei &
u2 = P1 . di )
;
:: thesis: P1 . (di + 2) = P2 . ei
di <= di + m
by NAT_1:11;
then A94:
di < (di + m) + 1
by NAT_1:13;
di + (m + 2) <= (len (P1 .cut di,(P1 .find (P2 . ei)))) + di
by A65, XREAL_1:8;
then
((di + m) + 1) + 1
<= (P1 .find (P2 . ei)) + 1
by A22, A25, GLIB_001:37;
then
(di + m) + 1
<= P1 .find (P2 . ei)
by XREAL_1:8;
then
di + (m + 1) <= len P1
by A22, XXREAL_0:2;
then
(
P1 .first() = P1 . di &
P1 .last() = P1 . di )
by A67, A85, A93, A94, GLIB_001:def 28;
hence
P1 . (di + 2) = P2 . ei
by A35, GLIB_001:def 24;
:: thesis: verum end; suppose A95:
(
u1 = P1 . di &
u2 = P2 . ei )
;
:: thesis: P1 . (di + 2) = P2 . ei
im = 0
proof
assume A96:
im <> 0
;
:: thesis: contradiction
di + im < (len (P1 .cut di,(P1 .find (P2 . ei)))) + di
by A81, XREAL_1:8;
then
di + im < (P1 .find (P2 . ei)) + 1
by A22, A25, GLIB_001:37;
then
di + im <= P1 .find (P2 . ei)
by NAT_1:13;
then A97:
di + im <= len P1
by A22, XXREAL_0:2;
m - 1
= im
by A80;
then reconsider im =
im as
even Element of
NAT ;
im > 0
by A96;
then
di + 0 < di + im
by XREAL_1:8;
then
(
P1 .first() = P1 . di &
P1 .last() = P1 . di )
by A66, A82, A95, A97, GLIB_001:def 28;
hence
contradiction
by A35, GLIB_001:def 24;
:: thesis: verum
end; hence
P1 . (di + 2) = P2 . ei
by A22, A25, A67, A80, A84, A95, GLIB_001:37;
:: thesis: verum end;
end;
P2 . (di + 2) = P2 . ei
proof
per cases
( ( v1 = P2 . ei & v2 = P1 . di ) or ( v1 = P1 . di & v2 = P2 . ei ) )
by A70, A79;
suppose A98:
(
v1 = P2 . ei &
v2 = P1 . di )
;
:: thesis: P2 . (di + 2) = P2 . ei
di <= di + n
by NAT_1:11;
then A99:
di < (di + n) + 1
by NAT_1:13;
di + (n + 2) <= (len (P2 .cut di,ei)) + di
by A61, XREAL_1:8;
then
((di + n) + 1) + 1
<= ei + 1
by A20, GLIB_001:37;
then
(di + n) + 1
<= ei
by XREAL_1:8;
then
di + (n + 1) <= len P2
by A20, XXREAL_0:2;
then
(
P2 .first() = P1 . di &
P2 .last() = P1 . di )
by A30, A63, A91, A98, A99, GLIB_001:def 28;
hence
P2 . (di + 2) = P2 . ei
by A36, GLIB_001:def 24;
:: thesis: verum end; suppose A100:
(
v1 = P1 . di &
v2 = P2 . ei )
;
:: thesis: P2 . (di + 2) = P2 . ei
ni = 0
proof
assume A101:
ni <> 0
;
:: thesis: contradiction
di + ni < (len (P2 .cut di,ei)) + di
by A87, XREAL_1:8;
then
di + ni < ei + 1
by A20, GLIB_001:37;
then
di + ni <= ei
by NAT_1:13;
then A102:
di + ni <= len P2
by A20, XXREAL_0:2;
n - 1
= ni
by A86;
then reconsider ni =
ni as
even Element of
NAT ;
ni > 0
by A101;
then
di + 0 < di + ni
by XREAL_1:8;
then
(
P2 .first() = P1 . di &
P2 .last() = P1 . di )
by A30, A62, A88, A100, A102, GLIB_001:def 28;
hence
contradiction
by A36, GLIB_001:def 24;
:: thesis: verum
end; hence
P2 . (di + 2) = P2 . ei
by A20, A63, A86, A90, A100, GLIB_001:37;
:: thesis: verum end;
end; hence
contradiction
by A3, A4, A6, A12, A92, Th23;
:: thesis: verum end;
end;
then
(P2 .cut di,ei) .append ((P1 .cut di,(P1 .find (P2 . ei))) .reverse() ) is Cycle-like
by A29, A31, A32, A34, A37, A38, A41, Th19;
hence
contradiction
; :: thesis: verum