let G be _Graph; 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; 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 ; ( 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 that
A1:
e Joins x,y,G
and
A2:
e in W1 .edges()
and
A3:
W1 is Cycle-like
; ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )
consider v1, v2 being Vertex of G, n being odd Element of NAT such that
A4:
n + 2 <= len W1
and
A5:
v1 = W1 . n
and
A6:
e = W1 . (n + 1)
and
A7:
v2 = W1 . (n + 2)
and
A8:
e Joins v1,v2,G
by A2, Lm47;
set WA = W1 .cut ((n + 2),(len W1));
set WB = W1 .cut (((2 * 0) + 1),n);
A9:
(W1 .cut ((n + 2),(len W1))) .last() = W1 .last()
by A4, Lm16;
A10:
(n + 2) - 2 < (len W1) - 0
by A4, XREAL_1:15;
A11:
now not e in (W1 .cut (((2 * 0) + 1),n)) .edges() assume
e in (W1 .cut (((2 * 0) + 1),n)) .edges()
;
contradictionthen consider m being
even Element of
NAT such that A12:
1
<= m
and A13:
m <= len (W1 .cut (((2 * 0) + 1),n))
and A14:
(W1 .cut (((2 * 0) + 1),n)) . m = e
by Lm46;
m in dom (W1 .cut (((2 * 0) + 1),n))
by A12, A13, FINSEQ_3:25;
then A15:
W1 . m = W1 . (n + 1)
by A6, A10, A14, Lm23;
len (W1 .cut (((2 * 0) + 1),n)) = n
by A10, Lm22;
then A16:
m + 0 < n + 1
by A13, XREAL_1:8;
n + 1
<= len W1
by A10, NAT_1:13;
hence
contradiction
by A3, A12, A15, A16, Lm57;
verum end;
1 <= n
by ABIAN:12;
then
W1 .cut (((2 * 0) + 1),n) is_Walk_from W1 .first() ,v1
by A5, A10, Lm16;
then A17:
W1 .cut (((2 * 0) + 1),n) is_Walk_from W1 .last() ,v1
by A3, Def24;
A18:
W1 .cut ((n + 2),(len W1)) is_Walk_from v2,W1 . (len W1)
by A4, A7, Lm16;
then
(W1 .cut ((n + 2),(len W1))) .append (W1 .cut (((2 * 0) + 1),n)) is_Walk_from v2,v1
by A17, Th29;
then A19:
((W1 .cut ((n + 2),(len W1))) .append (W1 .cut (((2 * 0) + 1),n))) .reverse() is_Walk_from v1,v2
by Th22;
A20:
now not e in (W1 .cut ((n + 2),(len W1))) .edges() assume
e in (W1 .cut ((n + 2),(len W1))) .edges()
;
contradictionthen consider m being
even Element of
NAT such that A21:
1
<= m
and A22:
m <= len (W1 .cut ((n + 2),(len W1)))
and A23:
(W1 .cut ((n + 2),(len W1))) . m = e
by Lm46;
reconsider maa1 =
m - 1 as
odd Element of
NAT by A21, INT_1:5;
A24:
maa1 < (len (W1 .cut ((n + 2),(len W1)))) - 0
by A22, XREAL_1:15;
then
(n + 2) + maa1 in dom W1
by A4, Lm15;
then A25:
(n + 2) + maa1 <= len W1
by FINSEQ_3:25;
maa1 + 1
= m
;
then A26:
e = W1 . ((n + 2) + maa1)
by A4, A23, A24, Lm15;
n + 1
< (n + 1) + 1
by NAT_1:13;
then A27:
(n + 1) + 0 < (n + 2) + maa1
by XREAL_1:8;
1
<= n + 1
by NAT_1:12;
hence
contradiction
by A3, A6, A26, A25, A27, Lm57;
verum end;
(W1 .cut (((2 * 0) + 1),n)) .first() = W1 .last()
by A17;
then
((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, Th100;
then A28:
not e in ((W1 .cut ((n + 2),(len W1))) .append (W1 .cut (((2 * 0) + 1),n))) .edges()
by A20, A11, XBOOLE_0:def 3;
then A29:
not e in (((W1 .cut ((n + 2),(len W1))) .append (W1 .cut (((2 * 0) + 1),n))) .reverse()) .edges()
by Th105;
hence
ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )
; verum