set n = (len W) + 1;
defpred S1[ 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 :: thesis: for n being Nat
for x being set ex y being set st S1[n,x,y]
let n be 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 :: thesis: ex y being set st S1[n,x,y]
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
A2: ( dom f = NAT & f . 0 = W & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 1(A1);
 defpred S2[ 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 ) );
now :: thesis: for n being Nat st S2[n] holds
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 ) )
let n be Nat; :: thesis: ( S2[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 S2[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
A3: Wn = f . n and
A4: len Wn <= len W and
A5: 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 A2;
hence f . (n + 1) = Wn1 by A3; :: 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 A4, 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 that
A6: m < (2 * (n + 1)) + 1 and
A7: m <= len Wn1 ; :: thesis: Wn1 .rfind m = m
set W1 = Wn .cut (1,(Wn .find ((2 * n) + 1)));
set W2 = Wn .cut ((Wn .rfind ((2 * n) + 1)),(len Wn));
A8: len Wn1 <= len Wn by Lm26;
then A9: m <= len Wn by A7, XXREAL_0:2;
m <= 2 * (n + 1) by A6, NAT_1:13;
then m < ((2 * n) + 1) + 1 by XXREAL_0:1;
then A10: m <= (2 * n) + 1 by NAT_1:13;
now :: thesis: Wn1 .rfind m = m
per cases ( (2 * n) + 1 <= len Wn or len Wn < (2 * n) + 1 ) ;
suppose A11: (2 * n) + 1 <= len Wn ; :: thesis: Wn1 .rfind m = m
then A12: Wn .find ((2 * n) + 1) <= (2 * n) + 1 by Lm49;
A13: Wn . (Wn .find ((2 * n) + 1)) = Wn . ((2 * n) + 1) by A11, Def20;
A14: Wn .find ((2 * n) + 1) <= len Wn by A11, Def20;
A15: now :: thesis: not Wn .find ((2 * n) + 1) < (2 * n) + 1
assume A16: Wn .find ((2 * n) + 1) < (2 * n) + 1 ; :: thesis: contradiction
then Wn .find ((2 * n) + 1) <= len Wn by A11, XXREAL_0:2;
then Wn .rfind (Wn .find ((2 * n) + 1)) = Wn .find ((2 * n) + 1) by A5, A16;
hence contradiction by A11, A14, A13, A16, Def22; :: thesis: verum
end;
then A17: Wn .find ((2 * n) + 1) = (2 * n) + 1 by A12, XXREAL_0:1;
A18: Wn . (Wn .rfind ((2 * n) + 1)) = Wn . ((2 * n) + 1) by A11, Def22;
set m9 = Wn1 .rfind m;
A19: 1 <= m by ABIAN:12;
A20: Wn1 . (Wn1 .rfind m) = Wn1 . m by A7, Def22;
A21: Wn1 .rfind m >= m by A7, Lm50;
A22: Wn .rfind ((2 * n) + 1) <= len Wn by A11, Def22;
1 <= Wn .find ((2 * n) + 1) by ABIAN:12;
then A23: (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .last() = Wn . ((2 * n) + 1) by A14, A13, Lm16, JORDAN12:2
.= (Wn .cut ((Wn .rfind ((2 * n) + 1)),(len Wn))) .first() by A22, A18, Lm16 ;
(2 * n) + 1 <= Wn .rfind ((2 * n) + 1) by A11, Lm50;
then A24: Wn .find ((2 * n) + 1) <= Wn .rfind ((2 * n) + 1) by A12, XXREAL_0:2;
then A25: Wn1 = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .append (Wn .cut ((Wn .rfind ((2 * n) + 1)),(len Wn))) by A13, A22, A18, Def12;
A26: Wn1 .rfind m <= len Wn1 by A7, Def22;
then A27: Wn1 .rfind m <= len Wn by A8, XXREAL_0:2;
now :: thesis: Wn1 .rfind m = m
per cases ( m < (2 * n) + 1 or m = (2 * n) + 1 ) by A10, XXREAL_0:1;
suppose A28: m < (2 * n) + 1 ; :: thesis: Wn1 .rfind m = m
then m < len (Wn .cut (1,(Wn .find ((2 * n) + 1)))) by A11, A17, Lm22;
then A29: Wn1 .cut (1,m) = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .cut (1,m) by A25, A19, A23, Lm21, JORDAN12:2
.= Wn .cut (1,m) by A10, A17, Lm20 ;
reconsider maa1 = m - 1 as Element of NAT by ABIAN:12, INT_1:5;
A30: maa1 + 1 = m ;
A31: maa1 < m - 0 by XREAL_1:15;
then A32: maa1 < len (Wn .cut (1,m)) by A7, A8, Lm22, XXREAL_0:2;
maa1 < len (Wn1 .cut (1,m)) by A7, A31, Lm22;
then Wn1 . m = (Wn .cut (1,m)) . m by A7, A19, A29, A30, Lm15, JORDAN12:2;
then A33: Wn1 . m = Wn . m by A9, A19, A30, A32, Lm15, JORDAN12:2;
A34: Wn .rfind m = m by A5, A9, A28;
now :: thesis: Wn1 .rfind m = m
per cases ( Wn1 .rfind m < Wn .find ((2 * n) + 1) or Wn .find ((2 * n) + 1) <= Wn1 .rfind m ) ;
suppose A35: Wn1 .rfind m < Wn .find ((2 * n) + 1) ; :: thesis: Wn1 .rfind m = m
reconsider m9aa1 = (Wn1 .rfind m) - 1 as Element of NAT by ABIAN:12, INT_1:5;
A36: 1 <= Wn1 .rfind m by ABIAN:12;
A37: m9aa1 < (Wn1 .rfind m) - 0 by XREAL_1:15;
then A38: m9aa1 < len (Wn1 .cut (1,(Wn1 .rfind m))) by A26, Lm22;
A39: m9aa1 < len (Wn .cut (1,(Wn1 .rfind m))) by A8, A26, A37, Lm22, XXREAL_0:2;
Wn1 .rfind m < len (Wn .cut (1,(Wn .find ((2 * n) + 1)))) by A14, A35, Lm22;
then Wn1 .cut (1,(Wn1 .rfind m)) = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .cut (1,(Wn1 .rfind m)) by A25, A23, A36, Lm21, JORDAN12:2
.= Wn .cut (1,(Wn1 .rfind m)) by A35, Lm20 ;
then Wn1 . (Wn1 .rfind m) = (Wn .cut (1,(Wn1 .rfind m))) . (m9aa1 + 1) by A26, A36, A38, Lm15, JORDAN12:2;
then Wn . (Wn1 .rfind m) = Wn . m by A20, A27, A33, A36, A39, Lm15, JORDAN12:2;
then Wn1 .rfind m <= m by A9, A27, A34, Def22;
hence Wn1 .rfind m = m by A21, XXREAL_0:1; :: thesis: verum
end;
suppose A40: 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));
A41: Wn1 . (Wn1 .rfind m) = Wn . (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) by A13, A22, A18, A24, A26, A40, Lm30;
A42: ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= len Wn by A13, A22, A18, A24, A26, A40, Lm30;
(Wn1 .rfind m) + (Wn .find ((2 * n) + 1)) <= (Wn1 .rfind m) + (Wn .rfind ((2 * n) + 1)) by A24, XREAL_1:7;
then A43: ((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:13;
reconsider x = ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) as Element of NAT by A13, A22, A18, A24, A26, A40, Lm30;
x <= m by A9, A20, A34, A33, A41, A42, Def22;
then Wn1 .rfind m <= m by A43, 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 A44: m = (2 * n) + 1 ; :: thesis: Wn1 .rfind m = m
then m <= len (Wn .cut (1,(Wn .find ((2 * n) + 1)))) by A11, A17, Lm22;
then A45: Wn1 .cut (1,m) = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .cut (1,m) by A25, A19, A23, Lm21, JORDAN12:2
.= Wn .cut (1,m) by A10, A17, Lm20 ;
reconsider maa1 = m - 1 as Element of NAT by ABIAN:12, INT_1:5;
A46: maa1 + 1 = m ;
A47: maa1 < m - 0 by XREAL_1:15;
then A48: maa1 < len (Wn .cut (1,m)) by A7, A8, Lm22, XXREAL_0:2;
maa1 < len (Wn1 .cut (1,m)) by A7, A47, Lm22;
then Wn1 . m = (Wn .cut (1,m)) . m by A7, A19, A45, A46, Lm15, JORDAN12:2;
then A49: Wn1 . m = Wn . m by A9, A19, A46, A48, Lm15, JORDAN12:2;
now :: thesis: not m < Wn1 .rfind m
set x = ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1));
assume A50: m < Wn1 .rfind m ; :: thesis: contradiction
then A51: Wn .find ((2 * n) + 1) < Wn1 .rfind m by A12, A15, A44, XXREAL_0:1;
then A52: ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) is Element of NAT by A13, A22, A18, A24, A26, Lm30;
A53: ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= len Wn by A13, A22, A18, A24, A26, A51, Lm30;
Wn1 . (Wn1 .rfind m) = Wn . (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) by A13, A22, A18, A24, A26, A51, Lm30;
then ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= Wn .rfind ((2 * n) + 1) by A11, A20, A44, A49, A52, A53, 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:13;
then ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .find ((2 * n) + 1)) <= 0 + (Wn .find ((2 * n) + 1)) by XREAL_1:7;
hence contradiction by A12, A15, A44, A50, 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 A54: len Wn < (2 * n) + 1 ; :: thesis: Wn1 .rfind m = m
then A55: m < (2 * n) + 1 by A9, XXREAL_0:2;
A56: Wn .rfind ((2 * n) + 1) = len Wn by A54, Def22;
Wn .find ((2 * n) + 1) = len Wn by A54, Def20;
then Wn1 = Wn by A56, Lm27;
hence Wn1 .rfind m = m by A5, A7, A55; :: thesis: verum
end;
end;
end;
hence Wn1 .rfind m = m ; :: thesis: verum
end;
then A57: for n being Nat st S2[n] holds
S2[n + 1] ;
reconsider W0 = f . 0 as Subwalk of W by A2, Lm70;
for m being odd Element of NAT st m < (2 * 0) + 1 & m <= len W0 holds
W0 .rfind m = m by ABIAN:12;
then A58: S2[ 0 ] by A2;
for n being Nat holds S2[n] from NAT_1:sch 2(A58, A57);
 then consider P being Subwalk of W such that
P = f . ((len W) + 1) and
A59: len P <= len W and
A60: for m being odd Element of NAT st m < (2 * ((len W) + 1)) + 1 & m <= len P holds
P .rfind m = m ;
take P ; :: thesis: ( P is Trail-like & P is Path-like )
now :: thesis: for m being odd Element of NAT st m <= len P holds
P .rfind m = m
let m be odd Element of NAT ; :: thesis: ( m <= len P implies P .rfind m = m )
assume A61: m <= len P ; :: thesis: P .rfind m = m
(len P) + 0 < (len W) + 1 by A59, XREAL_1:8;
then (len P) + 0 < ((len W) + 1) + ((len W) + 1) by XREAL_1:8;
then (len P) + 0 < (2 * ((len W) + 1)) + 1 by XREAL_1:8;
then m < (2 * ((len W) + 1)) + 1 by A61, XXREAL_0:2;
hence P .rfind m = m by A60, A61; :: thesis: verum
end;
then P is Path-like by Lm67;
hence ( P is Trail-like & P is Path-like ) ; :: thesis: verum