let G be _Graph; for W being closed Walk of G
for n being odd Element of NAT st n < len W holds
( (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is_Walk_from W . (n + 2),W . n & ( W is Trail-like implies ( (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() & ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} ) ) & ( W is Path-like implies ( ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} & ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like ) ) )
let W be closed Walk of G; for n being odd Element of NAT st n < len W holds
( (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is_Walk_from W . (n + 2),W . n & ( W is Trail-like implies ( (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() & ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} ) ) & ( W is Path-like implies ( ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} & ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like ) ) )
let n be odd Element of NAT ; ( n < len W implies ( (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is_Walk_from W . (n + 2),W . n & ( W is Trail-like implies ( (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() & ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} ) ) & ( W is Path-like implies ( ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} & ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like ) ) ) )
assume A1:
n < len W
; ( (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is_Walk_from W . (n + 2),W . n & ( W is Trail-like implies ( (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() & ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} ) ) & ( W is Path-like implies ( ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} & ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like ) ) )
set W7 = W .cut ((n + 2),(len W));
set W8 = W .cut (1,n);
set W9 = (W .cut ((n + 2),(len W))) .append (W .cut (1,n));
set e = W . (n + 1);
A2:
( 0 + 1 <= n + 1 & n + 2 <= len W )
by A1, CHORD:4, XREAL_1:6;
then A3:
W .cut ((n + 2),(len W)) is_Walk_from W . (n + 2),W . (len W)
by GLIB_001:37;
A4:
n <= len W
by A1;
A5:
( 1 <= n & 1 is odd )
by CHORD:2, POLYFORM:4;
then A6:
W .cut (1,n) is_Walk_from W . 1,W . n
by A4, GLIB_001:37;
A7: W . (len W) =
W .last()
.=
W .first()
by GLIB_001:def 24
.=
W . 1
;
hence
(W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is_Walk_from W . (n + 2),W . n
by A3, A6, GLIB_001:31; ( ( W is Trail-like implies ( (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() & ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} ) ) & ( W is Path-like implies ( ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} & ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like ) ) )
A8:
( (W .cut ((n + 2),(len W))) .last() = W . (len W) & (W .cut (1,n)) .first() = W . 1 )
by A3, A6, GLIB_001:def 23;
then A9:
(len ((W .cut ((n + 2),(len W))) .append (W .cut (1,n)))) + 1 = (len (W .cut ((n + 2),(len W)))) + (len (W .cut (1,n)))
by A7, GLIB_001:28;
A10:
len (W .cut (1,n)) = n
by A4, GLIB_001:45;
A11:
(len (W .cut ((n + 2),(len W)))) + (n + 2) = (len W) + 1
by A2, GLIB_001:36;
thus
( W is Trail-like implies ( (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() & ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} ) )
( W is Path-like implies ( ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} & ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like ) )proof
assume A12:
W is
Trail-like
;
( (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() & ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} )
((W .cut ((n + 2),(len W))) .edges()) /\ ((W .cut (1,n)) .edges()) = {}
proof
assume
((W .cut ((n + 2),(len W))) .edges()) /\ ((W .cut (1,n)) .edges()) <> {}
;
contradiction
then consider x being
object such that A13:
x in ((W .cut ((n + 2),(len W))) .edges()) /\ ((W .cut (1,n)) .edges())
by XBOOLE_0:def 1;
A14:
(
x in (W .cut ((n + 2),(len W))) .edges() &
x in (W .cut (1,n)) .edges() )
by A13, XBOOLE_0:def 4;
then consider n1 being
odd Element of
NAT such that A15:
(
n1 < len (W .cut ((n + 2),(len W))) &
(W .cut ((n + 2),(len W))) . (n1 + 1) = x )
by GLIB_001:100;
consider n2 being
odd Element of
NAT such that A16:
(
n2 < len (W .cut (1,n)) &
(W .cut (1,n)) . (n2 + 1) = x )
by A14, GLIB_001:100;
A17:
W . (1 + n2) =
x
by A4, A5, A16, GLIB_001:36
.=
W . ((n + 2) + n1)
by A2, A15, GLIB_001:36
;
1
+ 0 <= 2
+ n1
by XREAL_1:7;
then A18:
1
+ n2 < (2 + n1) + n
by A10, A16, XREAL_1:8;
(n + 2) + n1 < (n + 2) + (len (W .cut ((n + 2),(len W))))
by A15, XREAL_1:6;
then
(n + 2) + n1 < (len W) + 1
by A11;
then A19:
(n + 2) + n1 <= len W
by NAT_1:13;
1
+ 0 <= 1
+ n2
by XREAL_1:6;
hence
contradiction
by A12, A17, A18, A19, GLIB_001:138;
verum
end;
hence
(W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges()
by XBOOLE_0:def 7;
((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))}
now for x being object holds
( ( x in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() implies x in (W .edges()) \ {(W . (n + 1))} ) & ( x in (W .edges()) \ {(W . (n + 1))} implies x in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() ) )let x be
object ;
( ( x in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() implies x in (W .edges()) \ {(W . (n + 1))} ) & ( x in (W .edges()) \ {(W . (n + 1))} implies b1 in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() ) )hereby ( x in (W .edges()) \ {(W . (n + 1))} implies b1 in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() )
assume
x in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges()
;
x in (W .edges()) \ {(W . (n + 1))}then consider m being
odd Element of
NAT such that A20:
(
m < len ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) &
((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) . (m + 1) = x )
by GLIB_001:100;
m + 1
in dom ((W .cut ((n + 2),(len W))) .append (W .cut (1,n)))
by A20, GLIB_001:12;
per cases then
( m + 1 in dom (W .cut ((n + 2),(len W))) or ex k being Element of NAT st
( k < len (W .cut (1,n)) & m + 1 = (len (W .cut ((n + 2),(len W)))) + k ) )
by GLIB_001:34;
suppose A21:
m + 1
in dom (W .cut ((n + 2),(len W)))
;
x in (W .edges()) \ {(W . (n + 1))}then A22:
x =
(W .cut ((n + 2),(len W))) . (m + 1)
by A20, GLIB_001:32
.=
W . (((n + 2) + (m + 1)) - 1)
by A2, A21, GLIB_001:47
.=
W . ((n + 2) + m)
;
((n + 2) + (m + 1)) - 1
in dom W
by A2, A21, GLIB_001:47;
then A23:
(n + 2) + m <= len W
by FINSEQ_3:25;
1
+ 0 < 2
+ m
by XREAL_1:8;
then
n + 1
< n + (2 + m)
by XREAL_1:8;
then A24:
W . (n + 1) <> W . ((n + 2) + m)
by A12, A2, A23, GLIB_001:138;
((n + 1) + m) + 1
< (len W) + 1
by A23, NAT_1:13;
then
x in W .edges()
by A22, XREAL_1:6, GLIB_001:100;
hence
x in (W .edges()) \ {(W . (n + 1))}
by A22, A24, ZFMISC_1:56;
verum end; suppose
ex
k being
Element of
NAT st
(
k < len (W .cut (1,n)) &
m + 1
= (len (W .cut ((n + 2),(len W)))) + k )
;
x in (W .edges()) \ {(W . (n + 1))}then consider k being
Element of
NAT such that A25:
(
k < len (W .cut (1,n)) &
m + 1
= (len (W .cut ((n + 2),(len W)))) + k )
;
A26:
x =
(W .cut (1,n)) . (k + 1)
by A7, A8, A20, A25, GLIB_001:33
.=
W . (1 + k)
by A4, A5, A25, GLIB_001:36
;
A27:
1
+ 0 <= k + 1
by XREAL_1:6;
A28:
k is
odd
by A25;
A29:
k + 1
< n + 1
by A10, A25, XREAL_1:8;
n + 1
<= len W
by A1, NAT_1:13;
then
W . (k + 1) <> W . (n + 1)
by A12, A27, A28, A29, GLIB_001:138;
then A30:
x <> W . (n + 1)
by A26;
k < len W
by A1, A10, A25, XXREAL_0:2;
then
x in W .edges()
by A26, A28, GLIB_001:100;
hence
x in (W .edges()) \ {(W . (n + 1))}
by A30, ZFMISC_1:56;
verum end;
end; assume
x in (W .edges()) \ {(W . (n + 1))}
;
b1 in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() then A31:
(
x in W .edges() &
x <> W . (n + 1) )
by ZFMISC_1:56;
then consider m being
odd Element of
NAT such that A32:
(
m < len W &
W . (m + 1) = x )
by GLIB_001:100;
per cases
( m < n or n < m )
by A31, A32, XXREAL_0:1;
suppose A33:
m < n
;
b1 in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() A34:
x =
(W .cut (1,n)) . (m + 1)
by A4, A5, A10, A32, A33, GLIB_001:36
.=
((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) . ((len (W .cut ((n + 2),(len W)))) + m)
by A7, A8, A10, A33, GLIB_001:33
;
( 1
<= m &
0 <= len (W .cut ((n + 2),(len W))) )
by CHORD:2;
then A35:
1
+ 0 <= m + (len (W .cut ((n + 2),(len W))))
by XREAL_1:7;
(len (W .cut ((n + 2),(len W)))) + m < (len (W .cut ((n + 2),(len W)))) + (len (W .cut (1,n)))
by A10, A33, XREAL_1:8;
then
(len (W .cut ((n + 2),(len W)))) + m <= len ((W .cut ((n + 2),(len W))) .append (W .cut (1,n)))
by A9, NAT_1:13;
hence
x in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges()
by A34, A35, GLIB_001:99;
verum end; suppose
n < m
;
b1 in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() then
(len (W .cut (1,n))) + 1
<= m
by A10, NAT_1:13;
then consider k being
Nat such that A36:
m = ((len (W .cut (1,n))) + 1) + k
by NAT_1:10;
reconsider k =
k as
odd Element of
NAT by A36, ORDINAL1:def 12;
A37:
k < len (W .cut ((n + 2),(len W)))
then A38:
k + 1
in dom (W .cut ((n + 2),(len W)))
by GLIB_001:12;
A39:
x =
W . ((n + 2) + k)
by A10, A32, A36
.=
(W .cut ((n + 2),(len W))) . (k + 1)
by A2, A37, GLIB_001:36
.=
((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) . (k + 1)
by A38, GLIB_001:32
;
len (W .cut ((n + 2),(len W))) <= len ((W .cut ((n + 2),(len W))) .append (W .cut (1,n)))
by A7, A8, GLIB_001:29;
then
k < len ((W .cut ((n + 2),(len W))) .append (W .cut (1,n)))
by A37, XXREAL_0:2;
hence
x in ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges()
by A39, GLIB_001:100;
verum end; end;
hence
((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))}
by TARSKI:2;
verum
end;
assume A40:
W is Path-like
; ( ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} & ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like )
now for x being object holds
( ( x in ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) implies x = W .first() ) & ( x = W .first() implies x in ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) ) )let x be
object ;
( ( x in ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) implies x = W .first() ) & ( x = W .first() implies x in ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) ) )hereby ( x = W .first() implies x in ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) )
assume
x in ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices())
;
x = W .first() then A41:
(
x in (W .cut ((n + 2),(len W))) .vertices() &
x in (W .cut (1,n)) .vertices() )
by XBOOLE_0:def 4;
then consider n1 being
odd Element of
NAT such that A42:
(
n1 <= len (W .cut ((n + 2),(len W))) &
(W .cut ((n + 2),(len W))) . n1 = x )
by GLIB_001:87;
consider n2 being
odd Element of
NAT such that A43:
(
n2 <= len (W .cut (1,n)) &
(W .cut (1,n)) . n2 = x )
by A41, GLIB_001:87;
reconsider n3 =
n1 - 1,
n4 =
n2 - 1 as
Nat by CHORD:2;
reconsider n3 =
n3,
n4 =
n4 as
even Element of
NAT by ORDINAL1:def 12;
(
n3 + 1
< (len (W .cut ((n + 2),(len W)))) + 1 &
n4 + 1
< (len (W .cut (1,n))) + 1 )
by A42, A43, NAT_1:13;
then A44:
(
n3 < len (W .cut ((n + 2),(len W))) &
n4 < len (W .cut (1,n)) )
by XREAL_1:6;
then A45:
W . ((n + 2) + n3) =
(W .cut ((n + 2),(len W))) . (n3 + 1)
by A2, GLIB_001:36
.=
x
by A42
;
A46:
x = W . (1 + n4)
by A4, A5, A43, A44, GLIB_001:36;
A47:
n2 + 0 < n + (2 + n3)
by A10, A43, XREAL_1:8;
(n + 2) + n3 = (n + 1) + n1
;
then
(n + 2) + n3 <= (n + 1) + (len (W .cut ((n + 2),(len W))))
by A42, XREAL_1:6;
then
1
+ n4 = 1
by A11, A40, A45, A46, A47, GLIB_001:def 28;
hence
x = W .first()
by A46;
verum
end; assume
x = W .first()
;
x in ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices())then
x = W . 1
;
then
(
x in (W .cut ((n + 2),(len W))) .vertices() &
x in (W .cut (1,n)) .vertices() )
by A7, A8, GLIB_001:88;
hence
x in ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices())
by XBOOLE_0:def 4;
verum end;
hence A48:
((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())}
by TARSKI:def 1; ( ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like )
thus
( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open )
(W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like proof
assume A49:
( not
W . (n + 1) in G .loops() &
(W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is
closed )
;
contradiction
A50:
W . (n + 2) =
(W .cut ((n + 2),(len W))) .first()
by A3, GLIB_001:def 23
.=
((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .first()
by A7, A8, GLIB_001:30
.=
((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .last()
by A49, GLIB_001:def 24
.=
(W .cut (1,n)) .last()
by A7, A8, GLIB_001:30
.=
W . n
by A6, GLIB_001:def 23
;
n + 0 < n + 2
by XREAL_1:8;
then A51:
(
n = 1 &
n + 2
= len W )
by A2, A40, A50, GLIB_001:def 28;
W . (n + 1) Joins W . n,
W . (n + 2),
G
by A1, GLIB_001:def 3;
hence
contradiction
by A7, A49, A51, GLIB_009:def 2;
verum
end;
per cases
( n = 1 or n + 2 = len W or ( n <> 1 & n + 2 <> len W ) )
;
suppose A52:
(
n <> 1 &
n + 2
<> len W )
;
(W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like then
( 1
< n &
n <> len W )
by A1, A5, XXREAL_0:1;
then A53:
W .cut (1,
n) is
open
by A4, A40, Th30, POLYFORM:4;
(
n + 2
< len W &
n + 2
<> 1 )
by A2, A52, XXREAL_0:1;
then
W .cut (
(n + 2),
(len W)) is
open
by A40, Th30;
hence
(W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is
Path-like
by A7, A8, A40, A48, A53, HELLY:19;
verum end;