let G be _Graph; for W1, W3 being Walk of G
for e being object st e Joins W3 .first() ,W3 .last() ,G & not e in W3 .edges() & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 & ( for n, m being even Nat st n in dom W1 & m in dom W1 & W1 . n = e & W1 . m = e holds
n = m ) holds
not e in (W1 .replaceEdgeWith (e,W3)) .edges()
let W1, W3 be Walk of G; for e being object st e Joins W3 .first() ,W3 .last() ,G & not e in W3 .edges() & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 & ( for n, m being even Nat st n in dom W1 & m in dom W1 & W1 . n = e & W1 . m = e holds
n = m ) holds
not e in (W1 .replaceEdgeWith (e,W3)) .edges()
let e be object ; ( e Joins W3 .first() ,W3 .last() ,G & not e in W3 .edges() & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 & ( for n, m being even Nat st n in dom W1 & m in dom W1 & W1 . n = e & W1 . m = e holds
n = m ) implies not e in (W1 .replaceEdgeWith (e,W3)) .edges() )
assume that
A1:
e Joins W3 .first() ,W3 .last() ,G
and
A2:
not e in W3 .edges()
and
A3:
G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0
and
A4:
for n, m being even Nat st n in dom W1 & m in dom W1 & W1 . n = e & W1 . m = e holds
n = m
; not e in (W1 .replaceEdgeWith (e,W3)) .edges()
set W2 = G .walkOf ((W3 .first()),e,(W3 .last()));
set W9 = W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3);
A6:
G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1,1
by A3, Th18;
A7:
len (G .walkOf ((W3 .first()),e,(W3 .last()))) = 3
by A1, GLIB_001:14;
defpred S1[ Nat] means ( $1 is odd & 1 <= $1 & $1 <= len W1 & mid (W1,$1,(($1 -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))))) = G .walkOf ((W3 .first()),e,(W3 .last())) );
A9:
ex i being Nat st S1[i]
by A6;
consider i being Nat such that
A10:
S1[i]
and
A11:
for n being Nat st S1[n] holds
i <= n
from NAT_1:sch 5(A9);
reconsider i = i as odd Element of NAT by A10, ORDINAL1:def 12;
set j = (i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last()))));
G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1,i
by A10;
then
G .walkOf ((W3 .first()),e,(W3 .last())) is_substring_of W1,i
by Th12;
then A12:
( 1 <= (i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))) & (i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))) <= len W1 & i <= (i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))) )
by Th11;
A13:
mid (W1,i,((i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))))) = <*(W3 .first()),e,(W3 .last())*>
by A1, A10, GLIB_001:def 5;
set n1 = i + 1;
i - 1 = i -' 1
by A10, XREAL_1:233;
then A15:
(i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))) = i + 2
by A7;
A16:
( 1 <= 2 & 2 <= len (mid (W1,i,((i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last()))))))) )
by A7, A10;
A19:
( 1 <= (i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))) & (i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))) <= len W1 )
by A12;
A20:
i <= (i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last()))))
by A12;
then
(mid (W1,i,((i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last()))))))) . 2 = W1 . ((2 + i) -' 1)
by A10, A16, A19, FINSEQ_6:118;
then <*(W3 .first()),e,(W3 .last())*> . 2 =
W1 . ((2 + i) - 1)
by A13, NAT_D:37
.=
W1 . (i + 1)
;
then A21:
W1 . (i + 1) = e
by FINSEQ_1:45;
reconsider k = i - 1 as even Nat by CHORD:1;
A22:
for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n
proof
let n be
Nat;
( 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) implies W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n )
assume A23:
( 1
<= n &
n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) )
;
W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n
then
( 1
<= n &
n <= len (mid (W1,i,((i -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last()))))))) )
by A10;
then A24:
W1 . ((n + i) -' 1) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n
by A10, A19, A20, FINSEQ_6:118;
(n + i) -' 1 =
(n + i) - 1
by A23, NAT_D:37
.=
k + n
;
hence
W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n
by A24;
verum
end;
A25:
for l being even Nat st ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (l + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) holds
k <= l
proof
let l be
even Nat;
( ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (l + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) implies k <= l )
assume A26:
for
n being
Nat st 1
<= n &
n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (l + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n
;
k <= l
per cases
( l <= len W1 or l > len W1 )
;
suppose A27:
l <= len W1
;
k <= lreconsider k2 =
l + 1 as
odd Nat ;
per cases
( k2 + 2 <= len W1 or k2 + 2 > len W1 )
;
suppose A28:
k2 + 2
<= len W1
;
k <= l
S1[
k2]
proof
thus
k2 is
odd
;
( 1 <= k2 & k2 <= len W1 & mid (W1,k2,((k2 -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))))) = G .walkOf ((W3 .first()),e,(W3 .last())) )
thus A30:
1
<= k2
by ABIAN:12;
( k2 <= len W1 & mid (W1,k2,((k2 -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))))) = G .walkOf ((W3 .first()),e,(W3 .last())) )
thus A31:
k2 <= len W1
by A27, Th1;
mid (W1,k2,((k2 -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))))) = G .walkOf ((W3 .first()),e,(W3 .last()))
k2 - 1
= k2 -' 1
by A30, XREAL_1:233;
then A33:
(k2 -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))) = k2 + 2
by A7;
A34:
k2 in dom W1
by A30, A31, FINSEQ_3:25;
A35:
( 1
<= 1 & 1
<= len (G .walkOf ((W3 .first()),e,(W3 .last()))) & 1
<= 2 & 2
<= len (G .walkOf ((W3 .first()),e,(W3 .last()))) & 1
<= 3 & 3
<= len (G .walkOf ((W3 .first()),e,(W3 .last()))) )
by A7;
mid (
W1,
k2,
((k2 -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last())))))) =
<*(W1 . k2),(W1 . (k2 + 1)),(W1 . (k2 + 2))*>
by A33, A34, A28, Th10
.=
<*((G .walkOf ((W3 .first()),e,(W3 .last()))) . 1),(W1 . (l + 2)),(W1 . (l + 3))*>
by A26, A35
.=
<*((G .walkOf ((W3 .first()),e,(W3 .last()))) . 1),((G .walkOf ((W3 .first()),e,(W3 .last()))) . 2),(W1 . (l + 3))*>
by A26, A35
.=
<*((G .walkOf ((W3 .first()),e,(W3 .last()))) . 1),((G .walkOf ((W3 .first()),e,(W3 .last()))) . 2),((G .walkOf ((W3 .first()),e,(W3 .last()))) . 3)*>
by A26, A35
;
hence
mid (
W1,
k2,
((k2 -' 1) + (len (G .walkOf ((W3 .first()),e,(W3 .last()))))))
= G .walkOf (
(W3 .first()),
e,
(W3 .last()))
by A7, FINSEQ_1:45;
verum
end; then
i - 1
<= k2 - 1
by A11, XREAL_1:9;
hence
k <= l
;
verum end; end; end; end;
end;
( i <= len W1 & ex k being even Nat st
( i = k + 1 & ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (l + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) holds
k <= l ) ) )
proof
thus
i <= len W1
by A10;
ex k being even Nat st
( i = k + 1 & ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (l + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) holds
k <= l ) )
take
k
;
( i = k + 1 & ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (l + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) holds
k <= l ) )
thus
i = k + 1
;
( ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (l + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) holds
k <= l ) )
thus
( ( for
n being
Nat st 1
<= n &
n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) & ( for
l being
even Nat st ( for
n being
Nat st 1
<= n &
n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (l + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) holds
k <= l ) )
by A22, A25;
verum
end;
then A39:
i = W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))
by A3, Def3;
( i + 2 <= len W1 & ex k being even Nat st
( i + 2 = k + (len (G .walkOf ((W3 .first()),e,(W3 .last())))) & ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (k + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len (G .walkOf ((W3 .first()),e,(W3 .last()))) holds
W1 . (l + n) = (G .walkOf ((W3 .first()),e,(W3 .last()))) . n ) holds
k <= l ) ) )
by A7, A15, A19, A22, A25;
then A40:
i + 2 = W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))
by A3, Def4;
A41:
W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) < i + 1
A42:
i + 1 < W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))
by A40, XREAL_1:6;
i + 1 in dom W1
then A44:
( i + 1 in dom W1 & W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) < i + 1 & i + 1 < W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) )
by A41, A42;
A45:
not e in (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges()
proof
assume
e in (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges()
;
contradiction
then consider n2 being
even Element of
NAT such that A46:
( 1
<= n2 &
n2 <= len (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) )
and A47:
(W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) . n2 = e
by GLIB_001:99;
reconsider n9 = 1 as
odd Element of
NAT by POLYFORM:4;
A48:
(
n9 <= W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) &
W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) <= len W1 )
by A3, Th35;
then A49:
(len (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last()))))))) + 1
= (W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + 1
by GLIB_001:36;
then A50:
n2 <= W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))
by A46;
not
n2 is
zero
by A46;
then reconsider n3 =
n2 - 1 as
Nat by CHORD:1;
reconsider n3 =
n3 as
Element of
NAT by ORDINAL1:def 12;
W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) <= len W1
by A3, Th35;
then
n2 <= len W1
by A50, XXREAL_0:2;
then A51:
n2 in dom W1
by A46, FINSEQ_3:25;
n3 < W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))
proof
assume
n3 >= W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))
;
contradiction
then A52:
(n2 - 1) + 1
>= (W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + 1
by XREAL_1:6;
(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + 0 < (W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + 1
by XREAL_1:8;
hence
contradiction
by A50, A52, XXREAL_0:2;
verum
end;
then
(W1 .cut (n9,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) . (n3 + 1) = W1 . (n9 + n3)
by A48, A49, GLIB_001:36;
hence
contradiction
by A50, A44, A21, A4, A47, A51;
verum
end;
not e in (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges()
proof
assume
e in (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges()
;
contradiction
then consider n2 being
even Element of
NAT such that A53:
( 1
<= n2 &
n2 <= len (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) )
and A54:
(W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) . n2 = e
by GLIB_001:99;
reconsider n9 = 1 as
odd Element of
NAT by POLYFORM:4;
set D =
((len W1) + 1) - (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))));
A55:
(
n9 <= W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) &
W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) <= len W1 )
by A3, Th35;
then A56:
(len (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1)))) + (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) = (len W1) + 1
by GLIB_001:36;
then A57:
n2 <= ((len W1) + 1) - (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))))
by A53;
not
n2 is
zero
by A53;
then reconsider n3 =
n2 - 1 as
Nat by CHORD:1;
reconsider n3 =
n3 as
Element of
NAT by ORDINAL1:def 12;
1
<= W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))
by A3, Th35;
then
1
+ (n2 - 1) <= (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + (n2 - 1)
by XREAL_1:6;
then A58:
1
<= (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + n3
by A53, XXREAL_0:2;
(W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + n3 = n2 + ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) - 1)
;
then
n3 + (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) <= (((len W1) + 1) - (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))))) + ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) - 1)
by A57, XREAL_1:6;
then A59:
(W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + n3 in dom W1
by A58, FINSEQ_3:25;
n3 < ((len W1) + 1) - (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))))
proof
assume
n3 >= ((len W1) + 1) - (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))))
;
contradiction
then A60:
(n2 - 1) + 1
>= (((len W1) + 1) - (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))))) + 1
by XREAL_1:6;
(((len W1) + 1) - (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))))) + 0 < (((len W1) + 1) - (W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))))) + 1
by XREAL_1:8;
hence
contradiction
by A57, A60, XXREAL_0:2;
verum
end;
then
(W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) . (n3 + 1) = W1 . ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + n3)
by A55, GLIB_001:36, A56;
then
((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + n2) - 1
= i + 1
by A21, A4, A54, A59, A44;
then
(W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + 1
<= (i + 1) + 1
by A53, XREAL_1:7;
hence
contradiction
by A44, XREAL_1:6;
verum
end;
hence
not e in (W1 .replaceEdgeWith (e,W3)) .edges()
by A2, A45, A1, A3, Th42; verum