let G be _Graph; :: thesis: for W being Walk of G

for e, v being object st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ) holds

W .addEdge e is Path-like

let W be Walk of G; :: thesis: for e, v being object st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ) holds

W .addEdge e is Path-like

let e, v be object ; :: thesis: ( W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ) implies W .addEdge e is Path-like )

assume that

A1: W is Path-like and

A2: e Joins W .last() ,v,G and

A3: not e in W .edges() and

A4: ( W is trivial or W is open ) and

A5: for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ; :: thesis: W .addEdge e is Path-like

reconsider lenW = len W as odd Element of NAT ;

set W2 = W .addEdge e;

A6: e in (W .last()) .edgesInOut() by A2, GLIB_000:62;

for e, v being object st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ) holds

W .addEdge e is Path-like

let W be Walk of G; :: thesis: for e, v being object st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ) holds

W .addEdge e is Path-like

let e, v be object ; :: thesis: ( W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ) implies W .addEdge e is Path-like )

assume that

A1: W is Path-like and

A2: e Joins W .last() ,v,G and

A3: not e in W .edges() and

A4: ( W is trivial or W is open ) and

A5: for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ; :: thesis: W .addEdge e is Path-like

reconsider lenW = len W as odd Element of NAT ;

set W2 = W .addEdge e;

A6: e in (W .last()) .edgesInOut() by A2, GLIB_000:62;

now :: thesis: ( W .addEdge e is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds

( m = 1 & n = len (W .addEdge e) ) ) )

hence
W .addEdge e is Path-like
; :: thesis: verum( m = 1 & n = len (W .addEdge e) ) ) )

W is Trail-like
by A1;

hence W .addEdge e is Trail-like by A3, A6, Lm60; :: thesis: for m, n being odd Element of NAT st m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds

( m = 1 & n = len (W .addEdge e) )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )

assume that

A7: m < n and

A8: n <= len (W .addEdge e) and

A9: (W .addEdge e) . m = (W .addEdge e) . n ; :: thesis: ( m = 1 & n = len (W .addEdge e) )

end;hence W .addEdge e is Trail-like by A3, A6, Lm60; :: thesis: for m, n being odd Element of NAT st m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds

( m = 1 & n = len (W .addEdge e) )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )

assume that

A7: m < n and

A8: n <= len (W .addEdge e) and

A9: (W .addEdge e) . m = (W .addEdge e) . n ; :: thesis: ( m = 1 & n = len (W .addEdge e) )

now :: thesis: ( m = 1 & n = len (W .addEdge e) )end;

hence
( m = 1 & n = len (W .addEdge e) )
; :: thesis: verumper cases
( W is open or W is trivial )
by A4;

end;

suppose A10:
W is open
; :: thesis: ( m = 1 & n = len (W .addEdge e) )

end;

now :: thesis: ( m = 1 & n = len (W .addEdge e) )end;

hence
( m = 1 & n = len (W .addEdge e) )
; :: thesis: verumper cases
( n <= len W or n > len W )
;

end;

suppose A11:
n <= len W
; :: thesis: ( m = 1 & n = len (W .addEdge e) )

A12:
1 <= m
by ABIAN:12;

m <= len W by A7, A11, XXREAL_0:2;

then m in dom W by A12, FINSEQ_3:25;

then A13: (W .addEdge e) . m = W . m by A2, Lm38;

1 <= n by ABIAN:12;

then n in dom W by A11, FINSEQ_3:25;

then A14: W . m = W . n by A2, A9, A13, Lm38;

then m = 1 by A1, A7, A11;

then W .first() = W .last() by A1, A7, A11, A14;

hence ( m = 1 & n = len (W .addEdge e) ) by A10; :: thesis: verum

end;m <= len W by A7, A11, XXREAL_0:2;

then m in dom W by A12, FINSEQ_3:25;

then A13: (W .addEdge e) . m = W . m by A2, Lm38;

1 <= n by ABIAN:12;

then n in dom W by A11, FINSEQ_3:25;

then A14: W . m = W . n by A2, A9, A13, Lm38;

then m = 1 by A1, A7, A11;

then W .first() = W .last() by A1, A7, A11, A14;

hence ( m = 1 & n = len (W .addEdge e) ) by A10; :: thesis: verum

suppose
n > len W
; :: thesis: ( m = 1 & n = len (W .addEdge e) )

then
lenW + 1 <= n
by NAT_1:13;

then lenW + 1 < n by XXREAL_0:1;

then (lenW + 1) + 1 <= n by NAT_1:13;

then (len W) + (1 + 1) <= n ;

then A15: len (W .addEdge e) <= n by A2, Lm37;

