hereby ( ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W is Walk of G ) & ( for b1 being Walk of G holds verum ) )
set W2 = (
m,
n)
-cut W;
set VG =
the_Vertices_of G;
assume that A1:
m is
odd
and A2:
n is
odd
and A3:
m <= n
and A4:
n <= len W
;
(m,n) -cut W is Walk of Greconsider m4 =
m,
n4 =
n as
odd Nat by A1, A2;
A5:
1
<= m
by A1, ABIAN:12;
then
((len ((m,n) -cut W)) + m4) - m4 = (n4 + 1) - m4
by A3, A4, FINSEQ_6:def 4;
then reconsider lenW2 =
len ((m,n) -cut W) as
odd Element of
NAT ;
now ( len ((m,n) -cut W) is odd & ((m,n) -cut W) . 1 in the_Vertices_of G & ( for i being odd Element of NAT st i < len ((m,n) -cut W) holds
((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G ) )reconsider lenW2aa1 =
lenW2 - 1 as
Element of
NAT by ABIAN:12, INT_1:5;
lenW2 is
odd
;
hence
len ((m,n) -cut W) is
odd
;
( ((m,n) -cut W) . 1 in the_Vertices_of G & ( for i being odd Element of NAT st i < len ((m,n) -cut W) holds
((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G ) )
0 < lenW2aa1 + 1
;
then A6:
((m,n) -cut W) . (0 + 1) = W . (m + 0)
by A3, A4, A5, FINSEQ_6:def 4;
m <= len W
by A3, A4, XXREAL_0:2;
then
W . m = W .vertexAt m
by A1, Def8;
hence
((m,n) -cut W) . 1
in the_Vertices_of G
by A6;
for i being odd Element of NAT st i < len ((m,n) -cut W) holds
((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),Glet i be
odd Element of
NAT ;
( i < len ((m,n) -cut W) implies ((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G )reconsider x =
(m4 + i) - 1 as
odd Element of
NAT by A5, INT_1:5, NAT_1:12;
reconsider iaa1 =
i - 1 as
even Element of
NAT by ABIAN:12, INT_1:5;
assume A7:
i < len ((m,n) -cut W)
;
((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),Gthen
i + 1
<= lenW2
by NAT_1:13;
then
i + 1
< len ((m,n) -cut W)
by XXREAL_0:1;
then A8:
((m,n) -cut W) . ((i + 1) + 1) = W . (m + (i + 1))
by A3, A4, A5, FINSEQ_6:def 4;
i + m < (len ((m,n) -cut W)) + m
by A7, XREAL_1:8;
then
i + m < n + 1
by A3, A4, A5, FINSEQ_6:def 4;
then
i + m4 <= n4
by NAT_1:13;
then
m4 + i < n4
by XXREAL_0:1;
then
m + i < len W
by A4, XXREAL_0:2;
then
(m + i) - 1
< (len W) - 0
by XREAL_1:14;
then A9:
W . (x + 1) Joins W . x,
W . (x + 2),
G
by Def3;
iaa1 < (len ((m,n) -cut W)) - 0
by A7, XREAL_1:14;
then
((m,n) -cut W) . (iaa1 + 1) = W . (m + iaa1)
by A3, A4, A5, FINSEQ_6:def 4;
hence
((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,
((m,n) -cut W) . (i + 2),
G
by A3, A4, A5, A7, A8, A9, FINSEQ_6:def 4;
verum end; hence
(
m,
n)
-cut W is
Walk of
G
by Def3;
verum
end;
thus
( ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W is Walk of G ) & ( for b1 being Walk of G holds verum ) )
; verum