let G be _Graph; :: thesis: for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) & (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} holds

P1 .append P2 is Path-like

let P1, P2 be Path of G; :: thesis: ( P1 .last() = P2 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) & (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} implies P1 .append P2 is Path-like )

assume that

A1: P1 .last() = P2 .first() and

A2: P1 is open and

A3: P2 is open and

A4: P1 .edges() misses P2 .edges() and

A5: ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) and

A6: (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} ; :: thesis: P1 .append P2 is Path-like

thus P1 .append P2 is Trail-like by A1, A4, Th17; :: according to GLIB_001:def 28 :: thesis: for b_{1}, b_{2} being Element of omega holds

( b_{2} <= b_{1} or not b_{2} <= len (P1 .append P2) or not (P1 .append P2) . b_{1} = (P1 .append P2) . b_{2} or ( b_{1} = 1 & b_{2} = len (P1 .append P2) ) )

set P = P1 .append P2;

let m, n be odd Element of NAT ; :: thesis: ( n <= m or not n <= len (P1 .append P2) or not (P1 .append P2) . m = (P1 .append P2) . n or ( m = 1 & n = len (P1 .append P2) ) )

assume that

A7: m < n and

A8: n <= len (P1 .append P2) and

A9: (P1 .append P2) . m = (P1 .append P2) . n and

A10: ( m <> 1 or n <> len (P1 .append P2) ) ; :: thesis: contradiction

A11: 1 <= m by ABIAN:12;

1 <= n by ABIAN:12;

then A12: n in dom (P1 .append P2) by A8, FINSEQ_3:25;

m <= len (P1 .append P2) by A7, A8, XXREAL_0:2;

then A13: m in dom (P1 .append P2) by A11, FINSEQ_3:25;

P1 .append P2 is Path-like

let P1, P2 be Path of G; :: thesis: ( P1 .last() = P2 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) & (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} implies P1 .append P2 is Path-like )

assume that

A1: P1 .last() = P2 .first() and

A2: P1 is open and

A3: P2 is open and

A4: P1 .edges() misses P2 .edges() and

A5: ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) and

A6: (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} ; :: thesis: P1 .append P2 is Path-like

thus P1 .append P2 is Trail-like by A1, A4, Th17; :: according to GLIB_001:def 28 :: thesis: for b

( b

set P = P1 .append P2;

let m, n be odd Element of NAT ; :: thesis: ( n <= m or not n <= len (P1 .append P2) or not (P1 .append P2) . m = (P1 .append P2) . n or ( m = 1 & n = len (P1 .append P2) ) )

assume that

A7: m < n and

A8: n <= len (P1 .append P2) and

A9: (P1 .append P2) . m = (P1 .append P2) . n and

A10: ( m <> 1 or n <> len (P1 .append P2) ) ; :: thesis: contradiction

A11: 1 <= m by ABIAN:12;

1 <= n by ABIAN:12;

then A12: n in dom (P1 .append P2) by A8, FINSEQ_3:25;

m <= len (P1 .append P2) by A7, A8, XXREAL_0:2;

then A13: m in dom (P1 .append P2) by A11, FINSEQ_3:25;

per cases
( ex k being Element of NAT st

( k < len P2 & n = (len P1) + k ) or n in dom P1 ) by A12, GLIB_001:34;

end;

( k < len P2 & n = (len P1) + k ) or n in dom P1 ) by A12, GLIB_001:34;

suppose
ex k being Element of NAT st

( k < len P2 & n = (len P1) + k ) ; :: thesis: contradiction

( k < len P2 & n = (len P1) + k ) ; :: thesis: contradiction

then consider k being Element of NAT such that

A14: k < len P2 and

A15: n = (len P1) + k ;

A16: (P1 .append P2) . n = P2 . (k + 1) by A1, A14, A15, GLIB_001:33;

reconsider k = k as even Element of NAT by A15;

A17: k + 1 <= len P2 by A14, NAT_1:13;

then A18: P2 . (k + 1) in P2 .vertices() by GLIB_001:87;

end;A14: k < len P2 and

A15: n = (len P1) + k ;

A16: (P1 .append P2) . n = P2 . (k + 1) by A1, A14, A15, GLIB_001:33;

reconsider k = k as even Element of NAT by A15;

A17: k + 1 <= len P2 by A14, NAT_1:13;

then A18: P2 . (k + 1) in P2 .vertices() by GLIB_001:87;

per cases
( ex k being Element of NAT st

( k < len P2 & m = (len P1) + k ) or m in dom P1 ) by A13, GLIB_001:34;

end;

( k < len P2 & m = (len P1) + k ) or m in dom P1 ) by A13, GLIB_001:34;

suppose
ex k being Element of NAT st

( k < len P2 & m = (len P1) + k ) ; :: thesis: contradiction

( k < len P2 & m = (len P1) + k ) ; :: thesis: contradiction

then consider l being Element of NAT such that

A19: l < len P2 and

A20: m = (len P1) + l ;

A21: (P1 .append P2) . m = P2 . (l + 1) by A1, A19, A20, GLIB_001:33;

l < k by A7, A15, A20, XREAL_1:6;

then A22: l + 1 < k + 1 by XREAL_1:6;

reconsider l = l as even Element of NAT by A20;

l + 1 is odd ;

then A23: P2 .last() = P2 . (k + 1) by A9, A16, A17, A21, A22, GLIB_001:def 28;

P2 .first() = P2 . (l + 1) by A9, A16, A17, A21, A22, GLIB_001:def 28;

hence contradiction by A3, A9, A16, A21, A23; :: thesis: verum

end;A19: l < len P2 and

A20: m = (len P1) + l ;

A21: (P1 .append P2) . m = P2 . (l + 1) by A1, A19, A20, GLIB_001:33;

l < k by A7, A15, A20, XREAL_1:6;

then A22: l + 1 < k + 1 by XREAL_1:6;

reconsider l = l as even Element of NAT by A20;

l + 1 is odd ;

then A23: P2 .last() = P2 . (k + 1) by A9, A16, A17, A21, A22, GLIB_001:def 28;

P2 .first() = P2 . (l + 1) by A9, A16, A17, A21, A22, GLIB_001:def 28;

hence contradiction by A3, A9, A16, A21, A23; :: thesis: verum

suppose A24:
m in dom P1
; :: thesis: contradiction

set x = P1 . m;

A25: P1 . m = (P1 .append P2) . m by A24, GLIB_001:32;

A26: m <= len P1 by A24, FINSEQ_3:25;

then P1 . m in P1 .vertices() by GLIB_001:87;

then A27: P1 . m in (P1 .vertices()) /\ (P2 .vertices()) by A9, A16, A18, A25, XBOOLE_0:def 4;

end;A25: P1 . m = (P1 .append P2) . m by A24, GLIB_001:32;

A26: m <= len P1 by A24, FINSEQ_3:25;

then P1 . m in P1 .vertices() by GLIB_001:87;

then A27: P1 . m in (P1 .vertices()) /\ (P2 .vertices()) by A9, A16, A18, A25, XBOOLE_0:def 4;

per cases
( P1 . m = P1 .last() or P1 . m = P1 .first() )
by A6, A27, TARSKI:def 2;

end;

suppose A28:
P1 . m = P1 .last()
; :: thesis: contradiction

then A29:
m >= len P1
by GLIB_001:def 28, A2;

A30: (2 * 0) + 1 >= k + 1 by A1, A3, A9, A16, A17, A25, A28, GLIB_001:def 28;

1 <= k + 1 by NAT_1:11;

then 1 = k + 1 by A30, XXREAL_0:1;

hence contradiction by A7, A15, A29; :: thesis: verum

end;A30: (2 * 0) + 1 >= k + 1 by A1, A3, A9, A16, A17, A25, A28, GLIB_001:def 28;

1 <= k + 1 by NAT_1:11;

then 1 = k + 1 by A30, XXREAL_0:1;

hence contradiction by A7, A15, A29; :: thesis: verum

suppose A31:
P1 . m = P1 .first()
; :: thesis: contradiction

then A32:
P1 . m = P1 . ((2 * 0) + 1)
;

P2 . (k + 1) = P2 .last() by A5, A9, A16, A18, A24, A31, GLIB_001:32;

then P2 .first() = P2 .last() by A34, GLIB_001:def 28;

hence contradiction by A3; :: thesis: verum

end;A33: now :: thesis: not m <> 1

assume
m <> 1
; :: thesis: contradiction

then 1 < m by A11, XXREAL_0:1;

then P1 . m = P1 .last() by A26, A32, GLIB_001:def 28;

hence contradiction by A2, A31; :: thesis: verum

end;then 1 < m by A11, XXREAL_0:1;

then P1 . m = P1 .last() by A26, A32, GLIB_001:def 28;

hence contradiction by A2, A31; :: thesis: verum

now :: thesis: not k + 1 = len P2

then A34:
k + 1 < len P2
by A17, XXREAL_0:1;assume
k + 1 = len P2
; :: thesis: contradiction

then (len (P1 .append P2)) + 1 = (len P1) + (k + 1) by A1, GLIB_001:28;

hence contradiction by A10, A15, A33; :: thesis: verum

end;then (len (P1 .append P2)) + 1 = (len P1) + (k + 1) by A1, GLIB_001:28;

hence contradiction by A10, A15, A33; :: thesis: verum

P2 . (k + 1) = P2 .last() by A5, A9, A16, A18, A24, A31, GLIB_001:32;

then P2 .first() = P2 .last() by A34, GLIB_001:def 28;

hence contradiction by A3; :: thesis: verum

suppose A35:
n in dom P1
; :: thesis: contradiction

then A36:
n <= len P1
by FINSEQ_3:25;

then ( 1 <= m & m <= len P1 ) by A7, ABIAN:12, XXREAL_0:2;

then m in dom P1 by FINSEQ_3:25;

then A37: P1 . m = (P1 .append P2) . m by GLIB_001:32

.= P1 . n by A9, A35, GLIB_001:32 ;

then m = 1 by A7, A36, GLIB_001:def 28;

then P1 .first() = P1 .last() by A7, A36, A37, GLIB_001:def 28;

hence contradiction by A2; :: thesis: verum

end;then ( 1 <= m & m <= len P1 ) by A7, ABIAN:12, XXREAL_0:2;

then m in dom P1 by FINSEQ_3:25;

then A37: P1 . m = (P1 .append P2) . m by GLIB_001:32

.= P1 . n by A9, A35, GLIB_001:32 ;

then m = 1 by A7, A36, GLIB_001:def 28;

then P1 .first() = P1 .last() by A7, A36, A37, GLIB_001:def 28;

hence contradiction by A2; :: thesis: verum