then n = len (W .addEdge e) by A8, XXREAL_0:1;

then (W .addEdge e) . n = (W .addEdge e) . ((len W) + 2) by A2, Lm37;

then A16: (W .addEdge e) . n = v by A2, Lm38;

m < len (W .addEdge e) by A7, A8, A15, XXREAL_0:1;

then m < (len W) + (1 + 1) by A2, Lm37;

then m < ((len W) + 1) + 1 ;

then m <= lenW + 1 by NAT_1:13;

then m < lenW + 1 by XXREAL_0:1;

then A17: m <= len W by NAT_1:13;

1 <= m by ABIAN:12;

then m in dom W by A17, FINSEQ_3:25;

then A18: W . m = v by A2, A9, A16, Lm38;

thus n = len (W .addEdge e) by A8, A15, XXREAL_0:1; :: thesis: verum

end;then lenW + 1 < n by XXREAL_0:1;

then (lenW + 1) + 1 <= n by NAT_1:13;

then (len W) + (1 + 1) <= n ;

then A15: len (W .addEdge e) <= n by A2, Lm37;

then n = len (W .addEdge e) by A8, XXREAL_0:1;

then (W .addEdge e) . n = (W .addEdge e) . ((len W) + 2) by A2, Lm37;

then A16: (W .addEdge e) . n = v by A2, Lm38;

m < len (W .addEdge e) by A7, A8, A15, XXREAL_0:1;

then m < (len W) + (1 + 1) by A2, Lm37;

then m < ((len W) + 1) + 1 ;

then m <= lenW + 1 by NAT_1:13;

then m < lenW + 1 by XXREAL_0:1;

then A17: m <= len W by NAT_1:13;

1 <= m by ABIAN:12;

then m in dom W by A17, FINSEQ_3:25;

then A18: W . m = v by A2, A9, A16, Lm38;

now :: thesis: not m <> 1

hence
m = 1
; :: thesis: n = len (W .addEdge e)A19:
1 <= m
by ABIAN:12;

assume m <> 1 ; :: thesis: contradiction

then 1 < m by A19, XXREAL_0:1;

hence contradiction by A5, A17, A18; :: thesis: verum

end;assume m <> 1 ; :: thesis: contradiction

then 1 < m by A19, XXREAL_0:1;

hence contradiction by A5, A17, A18; :: thesis: verum

thus n = len (W .addEdge e) by A8, A15, XXREAL_0:1; :: thesis: verum

suppose
W is trivial
; :: thesis: ( m = 1 & n = len (W .addEdge e) )

then
ex v being Vertex of G st W = G .walkOf v
by Lm56;

then len W = 1 by FINSEQ_1:39;

then A20: len (W .addEdge e) = 1 + 2 by A2, Lm37;

A21: m + 1 <= n by A7, NAT_1:13;

A22: 1 <= m by ABIAN:12;

then 1 + 1 <= m + 1 by XREAL_1:7;

then 2 * 1 <= n by A21, XXREAL_0:2;

then 2 * 1 < n by XXREAL_0:1;

then A23: len (W .addEdge e) <= n by A20, NAT_1:13;

then n = len (W .addEdge e) by A8, XXREAL_0:1;

then (m + 1) - 1 <= 3 - 1 by A7, A20, NAT_1:13;

then m < 2 * 1 by XXREAL_0:1;

then m + 1 <= 2 by NAT_1:13;

then (m + 1) - 1 <= 2 - 1 by XREAL_1:13;

hence ( m = 1 & n = len (W .addEdge e) ) by A8, A22, A23, XXREAL_0:1; :: thesis: verum

end;then len W = 1 by FINSEQ_1:39;

then A20: len (W .addEdge e) = 1 + 2 by A2, Lm37;

A21: m + 1 <= n by A7, NAT_1:13;

A22: 1 <= m by ABIAN:12;

then 1 + 1 <= m + 1 by XREAL_1:7;

then 2 * 1 <= n by A21, XXREAL_0:2;

then 2 * 1 < n by XXREAL_0:1;

then A23: len (W .addEdge e) <= n by A20, NAT_1:13;

then n = len (W .addEdge e) by A8, XXREAL_0:1;

then (m + 1) - 1 <= 3 - 1 by A7, A20, NAT_1:13;

then m < 2 * 1 by XXREAL_0:1;

then m + 1 <= 2 by NAT_1:13;

then (m + 1) - 1 <= 2 - 1 by XREAL_1:13;

hence ( m = 1 & n = len (W .addEdge e) ) by A8, A22, A23, XXREAL_0:1; :: thesis: verum