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 )
A1:
now 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 now 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 A3:
( 1
<= m &
m < n &
n <= len (W .reverse() ) )
;
:: thesis: (W .reverse() ) . m <> (W .reverse() ) . nthen
m <= len (W .reverse() )
by XXREAL_0:2;
then
m in dom (W .reverse() )
by A3, FINSEQ_3:27;
then A4:
(
(W .reverse() ) . m = W . (((len W) - m) + 1) &
((len W) - m) + 1
in dom W )
by Lm8;
1
<= n
by A3, XXREAL_0:2;
then
n in dom (W .reverse() )
by A3, FINSEQ_3:27;
then A5:
(
(W .reverse() ) . n = W . (((len W) - n) + 1) &
((len W) - n) + 1
in dom W )
by Lm8;
reconsider lenW =
len W as
odd Element of
NAT ;
reconsider rn =
(lenW - n) + 1 as
even Element of
NAT by A5;
reconsider rm =
(lenW - m) + 1 as
even Element of
NAT by A4;
(len W) - n < (len W) - m
by A3, XREAL_1:17;
then A6:
((len W) - n) + 1
< ((len W) - m) + 1
by XREAL_1:10;
( 1
<= rn &
rm <= len W )
by A4, A5, FINSEQ_3:27;
hence
(W .reverse() ) . m <> (W .reverse() ) . n
by A2, A4, A5, A6, Lm57;
:: thesis: verum end; hence
W .reverse() is
Trail-like
by Lm57;
:: thesis: verum end;
hence
( W is Trail-like implies W .reverse() is Trail-like )
; :: thesis: ( W .reverse() is Trail-like implies W 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
by FINSEQ_6:29; :: thesis: verum