defpred S1[ Element of NAT , set , set ] means ( ( W is Walk of G & ex Wn being Walk of G st
( Wn = W & c3 = Wn .remove (Wn .find ((2 * G) + 1)),(Wn .rfind ((2 * G) + 1)) ) ) or ( W is not Walk of G & c3 = W ) );
A1: now
let n be Element of NAT ; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
now
per cases ( x is Walk of G or not x is Walk of G ) ;
suppose x is Walk of G ; :: thesis: ex y being set st S1[n,x,y]
then reconsider W = x as Walk of G ;
set y = W .remove (W .find ((2 * n) + 1)),(W .rfind ((2 * n) + 1));
S1[n,x,W .remove (W .find ((2 * n) + 1)),(W .rfind ((2 * n) + 1))] ;
hence ex y being set st S1[n,x,y] ; :: thesis: verum
end;
suppose x is not Walk of G ; :: thesis: ex y being set st S1[n,x,y]
hence ex y being set st S1[n,x,y] ; :: thesis: verum
end;
end;
end;
hence ex y being set st S1[n,x,y] ; :: thesis: verum
end;
consider f being Function such that
A3: ( dom f = NAT & f . 0 = W & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 1(A1);
 defpred S2[ Element of NAT ] means f . G is Subwalk of W;
reconsider W0 = f . 0 as Subwalk of W by A3, Lm70;
defpred S3[ Element of NAT ] means ex Wn being Subwalk of W st
( Wn = f . G & len Wn <= len W & ( for m being odd Element of NAT st m < (2 * G) + 1 & m <= len Wn holds
Wn .rfind m = m ) );
for m being odd Element of NAT st m < (2 * 0 ) + 1 & m <= len W0 holds
W0 .rfind m = m by HEYTING3:1;
then A4: S3[ 0 ] by A3;
now
let n be Element of NAT ; :: thesis: ( S3[n] implies ex Wn1 being Subwalk of W st
( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds
Wn1 .rfind m = m ) ) )
assume S3[n] ; :: thesis: ex Wn1 being Subwalk of W st
( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds
Wn1 .rfind m = m ) )
then consider Wn being Subwalk of W such that
A5: ( Wn = f . n & len Wn <= len W & ( for m being odd Element of NAT st m < (2 * n) + 1 & m <= len Wn holds
Wn .rfind m = m ) ) ;
set a = Wn .find ((2 * n) + 1);
set b = Wn .rfind ((2 * n) + 1);
set Wn1 = Wn .remove (Wn .find ((2 * n) + 1)),(Wn .rfind ((2 * n) + 1));
reconsider Wn1 = Wn .remove (Wn .find ((2 * n) + 1)),(Wn .rfind ((2 * n) + 1)) as Subwalk of W by Lm71;
take Wn1 = Wn1; :: thesis: ( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds
Wn1 .rfind m = m ) )
S1[n,f . n,f . (n + 1)] by A3;
hence f . (n + 1) = Wn1 by A5; :: thesis: ( len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds
Wn1 .rfind m = m ) )
len Wn1 <= len Wn by Lm26;
hence len Wn1 <= len W by A5, XXREAL_0:2; :: thesis: for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds
Wn1 .rfind m = m
let m be odd Element of NAT ; :: thesis: ( m < (2 * (n + 1)) + 1 & m <= len Wn1 implies Wn1 .rfind m = m )
assume A6: ( m < (2 * (n + 1)) + 1 & m <= len Wn1 ) ; :: thesis: Wn1 .rfind m = m
then m <= 2 * (n + 1) by NAT_1:13;
then m < ((2 * n) + 1) + 1 by XXREAL_0:1;
then A7: m <= (2 * n) + 1 by NAT_1:13;
A8: len Wn1 <= len Wn by Lm26;
then A9: m <= len Wn by A6, XXREAL_0:2;
set W1 = Wn .cut 1,(Wn .find ((2 * n) + 1));
set W2 = Wn .cut (Wn .rfind ((2 * n) + 1)),(len Wn);
now
per cases ( (2 * n) + 1 <= len Wn or len Wn < (2 * n) + 1 ) ;
suppose A10: (2 * n) + 1 <= len Wn ; :: thesis: Wn1 .rfind m = m
then A11: ( Wn .find ((2 * n) + 1) <= len Wn & Wn . (Wn .find ((2 * n) + 1)) = Wn . ((2 * n) + 1) & ( for k being odd Element of NAT st k <= len Wn & Wn . k = Wn . ((2 * n) + 1) holds
Wn .find ((2 * n) + 1) <= k ) ) by Def20;
A12: ( Wn .rfind ((2 * n) + 1) <= len Wn & Wn . (Wn .rfind ((2 * n) + 1)) = Wn . ((2 * n) + 1) & ( for k being odd Element of NAT st k <= len Wn & Wn . k = Wn . ((2 * n) + 1) holds
k <= Wn .rfind ((2 * n) + 1) ) ) by A10, Def22;
A13: ( Wn .find ((2 * n) + 1) <= (2 * n) + 1 & (2 * n) + 1 <= Wn .rfind ((2 * n) + 1) ) by A10, Lm49, Lm50;
then A14: Wn .find ((2 * n) + 1) <= Wn .rfind ((2 * n) + 1) by XXREAL_0:2;
then A15: Wn1 = (Wn .cut 1,(Wn .find ((2 * n) + 1))) .append (Wn .cut (Wn .rfind ((2 * n) + 1)),(len Wn)) by A11, A12, Def12;
A16: now
assume A17: Wn .find ((2 * n) + 1) < (2 * n) + 1 ; :: thesis: contradiction
then Wn .find ((2 * n) + 1) <= len Wn by A10, XXREAL_0:2;
then Wn .rfind (Wn .find ((2 * n) + 1)) = Wn .find ((2 * n) + 1) by A5, A17;
hence contradiction by A10, A11, A17, Def22; :: thesis: verum
end;
then A18: Wn .find ((2 * n) + 1) = (2 * n) + 1 by A13, XXREAL_0:1;
A19: ( not 1 is even & 1 <= Wn .find ((2 * n) + 1) & 1 <= m ) by HEYTING3:1, JORDAN12:3;
then A20: (Wn .cut 1,(Wn .find ((2 * n) + 1))) .last() = Wn . ((2 * n) + 1) by A11, Lm16
.= (Wn .cut (Wn .rfind ((2 * n) + 1)),(len Wn)) .first() by A12, Lm16 ;
set m' = Wn1 .rfind m;
A21: Wn1 .rfind m >= m by A6, Lm50;
A22: ( Wn1 .rfind m <= len Wn1 & Wn1 . (Wn1 .rfind m) = Wn1 . m & ( for k being odd Element of NAT st k <= len Wn1 & Wn1 . k = Wn1 . m holds
k <= Wn1 .rfind m ) ) by A6, Def22;
then A23: Wn1 .rfind m <= len Wn by A8, XXREAL_0:2;
now
per cases ( m < (2 * n) + 1 or m = (2 * n) + 1 ) by A7, XXREAL_0:1;
suppose A24: m < (2 * n) + 1 ; :: thesis: Wn1 .rfind m = m
then A25: Wn .rfind m = m by A5, A9;
m < len (Wn .cut 1,(Wn .find ((2 * n) + 1))) by A10, A18, A24, Lm22;
then A26: Wn1 .cut 1,m = (Wn .cut 1,(Wn .find ((2 * n) + 1))) .cut 1,m by A15, A19, A20, Lm21
.= Wn .cut 1,m by A7, A18, Lm20 ;
reconsider maa1 = m - 1 as Element of NAT by HEYTING3:1, INT_1:18;
A27: maa1 + 1 = m ;
A28: maa1 < m - 0 by XREAL_1:17;
then maa1 < len (Wn1 .cut 1,m) by A6, Lm22;
then A29: Wn1 . m = (Wn .cut 1,m) . m by A6, A19, A26, A27, Lm15;
maa1 < len (Wn .cut 1,m) by A6, A8, A28, Lm22, XXREAL_0:2;
then A30: Wn1 . m = Wn . m by A9, A19, A27, A29, Lm15;
now
per cases ( Wn1 .rfind m < Wn .find ((2 * n) + 1) or Wn .find ((2 * n) + 1) <= Wn1 .rfind m ) ;
suppose A31: Wn1 .rfind m < Wn .find ((2 * n) + 1) ; :: thesis: Wn1 .rfind m = m
then A32: Wn1 .rfind m < len (Wn .cut 1,(Wn .find ((2 * n) + 1))) by A11, Lm22;
A33: 1 <= Wn1 .rfind m by HEYTING3:1;
then A34: Wn1 .cut 1,(Wn1 .rfind m) = (Wn .cut 1,(Wn .find ((2 * n) + 1))) .cut 1,(Wn1 .rfind m) by A15, A20, A32, Lm21, JORDAN12:3
.= Wn .cut 1,(Wn1 .rfind m) by A31, Lm20 ;
reconsider m'aa1 = (Wn1 .rfind m) - 1 as Element of NAT by HEYTING3:1, INT_1:18;
A35: m'aa1 < (Wn1 .rfind m) - 0 by XREAL_1:17;
then m'aa1 < len (Wn1 .cut 1,(Wn1 .rfind m)) by A22, Lm22;
then A36: Wn1 . (Wn1 .rfind m) = (Wn .cut 1,(Wn1 .rfind m)) . (m'aa1 + 1) by A22, A33, A34, Lm15, JORDAN12:3;
m'aa1 < len (Wn .cut 1,(Wn1 .rfind m)) by A23, A35, Lm22;
then Wn . (Wn1 .rfind m) = Wn . m by A22, A23, A30, A33, A36, Lm15, JORDAN12:3;
then Wn1 .rfind m <= m by A9, A23, A25, Def22;
hence Wn1 .rfind m = m by A21, XXREAL_0:1; :: thesis: verum
end;
suppose A37: Wn .find ((2 * n) + 1) <= Wn1 .rfind m ; :: thesis: Wn1 .rfind m = m
set x = ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1));
A38: ( Wn1 . (Wn1 .rfind m) = Wn . (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) & ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) is Element of NAT & ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= len Wn ) by A11, A12, A14, A22, A37, Lm30;
reconsider x = ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) as Element of NAT by A11, A12, A14, A22, A37, Lm30;
A39: x <= m by A9, A22, A25, A30, A38, Def22;
(Wn1 .rfind m) + (Wn .find ((2 * n) + 1)) <= (Wn1 .rfind m) + (Wn .rfind ((2 * n) + 1)) by A14, XREAL_1:9;
then ((Wn1 .rfind m) + (Wn .find ((2 * n) + 1))) - (Wn .find ((2 * n) + 1)) <= ((Wn1 .rfind m) + (Wn .rfind ((2 * n) + 1))) - (Wn .find ((2 * n) + 1)) by XREAL_1:15;
then Wn1 .rfind m <= m by A39, XXREAL_0:2;
hence Wn1 .rfind m = m by A21, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence Wn1 .rfind m = m ; :: thesis: verum
end;
suppose A40: m = (2 * n) + 1 ; :: thesis: Wn1 .rfind m = m
then m <= len (Wn .cut 1,(Wn .find ((2 * n) + 1))) by A10, A18, Lm22;
then A41: Wn1 .cut 1,m = (Wn .cut 1,(Wn .find ((2 * n) + 1))) .cut 1,m by A15, A19, A20, Lm21
.= Wn .cut 1,m by A7, A18, Lm20 ;
reconsider maa1 = m - 1 as Element of NAT by HEYTING3:1, INT_1:18;
A42: maa1 + 1 = m ;
A43: maa1 < m - 0 by XREAL_1:17;
then maa1 < len (Wn1 .cut 1,m) by A6, Lm22;
then A44: Wn1 . m = (Wn .cut 1,m) . m by A6, A19, A41, A42, Lm15;
maa1 < len (Wn .cut 1,m) by A6, A8, A43, Lm22, XXREAL_0:2;
then A45: Wn1 . m = Wn . m by A9, A19, A42, A44, Lm15;
now
assume A46: m < Wn1 .rfind m ; :: thesis: contradiction
then A47: Wn .find ((2 * n) + 1) < Wn1 .rfind m by A13, A16, A40, XXREAL_0:1;
set x = ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1));
( Wn1 . (Wn1 .rfind m) = Wn . (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) & ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) is Element of NAT & ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= len Wn ) by A11, A12, A14, A22, A47, Lm30;
then ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= Wn .rfind ((2 * n) + 1) by A10, A22, A40, A45, Def22;
then (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) - (Wn .rfind ((2 * n) + 1)) <= (Wn .rfind ((2 * n) + 1)) - (Wn .rfind ((2 * n) + 1)) by XREAL_1:15;
then ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .find ((2 * n) + 1)) <= 0 + (Wn .find ((2 * n) + 1)) by XREAL_1:9;
hence contradiction by A13, A16, A40, A46, XXREAL_0:1; :: thesis: verum
end;
hence Wn1 .rfind m = m by A21, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence Wn1 .rfind m = m ; :: thesis: verum
end;
suppose A48: len Wn < (2 * n) + 1 ; :: thesis: Wn1 .rfind m = m
then ( Wn .find ((2 * n) + 1) = len Wn & Wn .rfind ((2 * n) + 1) = len Wn ) by Def20, Def22;
then A49: Wn1 = Wn by Lm27;
m < (2 * n) + 1 by A9, A48, XXREAL_0:2;
hence Wn1 .rfind m = m by A5, A6, A49; :: thesis: verum
end;
end;
end;
hence Wn1 .rfind m = m ; :: thesis: verum
end;
then A50: for n being Element of NAT st S3[n] holds
S3[n + 1] ;
A51: for n being Element of NAT holds S3[n] from NAT_1:sch 1(A4, A50);
 set n = (len W) + 1;
consider P being Subwalk of W such that
A52: ( P = f . ((len W) + 1) & len P <= len W & ( for m being odd Element of NAT st m < (2 * ((len W) + 1)) + 1 & m <= len P holds
P .rfind m = m ) ) by A51;
take P ; :: thesis: ( P is Trail-like & P is Path-like )
now
let m be odd Element of NAT ; :: thesis: ( m <= len P implies P .rfind m = m )
assume A53: m <= len P ; :: thesis: P .rfind m = m
(len P) + 0 < (len W) + 1 by A52, XREAL_1:10;
then (len P) + 0 < ((len W) + 1) + ((len W) + 1) by XREAL_1:10;
then (len P) + 0 < (2 * ((len W) + 1)) + 1 by XREAL_1:10;
then m < (2 * ((len W) + 1)) + 1 by A53, XXREAL_0:2;
hence P .rfind m = m by A52, A53; :: thesis: verum
end;
then P is Path-like by Lm67;
hence ( P is Trail-like & P is Path-like ) ; :: thesis: verum