let T be _Tree; :: thesis:
let a, b be Vertex of T; :: thesis:
let P1, P2 be Path of T; :: thesis:
assume that
A1: P1 is_Walk_from a,b and
A2: P2 is_Walk_from a,b ; :: thesis:
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 S₁[ Nat] means ( $1 is odd & di < $1 & $1 <= len P2 & P2 . $1 in P1 .vertices() );
assume A4: P1 <> P2 ; :: thesis:
A5: not P2 c= P1

proof

assume A6: P2 c= P1 ; :: thesis:
then len P2 <= len P1 by FINSEQ_1:63;
then A7: len P2 < len P1 by A4, A6, FINSEQ_2:129, XXREAL_0:1;
1 <= len P2 by ABIAN:12;
then len P2 in dom P2 by FINSEQ_3:25;
then A8: P2 . (len P2) = P1 . (len P2) by A6, GRFUNC_1:2;
A9: P1 . (len P1) = P1 .last()
.= b by A1 ;
P2 . (len P2) = P2 .last()
.= b by A2 ;
hence contradiction by A7, A8, A9, Th26; :: thesis:

end;

A10: ex k being Nat st S₁[k]

proof

take k = len P2; :: thesis:
thus k is odd ; :: thesis:
( di + 2 <= len P2 & di < di + 2 ) by A3, A5, Th23, NAT_1:19;
hence di < k by XXREAL_0:2; :: thesis:
thus k <= len P2 ; :: thesis:
P2 . k = P2 .last()
.= b by A2
.= P1 .last() by A1 ;
hence P2 . k in P1 .vertices() by GLIB_001:88; :: thesis:

end;

consider ei being Nat such that
A11: S₁[ei] and
A12: for n being Nat st S₁[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

proof

assume len P2 = 1 ; :: thesis:
then di < 1 by A11, XXREAL_0:2;
hence contradiction by ABIAN:12; :: thesis:

end;

then A18: P2 is V5() by GLIB_001:126;
A19: di < P1 .find (P2 . ei)

proof

assume di >= P1 .find (P2 . ei) ; :: thesis:
then ( P1 . (P1 .find (P2 . ei)) = P2 . (P1 .find (P2 . ei)) & ei > P1 .find (P2 . ei) ) by A11, Th7, XXREAL_0:2;
then ( P2 .first() = P2 . ei & P2 .last() = P2 . ei ) by A11, A17, GLIB_001:def 28;
hence contradiction by A18, GLIB_001:def 24; :: thesis:

end;

then A20: P1 .cut (di,(P1 .find (P2 . ei))) is V5() by A13, GLIB_001:131;
then A21: P1 is V5() ;
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)} ; :: thesis:
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

proof

A33: (len (P2 .cut (di,ei))) + di = ei + 1 by A11, GLIB_001:36;
assume A34: gi >= ei ; :: thesis:

per cases by A34, XXREAL_0:1;

suppose gi = ei ; :: thesis:

then (P2 .cut (di,ei)) . gii = (P2 .cut (di,ei)) .last() by A29, A33
.= P2 . ei by A11, GLIB_001:37 ;
hence contradiction by A25, A27, TARSKI:def 2; :: thesis:

end;

suppose gi > ei ; :: thesis:

then gi + 1 > ei + 1 by XREAL_1:6;
hence contradiction by A26, A29, A33, XREAL_1:6; :: thesis:

end;

gii <> 1 by A16, A25, A27, TARSKI:def 2;
then A35: gii > 1 by A31, XXREAL_0:1;
A36: di < gi

proof

assume di >= gi ; :: thesis:
then di + gii > gi + 1 by A35, XREAL_1:8;
hence contradiction by A29; :: thesis:

end;

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; :: thesis:

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())

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A40: x in {(P2 . ei),(P1 . di)} ; :: thesis:

per cases by A40, TARSKI:def 2;

suppose x = P2 . ei ; :: thesis:

then ( x in (P2 .cut (di,ei)) .vertices() & x in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() ) by A37, A39, GLIB_001:88;
hence x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) by XBOOLE_0:def 4; :: thesis:

end;

suppose x = P1 . di ; :: thesis:

then ( x in (P2 .cut (di,ei)) .vertices() & x in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() ) by A16, A38, GLIB_001:88;
hence x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) by XBOOLE_0:def 4; :: thesis:

end;

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 V5() by A11, GLIB_001:131;
then A43: P2 is V5() ;
A44: not P1 c= P2

proof

assume A45: P1 c= P2 ; :: thesis:
then len P1 <= len P2 by FINSEQ_1:63;
then A46: len P1 < len P2 by A4, A45, FINSEQ_2:129, XXREAL_0:1;
1 <= len P1 by ABIAN:12;
then len P1 in dom P1 by FINSEQ_3:25;
then A47: P1 . (len P1) = P2 . (len P1) by A45, GRFUNC_1:2;
A48: P2 . (len P2) = P2 .last()
.= b by A2 ;
P1 . (len P1) = P1 .last()
.= b by A1 ;
hence contradiction by A46, A47, A48, Th26; :: thesis:

end;

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()) <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
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 ;

suppose A62: v1 <> v2 ; :: thesis:

A63: 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 by A41, A62, A75, A74, A69, A76, XBOOLE_1:19, ZFMISC_1:22;

suppose A80: ( v1 = P2 . ei & v2 = P1 . di ) ; :: thesis:

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; :: thesis:

end;

suppose A82: ( v1 = P1 . di & v2 = P2 . ei ) ; :: thesis:

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 ; :: thesis:
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; :: thesis:

end;

hence P2 . (di + 2) = P2 . ei by A11, A59, A66, A64, A82, GLIB_001:36; :: thesis:

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 by A60, A56, A62, A76, A86, GLIB_000:15;

suppose A89: ( u1 = P2 . ei & u2 = P1 . di ) ; :: thesis:

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; :: thesis:

end;

suppose A91: ( u1 = P1 . di & u2 = P2 . ei ) ; :: thesis:

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 ; :: thesis:
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; :: thesis:

end;

hence P1 . (di + 2) = P2 . ei by A13, A19, A55, A85, A71, A91, GLIB_001:36; :: thesis:

end;

hence contradiction by A3, A44, A5, A79, Th24; :: thesis:

end;

suppose v1 = v2 ; :: thesis:

then ( (P2 .cut (di,ei)) .first() = v1 & (P2 .cut (di,ei)) .last() = v1 ) by A57, A58, A59, A61, GLIB_001:def 28;
hence contradiction by A42, GLIB_001:def 24; :: thesis:

end;

(P1 .cut (di,(P1 .find (P2 . ei)))) .reverse() is V5() 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 ; :: thesis: