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

for e being set st W is Trail-like & e in (W .last()) .edgesInOut() & not e in W .edges() holds

W .addEdge e is Trail-like

let W be Walk of G; :: thesis: for e being set st W is Trail-like & e in (W .last()) .edgesInOut() & not e in W .edges() holds

W .addEdge e is Trail-like

let e be set ; :: thesis: ( W is Trail-like & e in (W .last()) .edgesInOut() & not e in W .edges() implies W .addEdge e is Trail-like )

assume that

A1: W is Trail-like and

A2: e in (W .last()) .edgesInOut() and

A3: not e in W .edges() ; :: thesis: W .addEdge e is Trail-like

set W2 = W .addEdge e;

reconsider lenW2 = len (W .addEdge e) as odd Element of NAT ;

A4: e Joins W .last() ,(W .last()) .adj e,G by A2, GLIB_000:67;

for e being set st W is Trail-like & e in (W .last()) .edgesInOut() & not e in W .edges() holds

W .addEdge e is Trail-like

let W be Walk of G; :: thesis: for e being set st W is Trail-like & e in (W .last()) .edgesInOut() & not e in W .edges() holds

W .addEdge e is Trail-like

let e be set ; :: thesis: ( W is Trail-like & e in (W .last()) .edgesInOut() & not e in W .edges() implies W .addEdge e is Trail-like )

assume that

A1: W is Trail-like and

A2: e in (W .last()) .edgesInOut() and

A3: not e in W .edges() ; :: thesis: W .addEdge e is Trail-like

set W2 = W .addEdge e;

reconsider lenW2 = len (W .addEdge e) as odd Element of NAT ;

A4: e Joins W .last() ,(W .last()) .adj e,G by A2, GLIB_000:67;

now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len (W .addEdge e) holds

(W .addEdge e) . m <> (W .addEdge e) . n

hence
W .addEdge e is Trail-like
by Lm57; :: thesis: verum(W .addEdge e) . m <> (W .addEdge e) . n

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

assume that

A5: 1 <= m and

A6: m < n and

A7: n <= len (W .addEdge e) ; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n

end;assume that

A5: 1 <= m and

A6: m < n and

A7: n <= len (W .addEdge e) ; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n

now :: thesis: (W .addEdge e) . m <> (W .addEdge e) . nend;

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

end;

suppose A8:
n <= len W
; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n

then
m <= len W
by A6, XXREAL_0:2;

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

then A9: (W .addEdge e) . m = W . m by A4, Lm38;

1 <= n by A5, A6, XXREAL_0:2;

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

then (W .addEdge e) . n = W . n by A4, Lm38;

hence (W .addEdge e) . m <> (W .addEdge e) . n by A1, A5, A6, A8, A9, Lm57; :: thesis: verum

end;then m in dom W by A5, FINSEQ_3:25;

then A9: (W .addEdge e) . m = W . m by A4, Lm38;

1 <= n by A5, A6, XXREAL_0:2;

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

then (W .addEdge e) . n = W . n by A4, Lm38;

hence (W .addEdge e) . m <> (W .addEdge e) . n by A1, A5, A6, A8, A9, Lm57; :: thesis: verum

suppose A10:
n > len W
; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n

n < lenW2
by A7, XXREAL_0:1;

then n + 1 <= len (W .addEdge e) by NAT_1:13;

then (n + 1) - 1 <= (len (W .addEdge e)) - 1 by XREAL_1:13;

then A11: n <= ((len W) + (1 + 1)) - 1 by A4, Lm37;

(len W) + 1 <= n by A10, NAT_1:13;

then A12: n = (len W) + 1 by A11, XXREAL_0:1;

then A13: (W .addEdge e) . n = e by A4, Lm38;

A14: (m + 1) - 1 <= ((len W) + 1) - 1 by A6, A12, NAT_1:13;

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

then (W .addEdge e) . m = W . m by A4, Lm38;

hence (W .addEdge e) . m <> (W .addEdge e) . n by A3, A5, A13, A14, Lm46; :: thesis: verum

end;then n + 1 <= len (W .addEdge e) by NAT_1:13;

then (n + 1) - 1 <= (len (W .addEdge e)) - 1 by XREAL_1:13;

then A11: n <= ((len W) + (1 + 1)) - 1 by A4, Lm37;

(len W) + 1 <= n by A10, NAT_1:13;

then A12: n = (len W) + 1 by A11, XXREAL_0:1;

then A13: (W .addEdge e) . n = e by A4, Lm38;

A14: (m + 1) - 1 <= ((len W) + 1) - 1 by A6, A12, NAT_1:13;

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

then (W .addEdge e) . m = W . m by A4, Lm38;

hence (W .addEdge e) . m <> (W .addEdge e) . n by A3, A5, A13, A14, Lm46; :: thesis: verum