let G be _Graph; :: thesis: for W being Walk of G st ( for n being odd Element of NAT st n <= len W holds
W .find (W . n) = W .rfind (W . n) ) holds
W is Path-like
let W be Walk of G; :: thesis: ( ( for n being odd Element of NAT st n <= len W holds
W .find (W . n) = W .rfind (W . n) ) implies W is Path-like )
assume A1: for n being odd Element of NAT st n <= len W holds
W .find (W . n) = W .rfind (W . n) ; :: thesis: W is Path-like
A2: now :: thesis: for x being odd Element of NAT st x <= len W holds
( W .find (W . x) = x & W .rfind (W . x) = x )
let x be odd Element of NAT ; :: thesis: ( x <= len W implies ( W .find (W . x) = x & W .rfind (W . x) = x ) )
assume A3: x <= len W ; :: thesis: ( W .find (W . x) = x & W .rfind (W . x) = x )
then A4: W .rfind (W . x) >= x by Th113;
A5: W .find (W . x) = W .rfind (W . x) by A1, A3;
W .find (W . x) <= x by A3, Th113;
hence ( W .find (W . x) = x & W .rfind (W . x) = x ) by A4, A5, XXREAL_0:1; :: thesis: verum
end;
now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . n
let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len W implies W . m <> W . n )
assume that
A6: 1 <= m and
A7: m < n and
A8: n <= len W ; :: thesis: W . m <> W . n
1 <= n by A6, A7, XXREAL_0:2;
then n in dom W by A8, FINSEQ_3:25;
then consider naa1 being odd Element of NAT such that
A9: naa1 = n - 1 and
A10: n - 1 in dom W and
A11: n + 1 in dom W and
A12: W . n Joins W . naa1,W . (n + 1),G by Lm2;
m <= len W by A7, A8, XXREAL_0:2;
then m in dom W by A6, FINSEQ_3:25;
then consider maa1 being odd Element of NAT such that
A13: maa1 = m - 1 and
A14: m - 1 in dom W and
m + 1 in dom W and
A15: W . m Joins W . maa1,W . (m + 1),G by Lm2;
now :: thesis: not W . m = W . n
set Wnaa1 = W . naa1;
set Wn1 = W . (n + 1);
set Wmaa1 = W . maa1;
set Wm1 = W . (m + 1);
assume A16: W . m = W . n ; :: thesis: contradiction
maa1 <= len W by A13, A14, FINSEQ_3:25;
then A17: W .find (W . maa1) = maa1 by A2;
A18: n + 1 <= len W by A11, FINSEQ_3:25;
A19: naa1 <= len W by A9, A10, FINSEQ_3:25;
now :: thesis: contradiction
per cases ( ( W . maa1 = W . naa1 & W . (m + 1) = W . (n + 1) ) or ( W . maa1 = W . (n + 1) & W . (m + 1) = W . naa1 ) ) by A15, A12, A16, GLIB_000:15;
suppose ( W . maa1 = W . naa1 & W . (m + 1) = W . (n + 1) ) ; :: thesis: contradiction
then maa1 = naa1 by A2, A19, A17;
hence contradiction by A7, A13, A9; :: thesis: verum
end;
suppose ( W . maa1 = W . (n + 1) & W . (m + 1) = W . naa1 ) ; :: thesis: contradiction
then maa1 = n + 1 by A2, A18, A17;
then n <= (maa1 - 1) + 1 by NAT_1:12;
then n <= (m - 1) + 1 by A13, NAT_1:12;
hence contradiction by A7; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence W . m <> W . n ; :: thesis: verum
end;
then A20: W is Trail-like by Lm57;
now :: thesis: for m, n being odd Element of NAT st m < n & n <= len W & W . m = W . n holds
( m = 1 & n = len W )
let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len W & W . m = W . n implies ( m = 1 & n = len W ) )
assume that
A21: m < n and
A22: n <= len W and
A23: W . m = W . n ; :: thesis: ( m = 1 & n = len W )
m <= len W by A21, A22, XXREAL_0:2;
then W .find (W . m) = m by A2;
hence ( m = 1 & n = len W ) by A2, A21, A22, A23; :: thesis: verum
end;
hence W is Path-like by A20; :: thesis: verum