set W2 = W .remove m,n;
set es1 = (W .remove m,n) .edgeSeq() ;
now per cases
( ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n ) or m is even or n is even or not m <= n or not n <= len W or not W . m = W . n )
;
suppose A1:
( not
m is
even & not
n is
even &
m <= n &
n <= len W &
W . m = W . n )
;
:: thesis: W .remove m,n is Subwalk of Wthen reconsider m' =
m,
n' =
n as
odd Element of
NAT ;
W is_Walk_from W .first() ,
W .last()
by Def23;
then A2:
W .remove m,
n is_Walk_from W .first() ,
W .last()
by Lm25;
reconsider maa1 =
m' - 1 as
even Element of
NAT by HEYTING3:1, INT_1:18;
reconsider lenWn4 =
(len W) - n' as
even Element of
NAT by A1, INT_1:18;
reconsider n1 =
n' + 1 as
even Element of
NAT ;
reconsider lenWaa1 =
(len W) - 1 as
even Element of
NAT by HEYTING3:1, INT_1:18;
( 2
divides maa1 & 2
divides lenWn4 & 2
divides lenWaa1 & 2
divides n1 )
by PEPIN:22;
then A3:
(
maa1 = 2
* (maa1 div 2) &
lenWn4 = 2
* (lenWn4 div 2) &
lenWaa1 = 2
* (lenWaa1 div 2) &
n1 = 2
* (n1 div 2) )
by NAT_D:3;
set X =
{ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } ;
set Y =
{ x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ;
set Z =
{ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ;
set es =
(W .edgeSeq() ) | ({ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } );
then A10:
{ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= dom (W .edgeSeq() )
by TARSKI:def 3;
then A11:
(dom (W .edgeSeq() )) /\ ({ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ) = { x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) }
by XBOOLE_1:28;
then A12:
dom ((W .edgeSeq() ) | ({ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } )) = { x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) }
by RELAT_1:90;
A13:
{ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= Seg (len (W .edgeSeq() ))
by A10, FINSEQ_1:def 3;
then A14:
(
{ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } c= Seg (len (W .edgeSeq() )) &
{ x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= Seg (len (W .edgeSeq() )) )
by XBOOLE_1:11;
reconsider Z =
{ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } as
finite set by A10;
reconsider X =
{ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } ,
Y =
{ x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } as
finite set by A13, FINSET_1:13, XBOOLE_1:11;
A15:
now let a,
b be
Element of
NAT ;
:: thesis: ( a in X & b in Y implies a < b )assume A16:
(
a in X &
b in Y )
;
:: thesis: a < bthen consider a' being
Element of
NAT such that A17:
(
a' = a & 1
<= a' &
a' <= maa1 div 2 )
;
consider b' being
Element of
NAT such that A18:
(
b' = b &
n1 div 2
<= b' &
b' <= lenWaa1 div 2 )
by A16;
2
* a' <= maa1
by A3, A17, XREAL_1:66;
then
2
* a' < maa1 + 1
by NAT_1:13;
then
2
* a' < n
by A1, XXREAL_0:2;
then A19:
(2 * a') + 0 < n + 1
by XREAL_1:10;
A20:
n + 1
<= 2
* b'
by A3, A18, XREAL_1:66;
then
2
* a' < 2
* b'
by A19, XXREAL_0:2;
then
a' <= b'
by XREAL_1:70;
hence
a < b
by A17, A18, A19, A20, XXREAL_0:1;
:: thesis: verum end;
W .edgeSeq() is
Subset of
(W .edgeSeq() )
by GRAPH_2:28;
then reconsider es =
(W .edgeSeq() ) | ({ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } \/ { x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } ) as
Subset of
(W .edgeSeq() ) by GRAPH_2:29;
A21:
len (W .remove m,n) = (2 * (len ((W .remove m,n) .edgeSeq() ))) + 1
by Def15;
A22:
Seg (len ((W .remove m,n) .edgeSeq() )) = dom ((W .remove m,n) .edgeSeq() )
by FINSEQ_1:def 3;
set es2 =
Seq es;
A23:
Seq es = es * (Sgm (dom es))
by FINSEQ_1:def 14;
dom es c= Seg (len (W .edgeSeq() ))
by A11, A13, RELAT_1:90;
then
rng (Sgm (dom es)) = dom es
by FINSEQ_1:def 13;
then A24:
dom (Seq es) =
dom (Sgm Z)
by A12, A23, RELAT_1:46
.=
Seg (card Z)
by A13, FINSEQ_3:45
;
A25:
((len W) + m) - n = (2 * (len ((W .remove m,n) .edgeSeq() ))) + 1
by A1, A21, Lm31;
then
X misses Y
by XBOOLE_0:def 7;
then A40:
card Z = (maa1 div 2) + (lenWn4 div 2)
by A26, A31, CARD_2:53;
A41:
dom (Sgm X) = Seg (maa1 div 2)
by A13, A26, FINSEQ_3:45, XBOOLE_1:11;
A42:
dom (Sgm Y) = Seg (lenWn4 div 2)
by A13, A31, FINSEQ_3:45, XBOOLE_1:11;
A43:
X = { x where x is Element of NAT : ( 0 + 1 <= x & x <= 0 + (maa1 div 2) ) }
;
then reconsider n1div2aa1 =
(n1 div 2) - 1 as
Element of
NAT by INT_1:18;
set lenY =
(lenWaa1 div 2) - n1div2aa1;
then reconsider lenY =
(lenWaa1 div 2) - n1div2aa1 as
Element of
NAT by INT_1:18;
A44:
Y = { x where x is Element of NAT : ( n1div2aa1 + 1 <= x & x <= n1div2aa1 + lenY ) }
;
A45:
len (Sgm X) = maa1 div 2
by A41, FINSEQ_1:def 3;
now let x' be
set ;
:: thesis: ( x' in dom ((W .remove m,n) .edgeSeq() ) implies ((W .remove m,n) .edgeSeq() ) . x' = (Seq es) . x' )assume A46:
x' in dom ((W .remove m,n) .edgeSeq() )
;
:: thesis: ((W .remove m,n) .edgeSeq() ) . x' = (Seq es) . x'then reconsider x =
x' as
Element of
NAT ;
A47:
( 1
<= x &
x <= len ((W .remove m,n) .edgeSeq() ) )
by A46, FINSEQ_3:27;
then A48:
((W .remove m,n) .edgeSeq() ) . x = (W .remove m,n) . (2 * x)
by Def15;
now per cases
( (2 * x) + 1 <= m or (2 * x) + 1 > m )
;
suppose A49:
(2 * x) + 1
<= m
;
:: thesis: ((W .remove m,n) .edgeSeq() ) . x' = (Seq es) . x'then A50:
((2 * x) + 1) - 1
< m - 0
by XREAL_1:17;
1
<= x + x
by A47, NAT_1:12;
then
2
* x in Seg m
by A50, FINSEQ_1:3;
then A51:
((W .remove m,n) .edgeSeq() ) . x' = W . (2 * x)
by A1, A48, Lm29;
A52:
(Sgm Z) . x = ((Sgm X) ^ (Sgm Y)) . x
by A14, A15, FINSEQ_3:48;
((2 * x) + 1) - 1
<= maa1
by A49, XREAL_1:15;
then A53:
x <= maa1 div 2
by A3, XREAL_1:70;
then
x in dom (Sgm X)
by A41, A47, FINSEQ_1:3;
then (Sgm Z) . x =
(Sgm X) . x
by A52, FINSEQ_1:def 7
.=
0 + x
by A43, A47, A53, GRAPH_2:5
;
then A54:
(Seq es) . x = es . x
by A3, A12, A22, A23, A24, A25, A40, A46, FUNCT_1:22;
x in X
by A47, A53;
then A55:
x in dom es
by A12, XBOOLE_0:def 3;
then A56:
(Seq es) . x = (W .edgeSeq() ) . x
by A54, FUNCT_1:70;
x <= len (W .edgeSeq() )
by A12, A13, A55, FINSEQ_1:3;
hence
((W .remove m,n) .edgeSeq() ) . x' = (Seq es) . x'
by A47, A51, A56, Def15;
:: thesis: verum end; suppose A57:
(2 * x) + 1
> m
;
:: thesis: ((W .remove m,n) .edgeSeq() ) . x' = (Seq es) . x'then A58:
m <= 2
* x
by NAT_1:13;
2
* x <= 2
* (len ((W .remove m,n) .edgeSeq() ))
by A47, XREAL_1:66;
then
2
* x <= (2 * (len ((W .remove m,n) .edgeSeq() ))) + 1
by NAT_1:12;
then A59:
2
* x <= len (W .remove m,n)
by Def15;
then A60:
(
((W .remove m,n) .edgeSeq() ) . x' = W . (((2 * x) - m) + n) &
((2 * x) - m) + n is
Element of
NAT &
((2 * x) - m) + n <= len W )
by A1, A48, A58, Lm30;
A61:
(Sgm Z) . x = ((Sgm X) ^ (Sgm Y)) . x
by A14, A15, FINSEQ_3:48;
then consider k being
Nat such that A63:
x = (maa1 div 2) + k
by NAT_1:10;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 13;
k <> 0
by A62, A63;
then
0 < k
;
then
0 + 1
< k + 1
by XREAL_1:10;
then A64:
1
<= k
by NAT_1:13;
then
k in dom (Sgm Y)
by A42, A63, A64, FINSEQ_1:3;
then (Sgm Z) . x =
(Sgm Y) . k
by A45, A61, A63, FINSEQ_1:def 7
.=
n1div2aa1 + k
by A3, A44, A63, A64, A65, GRAPH_2:5
;
then A67:
(Seq es) . x = es . (n1div2aa1 + k)
by A3, A12, A22, A23, A24, A25, A40, A46, FUNCT_1:22;
A68:
1
<= n1div2aa1 + k
by A64, NAT_1:12;
A69:
n1div2aa1 + 1
<= n1div2aa1 + k
by A64, XREAL_1:9;
then
n1div2aa1 + k in Y
by A69;
then
n1div2aa1 + k in dom es
by A12, XBOOLE_0:def 3;
then A72:
es . (n1div2aa1 + k) = (W .edgeSeq() ) . (n1div2aa1 + k)
by FUNCT_1:70;
consider lenWaa1' being
even Element of
NAT such that A73:
(
lenWaa1' = lenWaa1 &
len (W .edgeSeq() ) = lenWaa1' div 2 )
by Lm42;
A74:
(Seq es) . x = W . (2 * (n1div2aa1 + k))
by A67, A68, A70, A72, A73, Def15;
2
* (n1div2aa1 + k) = ((2 * x) - m) + n
by A3, A63;
hence
((W .remove m,n) .edgeSeq() ) . x' = (Seq es) . x'
by A1, A48, A58, A59, A74, Lm30;
:: thesis: verum end; hence
((W .remove m,n) .edgeSeq() ) . x' = (Seq es) . x'
;
:: thesis: verum end; then
(W .remove m,n) .edgeSeq() = Seq es
by A3, A22, A24, A25, A40, FUNCT_1:9;
hence
W .remove m,
n is
Subwalk of
W
by A2, Def32;
:: thesis: verum end;
hence
W .remove m,n is Subwalk of W
; :: thesis: verum