let G be _Graph; :: thesis: for W being Walk of G holds
( W is Path-like iff W .reverse() is Path-like )
let W be Walk of G; :: thesis: ( W is Path-like iff W .reverse() is Path-like )
A1:
now let W be
Walk of
G;
:: thesis: ( W is Path-like implies W .reverse() is Path-like )assume A2:
W is
Path-like
;
:: thesis: W .reverse() is Path-likethen
(
W is
Trail-like & ( for
m,
n being
odd Element of
NAT st
m < n &
n <= len W &
W . m = W . n holds
(
m = 1 &
n = len W ) ) )
by Def28;
then A3:
W .reverse() is
Trail-like
by Lm58;
reconsider lenW =
len W as
odd Element of
NAT ;
now let m,
n be
odd Element of
NAT ;
:: thesis: ( m < n & n <= len (W .reverse() ) & (W .reverse() ) . m = (W .reverse() ) . n implies ( m = 1 & n = len (W .reverse() ) ) )assume A4:
(
m < n &
n <= len (W .reverse() ) &
(W .reverse() ) . m = (W .reverse() ) . n )
;
:: thesis: ( m = 1 & n = len (W .reverse() ) )then A5:
m <= len (W .reverse() )
by XXREAL_0:2;
1
<= m
by HEYTING3:1;
then A6:
m in dom (W .reverse() )
by A5, FINSEQ_3:27;
then A7:
(
(W .reverse() ) . m = W . (((len W) - m) + 1) &
((len W) - m) + 1
in dom W )
by Lm8;
then reconsider rm =
(lenW - m) + 1 as
odd Element of
NAT ;
1
<= n
by HEYTING3:1;
then
n in dom (W .reverse() )
by A4, FINSEQ_3:27;
then A8:
(
(W .reverse() ) . n = W . (((len W) - n) + 1) &
((len W) - n) + 1
in dom W )
by Lm8;
then reconsider rn =
(lenW - n) + 1 as
odd Element of
NAT ;
lenW - n < (len W) - m
by A4, XREAL_1:17;
then A9:
rn < rm
by XREAL_1:10;
A10:
rm <= len W
by A7, FINSEQ_3:27;
A11:
W . rm = W . rn
by A4, A6, A8, Lm8;
then A12:
(
rn = 1 &
rm = len W )
by A2, A9, A10, Def28;
(len W) + (1 + (- m)) = len W
by A2, A9, A10, A11, Def28;
hence
m = 1
;
:: thesis: n = len (W .reverse() )thus
n = len (W .reverse() )
by A12, FINSEQ_5:def 3;
:: thesis: verum end; hence
W .reverse() is
Path-like
by A3, Def28;
:: thesis: verum end;
hence
( W is Path-like implies W .reverse() is Path-like )
; :: thesis: ( W .reverse() is Path-like implies W is Path-like )
assume
W .reverse() is Path-like
; :: thesis: W is Path-like
then
(W .reverse() ) .reverse() is Path-like
by A1;
hence
W is Path-like
by FINSEQ_6:29; :: thesis: verum