let G be _Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 S₁[ 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 S₁[i] by A6;
consider i being Nat such that
A10: S₁[i] and
A11: for n being Nat st S₁[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 ;
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; :: thesis: ( 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()))) ) ; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: k <= l

per cases ( l <= len W1 or l > len W1 ) ;

suppose A27: l <= len W1 ; :: thesis: k <= l

reconsider k2 = l + 1 as odd Nat ;

per cases ( k2 + 2 <= len W1 or k2 + 2 > len W1 ) ;

suppose A28: k2 + 2 <= len W1 ; :: thesis: k <= l

S₁[k2]

proof

thus k2 is odd ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;

then i - 1 <= k2 - 1 by A11, XREAL_1:9;
hence k <= l ; :: thesis: verum

end;

suppose k2 + 2 > len W1 ; :: thesis: k <= l

then i + 2 <= k2 + 2 by A15, A19, XXREAL_0:2;
then i - 1 <= k2 - 1 by XREAL_1:6, XREAL_1:9;
hence k <= l ; :: thesis: verum

end;

end;

end;

suppose l > len W1 ; :: thesis: k <= l

then A37: len W1 <= l ;
A38: k <= (len W1) - 1 by A10, XREAL_1:9;
(len W1) - 1 <= (len W1) - 0 by XREAL_1:13;
then k <= len W1 by A38, XXREAL_0:2;
hence k <= l by A37, XXREAL_0:2; :: thesis: verum

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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( ( 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; :: thesis: 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

proof

assume W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) >= i + 1 ; :: thesis: contradiction
then (W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + 1 <= (W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))) + 0 by A39;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

A42: i + 1 < W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last()))) by A40, XREAL_1:6;
i + 1 in dom W1

proof

( i + 0 <= i + 1 & i + 1 <= i + 2 ) by XREAL_1:6;
then ( 1 <= i + 1 & i + 1 <= len W1 ) by XXREAL_0:2, A10, A15, A12;
hence i + 1 in dom W1 by FINSEQ_3:25; :: thesis: verum

end;

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() ; :: thesis: 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()))) ; :: thesis: 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; :: thesis: 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; :: thesis: 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() ; :: thesis: 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())))) ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

hence not e in (W1 .replaceEdgeWith (e,W3)) .edges() by A2, A45, A1, A3, Th42; :: thesis: verum