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 )
;
W .remove m,n is Subwalk of Wthen reconsider m9 =
m,
n9 =
n as
odd Element of
NAT ;
reconsider lenWn4 =
(len W) - n9 as
even Element of
NAT by A1, INT_1:18;
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 HEYTING3:1, INT_1:18;
reconsider n1 =
n9 + 1 as
even Element of
NAT ;
reconsider maa1 =
m9 - 1 as
even Element of
NAT by HEYTING3:1, INT_1:18;
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 ) } );
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;
then reconsider n1div2aa1 =
(n1 div 2) - 1 as
Element of
NAT by INT_1:18;
A5:
2
divides lenWaa1
by PEPIN:22;
then A6:
lenWaa1 = 2
* (lenWaa1 div 2)
by NAT_D:3;
then A17:
{ 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 A18:
{ 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 FINSEQ_1:def 3;
then A19:
{ x where x is Element of NAT : ( 1 <= x & x <= maa1 div 2 ) } c= Seg (len (W .edgeSeq() ))
by XBOOLE_1:11;
A20:
{ x where x is Element of NAT : ( n1 div 2 <= x & x <= lenWaa1 div 2 ) } c= Seg (len (W .edgeSeq() ))
by A18, XBOOLE_1:11;
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 A18, FINSET_1:13, XBOOLE_1:11;
A21:
X = { x where x is Element of NAT : ( 0 + 1 <= x & x <= 0 + (maa1 div 2) ) }
;
A22:
(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 A17, XBOOLE_1:28;
then A23:
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;
2
divides lenWn4
by PEPIN:22;
then A24:
lenWn4 = 2
* (lenWn4 div 2)
by NAT_D:3;
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 A17;
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;
set es2 =
Seq es;
A29:
Seq es = es * (Sgm (dom es))
by FINSEQ_1:def 14;
set lenY =
(lenWaa1 div 2) - n1div2aa1;
then reconsider lenY =
(lenWaa1 div 2) - n1div2aa1 as
Element of
NAT by INT_1:18;
A30:
Y = { x where x is Element of NAT : ( n1div2aa1 + 1 <= x & x <= n1div2aa1 + lenY ) }
;
A31:
now let a,
b be
Element of
NAT ;
( a in X & b in Y implies a < b )assume that A32:
a in X
and A33:
b in Y
;
a < bconsider b9 being
Element of
NAT such that A34:
b9 = b
and A35:
n1 div 2
<= b9
and
b9 <= lenWaa1 div 2
by A33;
consider a9 being
Element of
NAT such that A36:
a9 = a
and
1
<= a9
and A37:
a9 <= maa1 div 2
by A32;
2
* a9 <= maa1
by A3, A37, XREAL_1:66;
then
2
* a9 < maa1 + 1
by NAT_1:13;
then
2
* a9 < n
by A1, XXREAL_0:2;
then A38:
(2 * a9) + 0 < n + 1
by XREAL_1:10;
A39:
n + 1
<= 2
* b9
by A4, A35, XREAL_1:66;
then
2
* a9 < 2
* b9
by A38, XXREAL_0:2;
then
a9 <= b9
by XREAL_1:70;
hence
a < b
by A36, A34, A38, A39, XXREAL_0:1;
verum end; then A44:
dom (Sgm X) = Seg (maa1 div 2)
by A18, FINSEQ_3:45, XBOOLE_1:11;
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 A1, Lm31;
then
X misses Y
by XBOOLE_0:def 7;
then A52:
card Z = (maa1 div 2) + (lenWn4 div 2)
by A40, A25, CARD_2:53;
dom es c= Seg (len (W .edgeSeq() ))
by A22, A18, RELAT_1:90;
then
rng (Sgm (dom es)) = dom es
by FINSEQ_1:def 13;
then A53:
dom (Seq es) =
dom (Sgm Z)
by A23, A29, RELAT_1:46
.=
Seg (card Z)
by A18, FINSEQ_3:45
;
A54:
dom (Sgm Y) = Seg (lenWn4 div 2)
by A18, A25, FINSEQ_3:45, XBOOLE_1:11;
now let x9 be
set ;
( 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() )
;
((W .remove m,n) .edgeSeq() ) . x9 = (Seq es) . x9then reconsider x =
x9 as
Element of
NAT ;
A56:
1
<= x
by A55, FINSEQ_3:27;
A57:
x <= len ((W .remove m,n) .edgeSeq() )
by A55, FINSEQ_3:27;
then A58:
((W .remove m,n) .edgeSeq() ) . x = (W .remove m,n) . (2 * x)
by A56, Def15;
now per cases
( (2 * x) + 1 <= m or (2 * x) + 1 > m )
;
suppose A59:
(2 * x) + 1
<= m
;
((W .remove m,n) .edgeSeq() ) . x9 = (Seq es) . x9A60:
1
<= x + x
by A56, NAT_1:12;
((2 * x) + 1) - 1
< m - 0
by A59, XREAL_1:17;
then
2
* x in Seg m
by A60, FINSEQ_1:3;
then A61:
((W .remove m,n) .edgeSeq() ) . x9 = W . (2 * x)
by A1, A58, Lm29;
A62:
(Sgm Z) . x = ((Sgm X) ^ (Sgm Y)) . x
by A19, A20, A31, FINSEQ_3:48;
((2 * x) + 1) - 1
<= maa1
by A59, XREAL_1:15;
then A63:
x <= maa1 div 2
by A3, XREAL_1:70;
then
x in X
by A56;
then A64:
x in dom es
by A23, XBOOLE_0:def 3;
x in dom (Sgm X)
by A44, A56, A63, FINSEQ_1:3;
then (Sgm Z) . x =
(Sgm X) . x
by A62, FINSEQ_1:def 7
.=
0 + x
by A21, A56, A63, GRAPH_2:5
;
then
(Seq es) . x = es . x
by A3, A24, A23, A2, A29, A53, A46, A52, A55, FUNCT_1:22;
then A65:
(Seq es) . x = (W .edgeSeq() ) . x
by A64, FUNCT_1:70;
x <= len (W .edgeSeq() )
by A23, A18, A64, FINSEQ_1:3;
hence
((W .remove m,n) .edgeSeq() ) . x9 = (Seq es) . x9
by A56, A61, A65, Def15;
verum end; suppose A66:
(2 * x) + 1
> m
;
((W .remove m,n) .edgeSeq() ) . x9 = (Seq es) . x9then 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 A19, A20, A31, FINSEQ_3:48;
A70:
ex
lenWaa19 being
even Element of
NAT st
(
lenWaa19 = lenWaa1 &
len (W .edgeSeq() ) = lenWaa19 div 2 )
by Lm42;
2
* x <= 2
* (len ((W .remove m,n) .edgeSeq() ))
by A57, XREAL_1:66;
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 13;
A72:
2
* (n1div2aa1 + k) = ((2 * x) - m) + n
by A3, A4, A68;
A73:
m <= 2
* x
by A66, NAT_1:13;
then A74:
((2 * x) - m) + n <= len W
by A1, A71, Lm30;
k <> 0
by A67, A68;
then
0 + 1
< k + 1
by XREAL_1:10;
then A76:
1
<= k
by NAT_1:13;
then
n1div2aa1 + 1
<= n1div2aa1 + k
by XREAL_1:9;
then
n1div2aa1 + k in Y
by A75;
then
n1div2aa1 + k in dom es
by A23, XBOOLE_0:def 3;
then A77:
es . (n1div2aa1 + k) = (W .edgeSeq() ) . (n1div2aa1 + k)
by FUNCT_1:70;
then
k in dom (Sgm Y)
by A54, A68, A76, FINSEQ_1:3;
then (Sgm Z) . x =
(Sgm Y) . k
by A45, A69, A68, FINSEQ_1:def 7
.=
n1div2aa1 + k
by A24, A6, A4, A30, A68, A76, A78, GRAPH_2:5
;
then A80:
(Seq es) . x = es . (n1div2aa1 + k)
by A3, A24, A23, A2, A29, A53, A46, A52, A55, FUNCT_1:22;
1
<= n1div2aa1 + k
by A76, NAT_1:12;
then
(Seq es) . x = W . (2 * (n1div2aa1 + k))
by A80, A75, A77, A70, Def15;
hence
((W .remove m,n) .edgeSeq() ) . x9 = (Seq es) . x9
by A1, A58, A73, A71, A72, Lm30;
verum end; hence
((W .remove m,n) .edgeSeq() ) . x9 = (Seq es) . x9
;
verum end; then A81:
(W .remove m,n) .edgeSeq() = Seq es
by A3, A24, A2, A53, A46, A52, FUNCT_1:9;
W is_Walk_from W .first() ,
W .last()
by Def23;
then
W .remove m,
n is_Walk_from W .first() ,
W .last()
by Lm25;
hence
W .remove m,
n is
Subwalk of
W
by A81, Def32;
verum end;
hence
W .remove m,n is Subwalk of W
; verum