let G be _Graph; :: thesis: for W1 being Walk of G
for e, x, y being set st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )
let W1 be Walk of G; :: thesis: for e, x, y being set st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )
let e, x, y be set ; :: thesis: ( e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like implies ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() ) )
assume A1:
( e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like )
; :: thesis: ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )
then consider v1, v2 being Vertex of G, n being odd Element of NAT such that
A2:
( n + 2 <= len W1 & v1 = W1 . n & e = W1 . (n + 1) & v2 = W1 . (n + 2) & e Joins v1,v2,G )
by Lm47;
set WA = W1 .cut (n + 2),(len W1);
set WB = W1 .cut ((2 * 0 ) + 1),n;
A3:
W1 .cut (n + 2),(len W1) is_Walk_from v2,W1 . (len W1)
by A2, Lm16;
A4:
1 <= n
by HEYTING3:1;
A5:
(n + 2) - 2 < (len W1) - 0
by A2, XREAL_1:17;
then A6:
W1 .cut ((2 * 0 ) + 1),n is_Walk_from W1 .first() ,v1
by A2, A4, Lm16;
W1 is closed
by A1;
then A7:
W1 .cut ((2 * 0 ) + 1),n is_Walk_from W1 .last() ,v1
by A6, Def24;
then A8:
(W1 .cut (n + 2),(len W1)) .append (W1 .cut ((2 * 0 ) + 1),n) is_Walk_from v2,v1
by A3, Th32;
A9:
( (W1 .cut (n + 2),(len W1)) .last() = W1 .last() & (W1 .cut ((2 * 0 ) + 1),n) .first() = W1 .last() )
by A2, A7, Def23, Lm16;
W1 is Path-like
by A1;
then A10:
W1 is Trail-like
;
A11:
now assume
e in (W1 .cut (n + 2),(len W1)) .edges()
;
:: thesis: contradictionthen consider m being
even Element of
NAT such that A12:
( 1
<= m &
m <= len (W1 .cut (n + 2),(len W1)) &
(W1 .cut (n + 2),(len W1)) . m = e )
by Lm46;
reconsider maa1 =
m - 1 as
odd Element of
NAT by A12, INT_1:18;
A13:
maa1 + 1
= m
;
maa1 < (len (W1 .cut (n + 2),(len W1))) - 0
by A12, XREAL_1:17;
then A14:
(
e = W1 . ((n + 2) + maa1) &
(n + 2) + maa1 in dom W1 )
by A2, A12, A13, Lm15;
then A15:
(n + 2) + maa1 <= len W1
by FINSEQ_3:27;
n + 1
< (n + 1) + 1
by NAT_1:13;
then A16:
(n + 1) + 0 < (n + 2) + maa1
by XREAL_1:10;
1
<= n + 1
by NAT_1:12;
hence
contradiction
by A2, A10, A14, A15, A16, Lm57;
:: thesis: verum end;
A17:
now assume
e in (W1 .cut ((2 * 0 ) + 1),n) .edges()
;
:: thesis: contradictionthen consider m being
even Element of
NAT such that A18:
( 1
<= m &
m <= len (W1 .cut ((2 * 0 ) + 1),n) &
(W1 .cut ((2 * 0 ) + 1),n) . m = e )
by Lm46;
m in dom (W1 .cut ((2 * 0 ) + 1),n)
by A18, FINSEQ_3:27;
then A19:
W1 . m = W1 . (n + 1)
by A2, A5, A18, Lm23;
len (W1 .cut ((2 * 0 ) + 1),n) = n
by A5, Lm22;
then A20:
m + 0 < n + 1
by A18, XREAL_1:10;
n + 1
<= len W1
by A5, NAT_1:13;
hence
contradiction
by A10, A18, A19, A20, Lm57;
:: thesis: verum end;
((W1 .cut (n + 2),(len W1)) .append (W1 .cut ((2 * 0 ) + 1),n)) .edges() = ((W1 .cut (n + 2),(len W1)) .edges() ) \/ ((W1 .cut ((2 * 0 ) + 1),n) .edges() )
by A9, Th103;
then A21:
not e in ((W1 .cut (n + 2),(len W1)) .append (W1 .cut ((2 * 0 ) + 1),n)) .edges()
by A11, A17, XBOOLE_0:def 3;
then A22:
not e in (((W1 .cut (n + 2),(len W1)) .append (W1 .cut ((2 * 0 ) + 1),n)) .reverse() ) .edges()
by Th108;
A23:
((W1 .cut (n + 2),(len W1)) .append (W1 .cut ((2 * 0 ) + 1),n)) .reverse() is_Walk_from v1,v2
by A8, Th24;
hence
ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )
; :: thesis: verum