let G be _Graph; :: thesis: for W1, W2 being Trail of G st W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() holds

W1 .append W2 is Trail-like

let W1, W2 be Trail of G; :: thesis: ( W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() implies W1 .append W2 is Trail-like )

assume that

A1: W1 .last() = W2 .first() and

A2: W1 .edges() misses W2 .edges() ; :: thesis: W1 .append W2 is Trail-like

set W = W1 .append W2;

W1 .append W2 is Trail-like

let W1, W2 be Trail of G; :: thesis: ( W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() implies W1 .append W2 is Trail-like )

assume that

A1: W1 .last() = W2 .first() and

A2: W1 .edges() misses W2 .edges() ; :: thesis: W1 .append W2 is Trail-like

set W = W1 .append W2;

now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len (W1 .append W2) holds

(W1 .append W2) . m <> (W1 .append W2) . n

hence
W1 .append W2 is Trail-like
by GLIB_001:138; :: thesis: verum(W1 .append W2) . m <> (W1 .append W2) . n

let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len (W1 .append W2) implies (W1 .append W2) . b_{1} <> (W1 .append W2) . b_{2} )

assume that

A3: 1 <= m and

A4: m < n and

A5: n <= len (W1 .append W2) ; :: thesis: (W1 .append W2) . b_{1} <> (W1 .append W2) . b_{2}

1 <= n by A3, A4, XXREAL_0:2;

then A6: n in dom (W1 .append W2) by A5, FINSEQ_3:25;

m <= len (W1 .append W2) by A4, A5, XXREAL_0:2;

then A7: m in dom (W1 .append W2) by A3, FINSEQ_3:25;

end;assume that

A3: 1 <= m and

A4: m < n and

A5: n <= len (W1 .append W2) ; :: thesis: (W1 .append W2) . b

1 <= n by A3, A4, XXREAL_0:2;

then A6: n in dom (W1 .append W2) by A5, FINSEQ_3:25;

m <= len (W1 .append W2) by A4, A5, XXREAL_0:2;

then A7: m in dom (W1 .append W2) by A3, FINSEQ_3:25;

per cases
( n in dom W1 or ex k being Element of NAT st

( k < len W2 & n = (len W1) + k ) ) by A6, GLIB_001:34;

end;

( k < len W2 & n = (len W1) + k ) ) by A6, GLIB_001:34;

suppose A8:
n in dom W1
; :: thesis: (W1 .append W2) . b_{1} <> (W1 .append W2) . b_{2}

then A9:
n <= len W1
by FINSEQ_3:25;

then m <= len W1 by A4, XXREAL_0:2;

then m in dom W1 by A3, FINSEQ_3:25;

then A10: W1 . m = (W1 .append W2) . m by GLIB_001:32;

W1 . m <> W1 . n by A3, A4, A9, GLIB_001:138;

hence (W1 .append W2) . m <> (W1 .append W2) . n by A8, A10, GLIB_001:32; :: thesis: verum

end;then m <= len W1 by A4, XXREAL_0:2;

then m in dom W1 by A3, FINSEQ_3:25;

then A10: W1 . m = (W1 .append W2) . m by GLIB_001:32;

W1 . m <> W1 . n by A3, A4, A9, GLIB_001:138;

hence (W1 .append W2) . m <> (W1 .append W2) . n by A8, A10, GLIB_001:32; :: thesis: verum

suppose
ex k being Element of NAT st

( k < len W2 & n = (len W1) + k ) ; :: thesis: (W1 .append W2) . b_{1} <> (W1 .append W2) . b_{2}

( k < len W2 & n = (len W1) + k ) ; :: thesis: (W1 .append W2) . b

then consider k being Element of NAT such that

A11: k < len W2 and

A12: n = (len W1) + k ;

reconsider k = k as odd Element of NAT by A12;

A13: (W1 .append W2) . n = W2 . (k + 1) by A1, A11, A12, GLIB_001:33;

A14: k + 1 <= len W2 by A11, NAT_1:13;

1 <= k + 1 by NAT_1:11;

then A15: W2 . (k + 1) in W2 .edges() by A14, GLIB_001:99;

end;A11: k < len W2 and

A12: n = (len W1) + k ;

reconsider k = k as odd Element of NAT by A12;

A13: (W1 .append W2) . n = W2 . (k + 1) by A1, A11, A12, GLIB_001:33;

A14: k + 1 <= len W2 by A11, NAT_1:13;

1 <= k + 1 by NAT_1:11;

then A15: W2 . (k + 1) in W2 .edges() by A14, GLIB_001:99;

per cases
( m in dom W1 or ex l being Element of NAT st

( l < len W2 & m = (len W1) + l ) ) by A7, GLIB_001:34;

end;

( l < len W2 & m = (len W1) + l ) ) by A7, GLIB_001:34;

suppose A16:
m in dom W1
; :: thesis: (W1 .append W2) . b_{1} <> (W1 .append W2) . b_{2}

then
( 1 <= m & m <= len W1 )
by FINSEQ_3:25;

then A17: W1 . m in W1 .edges() by GLIB_001:99;

(W1 .append W2) . m = W1 . m by A16, GLIB_001:32;

hence (W1 .append W2) . m <> (W1 .append W2) . n by A2, A13, A15, A17, XBOOLE_0:3; :: thesis: verum

end;then A17: W1 . m in W1 .edges() by GLIB_001:99;

(W1 .append W2) . m = W1 . m by A16, GLIB_001:32;

hence (W1 .append W2) . m <> (W1 .append W2) . n by A2, A13, A15, A17, XBOOLE_0:3; :: thesis: verum

suppose
ex l being Element of NAT st

( l < len W2 & m = (len W1) + l ) ; :: thesis: (W1 .append W2) . b_{1} <> (W1 .append W2) . b_{2}

( l < len W2 & m = (len W1) + l ) ; :: thesis: (W1 .append W2) . b

then consider l being Element of NAT such that

A18: l < len W2 and

A19: m = (len W1) + l ;

reconsider l = l as odd Element of NAT by A19;

l < k by A4, A12, A19, XREAL_1:6;

then A20: ( 1 <= l + 1 & l + 1 < k + 1 ) by NAT_1:11, XREAL_1:6;

(W1 .append W2) . m = W2 . (l + 1) by A1, A18, A19, GLIB_001:33;

hence (W1 .append W2) . m <> (W1 .append W2) . n by A13, A14, A20, GLIB_001:138; :: thesis: verum

end;A18: l < len W2 and

A19: m = (len W1) + l ;

reconsider l = l as odd Element of NAT by A19;

l < k by A4, A12, A19, XREAL_1:6;

then A20: ( 1 <= l + 1 & l + 1 < k + 1 ) by NAT_1:11, XREAL_1:6;

(W1 .append W2) . m = W2 . (l + 1) by A1, A18, A19, GLIB_001:33;

hence (W1 .append W2) . m <> (W1 .append W2) . n by A13, A14, A20, GLIB_001:138; :: thesis: verum