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;
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
let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len (W1 .append W2) implies (W1 .append W2) . b1 <> (W1 .append W2) . b2 )
assume that
A3: 1 <= m and
A4: m < n and
A5: n <= len (W1 .append W2) ; :: thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
1 <= n by ;
then A6: n in dom (W1 .append W2) by ;
m <= len (W1 .append W2) by ;
then A7: m in dom (W1 .append W2) by ;
per cases ( n in dom W1 or ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) )
by ;
suppose A8: n in dom W1 ; :: thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
then A9: n <= len W1 by FINSEQ_3:25;
then m <= len W1 by ;
then m in dom W1 by ;
then A10: W1 . m = (W1 .append W2) . m by GLIB_001:32;
W1 . m <> W1 . n by ;
hence (W1 .append W2) . m <> (W1 .append W2) . n by ; :: thesis: verum
end;
suppose ex k being Element of NAT st
( k < len W2 & n = (len W1) + k ) ; :: thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
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 ;
A14: k + 1 <= len W2 by ;
1 <= k + 1 by NAT_1:11;
then A15: W2 . (k + 1) in W2 .edges() by ;
per cases ( m in dom W1 or ex l being Element of NAT st
( l < len W2 & m = (len W1) + l ) )
by ;
suppose A16: m in dom W1 ; :: thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
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 ;
hence (W1 .append W2) . m <> (W1 .append W2) . n by ; :: thesis: verum
end;
suppose ex l being Element of NAT st
( l < len W2 & m = (len W1) + l ) ; :: thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2
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 ;
then A20: ( 1 <= l + 1 & l + 1 < k + 1 ) by ;
(W1 .append W2) . m = W2 . (l + 1) by ;
hence (W1 .append W2) . m <> (W1 .append W2) . n by ; :: thesis: verum
end;
end;
end;
end;
end;
hence W1 .append W2 is Trail-like by GLIB_001:138; :: thesis: verum