let G1 be connected _Graph; :: thesis: for W being Walk of G1
for e being set
for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
let W be Walk of G1; :: thesis: for e being set
for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
let e be set ; :: thesis: for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds
G2 is connected
let G2 be removeEdge of G1,e; :: thesis: ( W is Cycle-like & e in W .edges() implies G2 is connected )
assume A1:
( W is Cycle-like & e in W .edges() )
; :: thesis: G2 is connected
then reconsider v1 = (the_Source_of G1) . e, v2 = (the_Target_of G1) . e as Vertex of G1 by FUNCT_2:7;
e Joins v1,v2,G1
by A1, GLIB_000:def 15;
then consider X being Walk of G1 such that
A2:
( X is_Walk_from v1,v2 & not e in X .edges() )
by A1, GLIB_001:158;
reconsider X2 = X as Walk of G2 by A2, GLIB_001:173;
A3:
X2 is_Walk_from v1,v2
by A2, GLIB_001:20;
then A4:
X2 .reverse() is_Walk_from v2,v1
by GLIB_001:24;
now let u,
v be
Vertex of
G2;
:: thesis: ex W being Walk of G2 st W is_Walk_from u,v
the_Vertices_of G2 c= the_Vertices_of G1
;
then reconsider u' =
u,
v' =
v as
Vertex of
G1 by TARSKI:def 3;
consider C being
Walk of
G1 such that A5:
C is_Walk_from u',
v'
by Def1;
consider P being
Path of
C;
A6:
P is_Walk_from u',
v'
by A5, GLIB_001:161;
then A7:
(
P . 1
= u &
P . (len P) = v )
by GLIB_001:18;
now per cases
( e in P .edges() or not e in P .edges() )
;
suppose
e in P .edges()
;
:: thesis: ex W being Walk of G2 st W is_Walk_from u,vthen consider a,
b being
Vertex of
G1,
m being
odd Element of
NAT such that A8:
(
m + 2
<= len P &
a = P . m &
e = P . (m + 1) &
b = P . (m + 2) &
e Joins a,
b,
G1 )
by GLIB_001:104;
reconsider a =
a,
b =
b as
Vertex of
G2 by GLIB_000:54;
set P1 =
P .cut 1,
m;
set P2 =
P .cut (m + 2),
(len P);
A9:
( 1
<= m & not 1 is
even )
by HEYTING3:1, JORDAN12:3;
A10:
(m + 2) - 2
< (len P) - 0
by A8, XREAL_1:17;
then A11:
P .cut 1,
m is_Walk_from u,
a
by A7, A8, A9, GLIB_001:38;
A12:
P .cut (m + 2),
(len P) is_Walk_from b,
v
by A7, A8, GLIB_001:38;
A13:
m + 1
<= len P
by A10, NAT_1:13;
now assume
e in (P .cut 1,m) .edges()
;
:: thesis: contradictionthen consider x being
even Element of
NAT such that A14:
( 1
<= x &
x <= len (P .cut 1,m) &
(P .cut 1,m) . x = e )
by GLIB_001:100;
x <= m
by A10, A14, GLIB_001:46;
then A15:
x < m + 1
by NAT_1:13;
x in dom (P .cut 1,m)
by A14, FINSEQ_3:27;
then
P . x = e
by A10, A14, GLIB_001:47;
hence
contradiction
by A8, A13, A14, A15, GLIB_001:139;
:: thesis: verum end; then reconsider P1' =
P .cut 1,
m as
Walk of
G2 by GLIB_001:173;
now assume
e in (P .cut (m + 2),(len P)) .edges()
;
:: thesis: contradictionthen consider x being
even Element of
NAT such that A16:
( 1
<= x &
x <= len (P .cut (m + 2),(len P)) &
(P .cut (m + 2),(len P)) . x = e )
by GLIB_001:100;
reconsider x1 =
x - 1 as
odd Element of
NAT by A16, INT_1:18;
A17:
x1 + 1
= x
;
x1 < (len (P .cut (m + 2),(len P))) - 0
by A16, XREAL_1:17;
then A18:
(
e = P . ((m + 2) + x1) &
(m + 2) + x1 in dom P )
by A8, A16, A17, GLIB_001:37;
then A19:
(m + 2) + x1 <= len P
by FINSEQ_3:27;
m + 1
< (m + 1) + 1
by NAT_1:13;
then A20:
(m + 1) + 0 < (m + 2) + x1
by NAT_1:2, XREAL_1:10;
1
<= m + 1
by NAT_1:12;
hence
contradiction
by A8, A18, A19, A20, GLIB_001:139;
:: thesis: verum end; then reconsider P2' =
P .cut (m + 2),
(len P) as
Walk of
G2 by GLIB_001:173;
A21:
P1' is_Walk_from u,
a
by A11, GLIB_001:20;
A22:
P2' is_Walk_from b,
v
by A12, GLIB_001:20;
hence
ex
W being
Walk of
G2 st
W is_Walk_from u,
v
;
:: thesis: verum end; hence
ex
W being
Walk of
G2 st
W is_Walk_from u,
v
;
:: thesis: verum end;
hence
G2 is connected
by Def1; :: thesis: verum