set W2 = W .remove (m,n);
set es1 = (W .remove (m,n)) .edgeSeq() ;
now :: thesis: W .remove (m,n) is Subwalk of W
per cases ( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) or not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) ;
suppose A1: ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) ; :: thesis: W .remove (m,n) is Subwalk of W
then reconsider m9 = m, n9 = n as odd Element of NAT ;
reconsider lenWn4 = (len W) - n9 as even Element of NAT by ;
A2: Seg (len ((W .remove (m,n)) .edgeSeq())) = dom ((W .remove (m,n)) .edgeSeq()) by FINSEQ_1:def 3;
reconsider lenWaa1 = (len W) - 1 as even Element of NAT by ;
reconsider n1 = n9 + 1 as even Element of NAT ;
reconsider maa1 = m9 - 1 as even Element of NAT by ;
set X = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } ;
set Y = { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ;
set Z = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ;
set es = () | ( { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } );
2 divides maa1 by PEPIN:22;
then A3: maa1 = 2 * (maa1 div 2) by NAT_D:3;
2 divides n1 by PEPIN:22;
then A4: n1 = 2 * (n1 div 2) by NAT_D:3;
now :: thesis: not n1 div 2 < 1
assume n1 div 2 < 1 ; :: thesis: contradiction
then 2 * (n1 div 2) < 2 * 1 by XREAL_1:68;
then (n + 1) - 1 < 2 - 1 by ;
then n9 < 1 ;
hence contradiction by ABIAN:12; :: thesis: verum
end;
then reconsider n1div2aa1 = (n1 div 2) - 1 as Element of NAT by INT_1:5;
A5: 2 divides lenWaa1 by PEPIN:22;
then A6: lenWaa1 = 2 * (lenWaa1 div 2) by NAT_D:3;
now :: thesis: for x being object st x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } holds
x in dom ()
let x be object ; :: thesis: ( x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } implies x in dom () )
assume A7: x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ; :: thesis: x in dom ()
now :: thesis: x in dom ()
per cases ( x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } or x in { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ) by ;
suppose x in { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } ; :: thesis: x in dom ()
then consider y being Nat such that
A8: y = x and
A9: 1 <= y and
A10: y <= maa1 div 2 ;
2 * y <= maa1 by ;
then 2 * y <= maa1 + 1 by NAT_1:12;
then 2 * y <= n by ;
then A11: 2 * y <= len W by ;
1 <= y + y by ;
then 2 * y in dom W by ;
hence x in dom () by ; :: thesis: verum
end;
suppose x in { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ; :: thesis: x in dom ()
then consider y being Nat such that
A12: y = x and
A13: n1 div 2 <= y and
A14: y <= lenWaa1 div 2 ;
2 * y <= lenWaa1 by ;
then A15: 2 * y <= lenWaa1 + 1 by NAT_1:12;
A16: 1 <= n1 by NAT_1:12;
n1 <= 2 * y by ;
then 1 <= 2 * y by ;
then 2 * y in dom W by ;
hence x in dom () by ; :: thesis: verum
end;
end;
end;
hence x in dom () ; :: thesis: verum
end;
then A17: { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= dom () by TARSKI:def 3;
then A18: { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= Seg (len ()) by FINSEQ_1:def 3;
then A19: { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } c= Seg (len ()) by XBOOLE_1:11;
A20: { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= Seg (len ()) by ;
reconsider X = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } , Y = { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } as finite set by ;
A21: X = { x where x is Nat : ( 0 + 1 <= x & x <= 0 + (maa1 div 2) ) } ;
A22: (dom ()) /\ ( { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ) = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } by ;
then A23: dom (() | ( { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } )) = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } by RELAT_1:61;
2 divides lenWn4 by PEPIN:22;
then A24: lenWn4 = 2 * (lenWn4 div 2) by NAT_D:3;
A25: now :: thesis: card Y = lenWn4 div 2
per cases ( n1 div 2 > lenWaa1 div 2 or n1 div 2 <= lenWaa1 div 2 ) ;
suppose A26: n1 div 2 > lenWaa1 div 2 ; :: thesis: card Y = lenWn4 div 2
then lenWaa1 < n + 1 by ;
then lenWaa1 + 1 <= n + 1 by NAT_1:13;
then len W <= n9 + 1 ;
then len W < n + 1 by XXREAL_0:1;
then len W <= n by NAT_1:13;
then A27: len W = n by ;
now :: thesis: not Y <> {}
assume Y <> {} ; :: thesis: contradiction
then consider x being object such that
A28: x in Y by XBOOLE_0:def 1;
ex x9 being Nat st
( x9 = x & n1 div 2 <= x9 & x9 <= lenWaa1 div 2 ) by A28;
hence contradiction by A26, XXREAL_0:2; :: thesis: verum
end;
hence card Y = lenWn4 div 2 by ; :: thesis: verum
end;
suppose n1 div 2 <= lenWaa1 div 2 ; :: thesis: card Y = lenWn4 div 2
then reconsider k = (lenWaa1 div 2) - (n1 div 2) as Element of NAT by INT_1:5;
Y = { x where x is Nat : ( n1 div 2 <= x & x <= (n1 div 2) + k ) } ;
then card Y = k + 1 by FINSEQ_6:130;
hence card Y = lenWn4 div 2 by A24, A6, A4; :: thesis: verum
end;
end;
end;
reconsider Z = { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } as finite set by A17;
W .edgeSeq() is Subset of () by FINSEQ_6:152;
then reconsider es = () | ( { x where x is Nat : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Nat : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ) as Subset of () by FINSEQ_6:153;
set es2 = Seq es;
A29: Seq es = es * (Sgm (dom es)) by FINSEQ_1:def 14;
set lenY = (lenWaa1 div 2) - n1div2aa1;
now :: thesis: not n1div2aa1 > lenWaa1 div 2
assume n1div2aa1 > lenWaa1 div 2 ; :: thesis: contradiction
then 2 * n1div2aa1 > 2 * (lenWaa1 div 2) by XREAL_1:68;
then ((n + 1) - 1) - 1 > (len W) - 1 by ;
hence contradiction by A1, XREAL_1:9; :: thesis: verum
end;
then reconsider lenY = (lenWaa1 div 2) - n1div2aa1 as Element of NAT by INT_1:5;
A30: Y = { x where x is Nat : ( n1div2aa1 + 1 <= x & x <= n1div2aa1 + lenY ) } ;
A31: now :: thesis: for a, b being Nat st a in X & b in Y holds
a < b
let a, b be Nat; :: thesis: ( a in X & b in Y implies a < b )
assume that
A32: a in X and
A33: b in Y ; :: thesis: a < b
consider b9 being Nat such that
A34: b9 = b and
A35: n1 div 2 <= b9 and
b9 <= lenWaa1 div 2 by A33;
consider a9 being Nat such that
A36: a9 = a and
1 <= a9 and
A37: a9 <= maa1 div 2 by A32;
2 * a9 <= maa1 by ;
then 2 * a9 < maa1 + 1 by NAT_1:13;
then 2 * a9 < n by ;
then A38: (2 * a9) + 0 < n + 1 by XREAL_1:8;
A39: n + 1 <= 2 * b9 by ;
then 2 * a9 < 2 * b9 by ;
then a9 <= b9 by XREAL_1:68;
hence a < b by ; :: thesis: verum
end;
A40: now :: thesis: card X = maa1 div 2
per cases ( maa1 div 2 = 0 or maa1 div 2 <> 0 ) ;
suppose A41: maa1 div 2 = 0 ; :: thesis: card X = maa1 div 2
now :: thesis: not X <> {}
assume X <> {} ; :: thesis: contradiction
then consider x being object such that
A42: x in X by XBOOLE_0:def 1;
ex x9 being Nat st
( x9 = x & 1 <= x9 & x9 <= maa1 div 2 ) by A42;
hence contradiction by A41; :: thesis: verum
end;
hence card X = maa1 div 2 by A41; :: thesis: verum
end;
suppose maa1 div 2 <> 0 ; :: thesis: card X = maa1 div 2
then consider k being Nat such that
A43: maa1 div 2 = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
maa1 div 2 = k + 1 by A43;
hence card X = maa1 div 2 by FINSEQ_6:130; :: thesis: verum
end;
end;
end;
then A44: dom (Sgm X) = Seg (maa1 div 2) by ;
then A45: len (Sgm X) = maa1 div 2 by FINSEQ_1:def 3;
len (W .remove (m,n)) = (2 * (len ((W .remove (m,n)) .edgeSeq()))) + 1 by Def15;
then A46: ((len W) + m) - n = (2 * (len ((W .remove (m,n)) .edgeSeq()))) + 1 by ;
now :: thesis: X /\ Y = {}
assume not X /\ Y = {} ; :: thesis: contradiction
then consider x being object such that
A47: x in X /\ Y by XBOOLE_0:def 1;
x in Y by ;
then consider y9 being Nat such that
A48: y9 = x and
A49: n1 div 2 <= y9 and
y9 <= lenWaa1 div 2 ;
x in X by ;
then consider x9 being Nat such that
A50: x9 = x and
1 <= x9 and
A51: x9 <= maa1 div 2 ;
2 * x9 <= maa1 by ;
then 2 * y9 < maa1 + 1 by ;
then 2 * y9 < n by ;
then (2 * y9) + 0 < n + 1 by XREAL_1:8;
hence contradiction by A4, A49, XREAL_1:64; :: thesis: verum
end;
then X misses Y by XBOOLE_0:def 7;
then A52: card Z = (maa1 div 2) + (lenWn4 div 2) by ;
dom es c= Seg (len ()) by ;
then rng (Sgm (dom es)) = dom es by FINSEQ_1:def 13;
then A53: dom (Seq es) = dom (Sgm Z) by
.= Seg (card Z) by ;
A54: dom (Sgm Y) = Seg (lenWn4 div 2) by ;
now :: thesis: for x9 being object st x9 in dom ((W .remove (m,n)) .edgeSeq()) holds
((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9
let x9 be object ; :: thesis: ( x9 in dom ((W .remove (m,n)) .edgeSeq()) implies ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9 )
assume A55: x9 in dom ((W .remove (m,n)) .edgeSeq()) ; :: thesis: ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9
then reconsider x = x9 as Element of NAT ;
A56: 1 <= x by ;
A57: x <= len ((W .remove (m,n)) .edgeSeq()) by ;
then A58: ((W .remove (m,n)) .edgeSeq()) . x = (W .remove (m,n)) . (2 * x) by ;
now :: thesis: ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9
per cases ) + 1 <= m or (2 * x) + 1 > m ) ;
suppose A59: (2 * x) + 1 <= m ; :: thesis: ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9
A60: 1 <= x + x by ;
((2 * x) + 1) - 1 < m - 0 by ;
then 2 * x in Seg m by ;
then A61: ((W .remove (m,n)) .edgeSeq()) . x9 = W . (2 * x) by ;
A62: (Sgm Z) . x = ((Sgm X) ^ (Sgm Y)) . x by ;
((2 * x) + 1) - 1 <= maa1 by ;
then A63: x <= maa1 div 2 by ;
then x in X by A56;
then A64: x in dom es by ;
x in dom (Sgm X) by ;
then (Sgm Z) . x = (Sgm X) . x by
.= 0 + x by ;
then (Seq es) . x = es . x by A3, A24, A23, A2, A29, A53, A46, A52, A55, FUNCT_1:12;
then A65: (Seq es) . x = () . x by ;
x <= len () by ;
hence ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9 by ; :: thesis: verum
end;
suppose A66: (2 * x) + 1 > m ; :: thesis: ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9
A67: now :: thesis: not x <= maa1 div 2
assume x <= maa1 div 2 ; :: thesis: contradiction
then 2 * x <= maa1 by ;
then (2 * x) + 1 <= maa1 + 1 by XREAL_1:7;
hence contradiction by A66; :: thesis: verum
end;
then consider k being Nat such that
A68: x = (maa1 div 2) + k by NAT_1:10;
A69: (Sgm Z) . x = ((Sgm X) ^ (Sgm Y)) . x by ;
A70: ex lenWaa19 being even Element of NAT st
( lenWaa19 = lenWaa1 & len () = lenWaa19 div 2 ) by Lm42;
2 * x <= 2 * (len ((W .remove (m,n)) .edgeSeq())) by ;
then 2 * x <= (2 * (len ((W .remove (m,n)) .edgeSeq()))) + 1 by NAT_1:12;
then A71: 2 * x <= len (W .remove (m,n)) by Def15;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A72: 2 * (n1div2aa1 + k) = ((2 * x) - m) + n by A3, A4, A68;
A73: m <= 2 * x by ;
then A74: ((2 * x) - m) + n <= len W by ;
A75: now :: thesis: not lenWaa1 div 2 < k + n1div2aa1
reconsider z = ((2 * x) - m9) + n9 as Element of NAT by A1, A73, A71, Lm30;
assume lenWaa1 div 2 < k + n1div2aa1 ; :: thesis: contradiction
then lenWaa1 < 2 * ((x - (maa1 div 2)) + n1div2aa1) by ;
then lenWaa1 + 1 < (((2 * x) - m) + n) + 1 by ;
then len W <= z by NAT_1:13;
hence contradiction by A74, XXREAL_0:1; :: thesis: verum
end;
k <> 0 by ;
then 0 + 1 < k + 1 by XREAL_1:8;
then A76: 1 <= k by NAT_1:13;
then n1div2aa1 + 1 <= n1div2aa1 + k by XREAL_1:7;
then n1div2aa1 + k in Y by A75;
then n1div2aa1 + k in dom es by ;
then A77: es . (n1div2aa1 + k) = () . (n1div2aa1 + k) by FUNCT_1:47;
A78: now :: thesis: not lenWn4 div 2 < x - (maa1 div 2)
set z = ((2 * x) - m9) + n9;
reconsider z = ((2 * x) - m9) + n9 as Element of NAT by A1, A73, A71, Lm30;
assume lenWn4 div 2 < x - (maa1 div 2) ; :: thesis: contradiction
then 2 * (lenWn4 div 2) < 2 * (x - (maa1 div 2)) by XREAL_1:68;
then A79: lenWn4 + n < (((2 * x) - m) + 1) + n by ;
((2 * x) - m9) + n9 < len W by ;
then z + 1 <= len W by NAT_1:13;
hence contradiction by A79; :: thesis: verum
end;
then k in dom (Sgm Y) by ;
then (Sgm Z) . x = (Sgm Y) . k by
.= n1div2aa1 + k by ;
then A80: (Seq es) . x = es . (n1div2aa1 + k) by A3, A24, A23, A2, A29, A53, A46, A52, A55, FUNCT_1:12;
1 <= n1div2aa1 + k by ;
then (Seq es) . x = W . (2 * (n1div2aa1 + k)) by ;
hence ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9 by A1, A58, A73, A71, A72, Lm30; :: thesis: verum
end;
end;
end;
hence ((W .remove (m,n)) .edgeSeq()) . x9 = (Seq es) . x9 ; :: thesis: verum
end;
then A81: (W .remove (m,n)) .edgeSeq() = Seq es by ;
W is_Walk_from W .first() ,W .last() ;
then W .remove (m,n) is_Walk_from W .first() ,W .last() by Lm25;
hence W .remove (m,n) is Subwalk of W by ; :: thesis: verum
end;
suppose ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) ; :: thesis: W .remove (m,n) is Subwalk of W
then W .remove (m,n) = W by Def12;
hence W .remove (m,n) is Subwalk of W by Lm70; :: thesis: verum
end;
end;
end;
hence W .remove (m,n) is Subwalk of W ; :: thesis: verum