let G be _Graph; :: thesis: for W being Walk of G holds

( W is Trail-like iff W .reverse() is Trail-like )

let W be Walk of G; :: thesis: ( W is Trail-like iff W .reverse() is Trail-like )

assume W .reverse() is Trail-like ; :: thesis: W is Trail-like

then (W .reverse()) .reverse() is Trail-like by A1;

hence W is Trail-like ; :: thesis: verum

( W is Trail-like iff W .reverse() is Trail-like )

let W be Walk of G; :: thesis: ( W is Trail-like iff W .reverse() is Trail-like )

A1: now :: thesis: for W being Walk of G st W is Trail-like holds

W .reverse() is Trail-like

hence
( W is Trail-like implies W .reverse() is Trail-like )
; :: thesis: ( W .reverse() is Trail-like implies W is Trail-like )W .reverse() is Trail-like

let W be Walk of G; :: thesis: ( W is Trail-like implies W .reverse() is Trail-like )

assume A2: W is Trail-like ; :: thesis: W .reverse() is Trail-like

end;assume A2: W is Trail-like ; :: thesis: W .reverse() is Trail-like

now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len (W .reverse()) holds

(W .reverse()) . m <> (W .reverse()) . n

hence
W .reverse() is Trail-like
by Lm57; :: thesis: verum(W .reverse()) . m <> (W .reverse()) . n

reconsider lenW = len W as odd Element of NAT ;

let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len (W .reverse()) implies (W .reverse()) . m <> (W .reverse()) . n )

assume that

A3: 1 <= m and

A4: m < n and

A5: n <= len (W .reverse()) ; :: thesis: (W .reverse()) . m <> (W .reverse()) . n

(len W) - n < (len W) - m by A4, XREAL_1:15;

then A6: ((len W) - n) + 1 < ((len W) - m) + 1 by XREAL_1:8;

m <= len (W .reverse()) by A4, A5, XXREAL_0:2;

then A7: m in dom (W .reverse()) by A3, FINSEQ_3:25;

then A8: ((len W) - m) + 1 in dom W by Lm8;

then reconsider rm = (lenW - m) + 1 as even Element of NAT ;

A9: rm <= len W by A8, FINSEQ_3:25;

1 <= n by A3, A4, XXREAL_0:2;

then A10: n in dom (W .reverse()) by A5, FINSEQ_3:25;

then A11: (W .reverse()) . n = W . (((len W) - n) + 1) by Lm8;

A12: ((len W) - n) + 1 in dom W by A10, Lm8;

then reconsider rn = (lenW - n) + 1 as even Element of NAT ;

A13: 1 <= rn by A12, FINSEQ_3:25;

(W .reverse()) . m = W . (((len W) - m) + 1) by A7, Lm8;

hence (W .reverse()) . m <> (W .reverse()) . n by A2, A11, A6, A13, A9, Lm57; :: thesis: verum

end;let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len (W .reverse()) implies (W .reverse()) . m <> (W .reverse()) . n )

assume that

A3: 1 <= m and

A4: m < n and

A5: n <= len (W .reverse()) ; :: thesis: (W .reverse()) . m <> (W .reverse()) . n

(len W) - n < (len W) - m by A4, XREAL_1:15;

then A6: ((len W) - n) + 1 < ((len W) - m) + 1 by XREAL_1:8;

m <= len (W .reverse()) by A4, A5, XXREAL_0:2;

then A7: m in dom (W .reverse()) by A3, FINSEQ_3:25;

then A8: ((len W) - m) + 1 in dom W by Lm8;

then reconsider rm = (lenW - m) + 1 as even Element of NAT ;

A9: rm <= len W by A8, FINSEQ_3:25;

1 <= n by A3, A4, XXREAL_0:2;

then A10: n in dom (W .reverse()) by A5, FINSEQ_3:25;

then A11: (W .reverse()) . n = W . (((len W) - n) + 1) by Lm8;

A12: ((len W) - n) + 1 in dom W by A10, Lm8;

then reconsider rn = (lenW - n) + 1 as even Element of NAT ;

A13: 1 <= rn by A12, FINSEQ_3:25;

(W .reverse()) . m = W . (((len W) - m) + 1) by A7, Lm8;

hence (W .reverse()) . m <> (W .reverse()) . n by A2, A11, A6, A13, A9, Lm57; :: thesis: verum

assume W .reverse() is Trail-like ; :: thesis: W is Trail-like

then (W .reverse()) .reverse() is Trail-like by A1;

hence W is Trail-like ; :: thesis: verum