let G be _Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( (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() by GLIB_001:def 7
.= W .first() by GLIB_001:def 24
.= W . 1 by GLIB_001:def 6 ;
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; :: thesis: ( ( 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))} ) ) :: thesis: ( 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 ; :: thesis: ( (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()) <> {} ; :: thesis: 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; :: thesis: verum
end;
hence (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() by XBOOLE_0:def 7; :: thesis: ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))}
now :: thesis: 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 ; :: thesis: ( ( 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 :: thesis: ( 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() ; :: thesis: 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))) ; :: thesis: 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; :: thesis: 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 ) ; :: thesis: 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; :: thesis: verum
end;
end;
end;
assume x in (W .edges()) \ {(W . (n + 1))} ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose n < m ; :: thesis: 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)))
proof
assume len (W .cut ((n + 2),(len W))) <= k ; :: thesis: contradiction
then (len (W .cut ((n + 2),(len W)))) + ((len (W .cut (1,n))) + 1) <= k + ((len (W .cut (1,n))) + 1) by XREAL_1:6;
hence contradiction by A10, A11, A32, A36; :: thesis: verum
end;
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; :: thesis: verum
end;
end;
end;
hence ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} by TARSKI:2; :: thesis: verum
end;
assume A40: W is Path-like ; :: thesis: ( ((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 :: thesis: 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 ; :: thesis: ( ( 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 :: thesis: ( 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()) ; :: thesis: 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, GLIB_001:def 6; :: thesis: verum
end;
assume x = W .first() ; :: thesis: x in ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices())
then x = W . 1 by GLIB_001:def 6;
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; :: thesis: verum
end;
hence A48: ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} by TARSKI:def 1; :: thesis: ( ( 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 ) :: thesis: (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 ) ; :: thesis: 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; :: thesis: verum
end;
per cases ( n = 1 or n + 2 = len W or ( n <> 1 & n + 2 <> len W ) ) ;
suppose n = 1 ; :: thesis: (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like
then W .cut (1,n) is V5() by A4, GLIB_001:131;
hence (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like by A40, GLIB_001:130; :: thesis: verum
end;
suppose n + 2 = len W ; :: thesis: (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like
then W .cut ((n + 2),(len W)) is V5() by GLIB_001:131;
hence (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like by A7, A8, A40, HELLY:16; :: thesis: verum
end;
suppose A52: ( n <> 1 & n + 2 <> len W ) ; :: thesis: (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 A54: W .cut ((n + 2),(len W)) is open by A40, Th30;
(W .cut ((n + 2),(len W))) .last() = W .first() by A7, A8, GLIB_001:def 6;
hence (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like by A7, A8, A40, A48, A53, A54, HELLY:19; :: thesis: verum
end;
end;