let W be Walk of T; :: thesis: ( W is Trail-like implies W is Path-like )

assume A1: W is Trail-like ; :: thesis: W is Path-like

defpred S_{1}[ Nat] means ( T is odd & T <= len W & ex k being odd Element of NAT st

( k < T & W . k = W . T ) );

assume not W is Path-like ; :: thesis: contradiction

then ex m, n being odd Element of NAT st

( m < n & n <= len W & W . m = W . n & ( m <> 1 or n <> len W ) ) by A1;

then A2: ex p being Nat st S_{1}[p]
;

consider p being Nat such that

A3: S_{1}[p]
and

A4: for r being Nat st S_{1}[r] holds

p <= r from NAT_1:sch 5(A2);

reconsider P = p as Element of NAT by ORDINAL1:def 12;

consider k being odd Element of NAT such that

A5: k < p and

p <= len W and

A6: W . k = W . p by A3;

set Wc = W .cut (k,P);

(len (W .cut (k,P))) + k = P + 1 by A3, A5, GLIB_001:36;

then len (W .cut (k,P)) <> 1 by A5;

then A7: W .cut (k,P) is V5() by GLIB_001:126;

A8: (W .cut (k,P)) .last() = W . p by A3, A5, GLIB_001:37;

A9: W .cut (k,P) is Path-like

then W .cut (k,P) is closed by A6, A8;

then W .cut (k,P) is Cycle-like by A7, A9;

hence contradiction by GLIB_002:def 2; :: thesis: verum

assume A1: W is Trail-like ; :: thesis: W is Path-like

defpred S

( k < T & W . k = W . T ) );

assume not W is Path-like ; :: thesis: contradiction

then ex m, n being odd Element of NAT st

( m < n & n <= len W & W . m = W . n & ( m <> 1 or n <> len W ) ) by A1;

then A2: ex p being Nat st S

consider p being Nat such that

A3: S

A4: for r being Nat st S

p <= r from NAT_1:sch 5(A2);

reconsider P = p as Element of NAT by ORDINAL1:def 12;

consider k being odd Element of NAT such that

A5: k < p and

p <= len W and

A6: W . k = W . p by A3;

set Wc = W .cut (k,P);

(len (W .cut (k,P))) + k = P + 1 by A3, A5, GLIB_001:36;

then len (W .cut (k,P)) <> 1 by A5;

then A7: W .cut (k,P) is V5() by GLIB_001:126;

A8: (W .cut (k,P)) .last() = W . p by A3, A5, GLIB_001:37;

A9: W .cut (k,P) is Path-like

proof

(W .cut (k,P)) .first() = W . k
by A3, A5, GLIB_001:37;
assume
not W .cut (k,P) is Path-like
; :: thesis: contradiction

then consider m, n being odd Element of NAT such that

A10: m < n and

A11: n <= len (W .cut (k,P)) and

A12: (W .cut (k,P)) . m = (W .cut (k,P)) . n and

A13: ( m <> 1 or n <> len (W .cut (k,P)) ) by A1;

A14: m < len (W .cut (k,P)) by A10, A11, XXREAL_0:2;

consider kn1 being odd Nat such that

A15: (W .cut (k,P)) . n = W . kn1 and

A16: kn1 = (k + n) - 1 and

A17: kn1 <= len W by A3, A5, A11, Th12;

reconsider kn1 = kn1 as odd Element of NAT by ORDINAL1:def 12;

A18: 1 <= m by ABIAN:12;

m <= len (W .cut (k,P)) by A10, A11, XXREAL_0:2;

then consider km1 being odd Nat such that

A19: (W .cut (k,P)) . m = W . km1 and

A20: km1 = (k + m) - 1 and

A21: km1 <= len W by A3, A5, Th12;

reconsider km1 = km1 as odd Element of NAT by ORDINAL1:def 12;

end;then consider m, n being odd Element of NAT such that

A10: m < n and

A11: n <= len (W .cut (k,P)) and

A12: (W .cut (k,P)) . m = (W .cut (k,P)) . n and

A13: ( m <> 1 or n <> len (W .cut (k,P)) ) by A1;

A14: m < len (W .cut (k,P)) by A10, A11, XXREAL_0:2;

consider kn1 being odd Nat such that

A15: (W .cut (k,P)) . n = W . kn1 and

A16: kn1 = (k + n) - 1 and

A17: kn1 <= len W by A3, A5, A11, Th12;

reconsider kn1 = kn1 as odd Element of NAT by ORDINAL1:def 12;

A18: 1 <= m by ABIAN:12;

m <= len (W .cut (k,P)) by A10, A11, XXREAL_0:2;

then consider km1 being odd Nat such that

A19: (W .cut (k,P)) . m = W . km1 and

A20: km1 = (k + m) - 1 and

A21: km1 <= len W by A3, A5, Th12;

reconsider km1 = km1 as odd Element of NAT by ORDINAL1:def 12;

per cases
( n < len (W .cut (k,P)) or n = len (W .cut (k,P)) )
by A11, XXREAL_0:1;

end;

suppose
n < len (W .cut (k,P))
; :: thesis: contradiction

then
k + n < k + (len (W .cut (k,P)))
by XREAL_1:6;

then k + n < p + 1 by A3, A5, GLIB_001:36;

then A22: kn1 < p by A16, XREAL_1:19;

k + m < k + n by A10, XREAL_1:6;

then km1 < kn1 by A20, A16, XREAL_1:9;

hence contradiction by A4, A12, A19, A15, A17, A22; :: thesis: verum

end;then k + n < p + 1 by A3, A5, GLIB_001:36;

then A22: kn1 < p by A16, XREAL_1:19;

k + m < k + n by A10, XREAL_1:6;

then km1 < kn1 by A20, A16, XREAL_1:9;

hence contradiction by A4, A12, A19, A15, A17, A22; :: thesis: verum

suppose A23:
n = len (W .cut (k,P))
; :: thesis: contradiction

k + m < (len (W .cut (k,P))) + k
by A14, XREAL_1:6;

then k + m < p + 1 by A3, A5, GLIB_001:36;

then A24: km1 < p by A20, XREAL_1:19;

1 < m by A13, A18, A23, XXREAL_0:1;

then k + 1 < k + m by XREAL_1:6;

then k < km1 by A20, XREAL_1:20;

hence contradiction by A4, A6, A8, A12, A19, A21, A23, A24; :: thesis: verum

end;then k + m < p + 1 by A3, A5, GLIB_001:36;

then A24: km1 < p by A20, XREAL_1:19;

1 < m by A13, A18, A23, XXREAL_0:1;

then k + 1 < k + m by XREAL_1:6;

then k < km1 by A20, XREAL_1:20;

hence contradiction by A4, A6, A8, A12, A19, A21, A23, A24; :: thesis: verum

then W .cut (k,P) is closed by A6, A8;

then W .cut (k,P) is Cycle-like by A7, A9;

hence contradiction by GLIB_002:def 2; :: thesis: verum