hereby :: thesis: ( ( ( m is even or n is even or not m <= n or not n <= len W ) implies W is Walk of G ) & ( for b1 being Walk of G holds verum ) )
assume A1:
( not
m is
even & not
n is
even &
m <= n &
n <= len W )
;
:: thesis: m,n -cut W is Walk of Gthen reconsider m4 =
m,
n4 =
n as
odd Nat ;
set W2 =
m,
n -cut W;
set VG =
the_Vertices_of G;
A2:
( 1
<= m &
m <= n &
n <= len W )
by A1, HEYTING3:1;
then
((len (m,n -cut W)) + m4) - m4 = (n4 + 1) - m4
by GRAPH_2:def 1;
then reconsider lenW2 =
len (m,n -cut W) as
odd Element of
NAT ;
now
not
lenW2 is
even
;
hence
not
len (m,n -cut W) is
even
;
:: thesis: ( (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 HEYTING3:1, INT_1:18;
0 < lenW2aa1 + 1
;
then A3:
(m,n -cut W) . (0 + 1) = W . (m + 0 )
by A2, GRAPH_2:def 1;
( 1
<= m &
m <= len W )
by A1, HEYTING3:1, XXREAL_0:2;
then
W . m = W .vertexAt m
by A1, Def8;
hence
(m,n -cut W) . 1
in the_Vertices_of G
by A3;
:: thesis: 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 ;
:: thesis: ( 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 )assume A4:
i < len (m,n -cut W)
;
:: thesis: (m,n -cut W) . (i + 1) Joins (m,n -cut W) . i,(m,n -cut W) . (i + 2),Gthen
i + m < (len (m,n -cut W)) + m
by XREAL_1:10;
then
i + m < n + 1
by A2, GRAPH_2:def 1;
then
i + m4 <= n4
by NAT_1:13;
then
m4 + i < n4
by XXREAL_0:1;
then A5:
m + i < len W
by A1, XXREAL_0:2;
reconsider iaa1 =
i - 1 as
even Element of
NAT by HEYTING3:1, INT_1:18;
iaa1 < (len (m,n -cut W)) - 0
by A4, XREAL_1:16;
then A6:
(m,n -cut W) . (iaa1 + 1) = W . (m + iaa1)
by A2, GRAPH_2:def 1;
i + 1
<= lenW2
by A4, NAT_1:13;
then
i + 1
< len (m,n -cut W)
by XXREAL_0:1;
then A7:
(m,n -cut W) . ((i + 1) + 1) = W . (m + (i + 1))
by A2, GRAPH_2:def 1;
reconsider x =
(m4 + i) - 1 as
odd Element of
NAT by A2, INT_1:18, NAT_1:12;
(m + i) - 1
< (len W) - 0
by A5, XREAL_1:16;
then
W . (x + 1) Joins W . x,
W . (x + 2),
G
by Def3;
hence
(m,n -cut W) . (i + 1) Joins (m,n -cut W) . i,
(m,n -cut W) . (i + 2),
G
by A2, A4, A6, A7, GRAPH_2:def 1;
:: thesis: verum hence
m,
n -cut W is
Walk of
G
by Def3;
:: thesis: verum
end;
thus
( ( ( m is even or n is even or not m <= n or not n <= len W ) implies W is Walk of G ) & ( for b1 being Walk of G holds verum ) )
; :: thesis: verum