let G be acyclic _Graph; :: thesis: for W being Path of G

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

W .addEdge e is Path-like

let W be Path of G; :: thesis: for e being set st not e in W .edges() & e in (W .last()) .edgesInOut() holds

W .addEdge e is Path-like

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

assume that

A1: not e in W .edges() and

A2: e in (W .last()) .edgesInOut() ; :: thesis: W .addEdge e is Path-like

set v = (W .last()) .adj e;

set W2 = W .addEdge e;

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

then A4: len (W .addEdge e) = (len W) + 2 by GLIB_001:64;

A5: W .addEdge e is Trail-like by A1, A2, GLIB_001:142;

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

W .addEdge e is Path-like

let W be Path of G; :: thesis: for e being set st not e in W .edges() & e in (W .last()) .edgesInOut() holds

W .addEdge e is Path-like

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

assume that

A1: not e in W .edges() and

A2: e in (W .last()) .edgesInOut() ; :: thesis: W .addEdge e is Path-like

set v = (W .last()) .adj e;

set W2 = W .addEdge e;

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

then A4: len (W .addEdge e) = (len W) + 2 by GLIB_001:64;

A5: W .addEdge e is Trail-like by A1, A2, GLIB_001:142;

now :: thesis: W .addEdge e is Path-like end;

hence
W .addEdge e is Path-like
; :: thesis: verumper cases
( W is trivial or not W is trivial )
;

end;

suppose A6:
W is trivial
; :: thesis: W .addEdge e is Path-like

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

W . n <> (W .last()) .adj e by GLIB_001:126;

hence W .addEdge e is Path-like by A1, A3, A6, GLIB_001:150; :: thesis: verum

end;W . n <> (W .last()) .adj e by GLIB_001:126;

hence W .addEdge e is Path-like by A1, A3, A6, GLIB_001:150; :: thesis: verum

suppose A7:
not W is trivial
; :: thesis: W .addEdge e is Path-like

hence W .addEdge e is Path-like by A1, A3, A8, GLIB_001:150; :: thesis: verum

end;

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

W . n <> (W .last()) .adj e

not W is closed
by A7, GLIB_001:def 31, Def2;W . n <> (W .last()) .adj e

let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len W implies W . n <> (W .last()) .adj e )

assume that

A9: 1 < n and

A10: n <= len W ; :: thesis: W . n <> (W .last()) .adj e

end;assume that

A9: 1 < n and

A10: n <= len W ; :: thesis: W . n <> (W .last()) .adj e

now :: thesis: not W . n = (W .last()) .adj e

hence
W . n <> (W .last()) .adj e
; :: thesis: verumset W3 = (W .addEdge e) .cut (n,(len (W .addEdge e)));

assume A11: W . n = (W .last()) .adj e ; :: thesis: contradiction

A12: n <= len (W .addEdge e) by A4, A10, NAT_1:12;

then A13: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .first() = (W .addEdge e) . n by GLIB_001:37;

A14: not W4 is trivial by A5, GLIB_001:166;

((W .addEdge e) .cut (n,(len (W .addEdge e)))) .last() = (W .addEdge e) . (len (W .addEdge e)) by A12, GLIB_001:37;

then A15: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .last() = (W .addEdge e) .last() by GLIB_001:def 7

.= (W .last()) .adj e by A3, GLIB_001:63 ;

n in dom W by A9, A10, FINSEQ_3:25;

then ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .first() = (W .last()) .adj e by A3, A11, A13, GLIB_001:65;

then W4 is_Walk_from (W .last()) .adj e,(W .last()) .adj e by A15, GLIB_001:def 32;

then W4 is closed by GLIB_001:119;

then W4 is Cycle-like by A14, GLIB_001:def 31;

hence contradiction by Def2; :: thesis: verum

end;assume A11: W . n = (W .last()) .adj e ; :: thesis: contradiction

A12: n <= len (W .addEdge e) by A4, A10, NAT_1:12;

then A13: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .first() = (W .addEdge e) . n by GLIB_001:37;

now :: thesis: not (W .addEdge e) .cut (n,(len (W .addEdge e))) is trivial

then consider W4 being Path of (W .addEdge e) .cut (n,(len (W .addEdge e))) such that assume
(W .addEdge e) .cut (n,(len (W .addEdge e))) is trivial
; :: thesis: contradiction

then len ((W .addEdge e) .cut (n,(len (W .addEdge e)))) = 1 by GLIB_001:126;

then 1 + n = (len (W .addEdge e)) + 1 by A12, GLIB_001:36;

then (2 + (len W)) - (len W) <= (len W) - (len W) by A4, A10, XREAL_1:13;

then 2 <= 0 ;

hence contradiction ; :: thesis: verum

end;then len ((W .addEdge e) .cut (n,(len (W .addEdge e)))) = 1 by GLIB_001:126;

then 1 + n = (len (W .addEdge e)) + 1 by A12, GLIB_001:36;

then (2 + (len W)) - (len W) <= (len W) - (len W) by A4, A10, XREAL_1:13;

then 2 <= 0 ;

hence contradiction ; :: thesis: verum

A14: not W4 is trivial by A5, GLIB_001:166;

((W .addEdge e) .cut (n,(len (W .addEdge e)))) .last() = (W .addEdge e) . (len (W .addEdge e)) by A12, GLIB_001:37;

then A15: ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .last() = (W .addEdge e) .last() by GLIB_001:def 7

.= (W .last()) .adj e by A3, GLIB_001:63 ;

n in dom W by A9, A10, FINSEQ_3:25;

then ((W .addEdge e) .cut (n,(len (W .addEdge e)))) .first() = (W .last()) .adj e by A3, A11, A13, GLIB_001:65;

then W4 is_Walk_from (W .last()) .adj e,(W .last()) .adj e by A15, GLIB_001:def 32;

then W4 is closed by GLIB_001:119;

then W4 is Cycle-like by A14, GLIB_001:def 31;

hence contradiction by Def2; :: thesis: verum

hence W .addEdge e is Path-like by A1, A3, A8, GLIB_001:150; :: thesis: verum