let G be _Graph; for W being Walk of G
for m, n being Element of NAT st W is Path-like holds
W .cut (m,n) is Path-like
let W be Walk of G; for m, n being Element of NAT st W is Path-like holds
W .cut (m,n) is Path-like
let m, n be Element of NAT ; ( W is Path-like implies W .cut (m,n) is Path-like )
assume A1:
W is Path-like
; W .cut (m,n) is Path-like
now W .cut (m,n) is Path-like per cases
( ( m is odd & n is odd & m <= n & n <= len W ) or not m is odd or not n is odd or not m <= n or not n <= len W )
;
suppose A2:
(
m is
odd &
n is
odd &
m <= n &
n <= len W )
;
W .cut (m,n) is Path-like then reconsider m9 =
m as
odd Element of
NAT ;
now ( W .cut (m,n) is Trail-like & ( for x, y being odd Element of NAT st x < y & y <= len (W .cut (m,n)) & (W .cut (m,n)) . x = (W .cut (m,n)) . y holds
( x = 1 & y = len (W .cut (m,n)) ) ) )
W is
Trail-like
by A1;
hence
W .cut (
m,
n) is
Trail-like
by Lm59;
for x, y being odd Element of NAT st x < y & y <= len (W .cut (m,n)) & (W .cut (m,n)) . x = (W .cut (m,n)) . y holds
( x = 1 & y = len (W .cut (m,n)) )let x,
y be
odd Element of
NAT ;
( x < y & y <= len (W .cut (m,n)) & (W .cut (m,n)) . x = (W .cut (m,n)) . y implies ( x = 1 & y = len (W .cut (m,n)) ) )assume that A3:
x < y
and A4:
y <= len (W .cut (m,n))
and A5:
(W .cut (m,n)) . x = (W .cut (m,n)) . y
;
( x = 1 & y = len (W .cut (m,n)) )reconsider xaa1 =
x - 1 as
even Element of
NAT by ABIAN:12, INT_1:5;
reconsider yaa1 =
y - 1 as
even Element of
NAT by ABIAN:12, INT_1:5;
x - 1
< y - 1
by A3, XREAL_1:14;
then A6:
xaa1 + m < yaa1 + m
by XREAL_1:8;
x <= len (W .cut (m,n))
by A3, A4, XXREAL_0:2;
then
x - 1
< (len (W .cut (m,n))) - 0
by XREAL_1:15;
then A7:
(W .cut (m,n)) . (xaa1 + 1) = W . (m + xaa1)
by A2, Lm15;
A8:
y - 1
< (len (W .cut (m,n))) - 0
by A4, XREAL_1:15;
then A9:
(W .cut (m,n)) . (yaa1 + 1) = W . (m + yaa1)
by A2, Lm15;
m + yaa1 in dom W
by A2, A8, Lm15;
then A10:
m9 + yaa1 <= len W
by FINSEQ_3:25;
then A11:
m9 + yaa1 = len W
by A1, A5, A7, A9, A6;
then
(m + 1) - 1
= 1
by A1, A5, A7, A9, A6, A10;
then A14:
(len (W .cut (m,n))) + 1
= n + 1
by A2, Lm15;
thus
x = 1
by A12;
y = len (W .cut (m,n))
m9 + xaa1 = 1
by A1, A5, A7, A9, A6, A10;
hence
y = len (W .cut (m,n))
by A2, A4, A11, A12, A14, XXREAL_0:1;
verum end; hence
W .cut (
m,
n) is
Path-like
;
verum end; end; end;
hence
W .cut (m,n) is Path-like
; verum