let G be _Graph; :: thesis: for P, H being Path of G st P .edges() misses H .edges() & P is open & not H is trivial & H is open & (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} & H .first() = P .last() & H .last() = P .first() holds

P .append H is Cycle-like

let P, H be Path of G; :: thesis: ( P .edges() misses H .edges() & P is open & not H is trivial & H is open & (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} & H .first() = P .last() & H .last() = P .first() implies P .append H is Cycle-like )

assume that

A1: P .edges() misses H .edges() and

A2: P is open and

A3: not H is trivial and

A4: H is open and

A5: (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} and

A6: H .first() = P .last() and

A7: H .last() = P .first() ; :: thesis: P .append H is Cycle-like

set J = P .append H;

A8: (P .append H) .first() = P .first() by A6, GLIB_001:30;

( m in dom (P .append H) & not m in dom P )

(P .append H) .last() = P .first() by A6, A7, GLIB_001:30;

then A52: P .append H is closed by A8;

P .edgeSeq() is one-to-one by GLIB_001:def 27;

then (P .edgeSeq()) ^ (H .edgeSeq()) is one-to-one by A1, A48, FINSEQ_3:91;

then (P .append H) .edgeSeq() is one-to-one by A6, GLIB_001:85;

then P .append H is Trail-like ;

then P .append H is Path-like by A15;

hence P .append H is Cycle-like by A52, A51; :: thesis: verum

P .append H is Cycle-like

let P, H be Path of G; :: thesis: ( P .edges() misses H .edges() & P is open & not H is trivial & H is open & (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} & H .first() = P .last() & H .last() = P .first() implies P .append H is Cycle-like )

assume that

A1: P .edges() misses H .edges() and

A2: P is open and

A3: not H is trivial and

A4: H is open and

A5: (P .vertices()) /\ (H .vertices()) = {(P .first()),(P .last())} and

A6: H .first() = P .last() and

A7: H .last() = P .first() ; :: thesis: P .append H is Cycle-like

set J = P .append H;

A8: (P .append H) .first() = P .first() by A6, GLIB_001:30;

A9: now :: thesis: for m being odd Nat st m <= len P holds

(P .append H) . m = P . m

A11:
for m being odd Nat st m > len P & m <= len (P .append H) holds (P .append H) . m = P . m

let m be odd Nat; :: thesis: ( m <= len P implies (P .append H) . m = P . m )

A10: 1 <= m by ABIAN:12;

assume m <= len P ; :: thesis: (P .append H) . m = P . m

then m in dom P by A10, FINSEQ_3:25;

hence (P .append H) . m = P . m by GLIB_001:32; :: thesis: verum

end;A10: 1 <= m by ABIAN:12;

assume m <= len P ; :: thesis: (P .append H) . m = P . m

then m in dom P by A10, FINSEQ_3:25;

hence (P .append H) . m = P . m by GLIB_001:32; :: thesis: verum

( m in dom (P .append H) & not m in dom P )

proof

A14:
((len (P .append H)) + 1) + (- 1) = ((len P) + (len H)) + (- 1)
by A6, GLIB_001:28;
let m be odd Nat; :: thesis: ( m > len P & m <= len (P .append H) implies ( m in dom (P .append H) & not m in dom P ) )

assume that

A12: m > len P and

A13: m <= len (P .append H) ; :: thesis: ( m in dom (P .append H) & not m in dom P )

1 <= m by ABIAN:12;

hence ( m in dom (P .append H) & not m in dom P ) by A12, A13, FINSEQ_3:25; :: thesis: verum

end;assume that

A12: m > len P and

A13: m <= len (P .append H) ; :: thesis: ( m in dom (P .append H) & not m in dom P )

1 <= m by ABIAN:12;

hence ( m in dom (P .append H) & not m in dom P ) by A12, A13, FINSEQ_3:25; :: thesis: verum

A15: now :: thesis: for m, n being odd Element of NAT st m < n & n <= len (P .append H) & (P .append H) . m = (P .append H) . n holds

( m = 1 & n = len (P .append H) )

A48:
H .edgeSeq() is one-to-one
by GLIB_001:def 27;( m = 1 & n = len (P .append H) )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len (P .append H) & (P .append H) . b_{1} = (P .append H) . b_{2} implies ( b_{1} = 1 & b_{2} = len (P .append H) ) )

assume that

A16: m < n and

A17: n <= len (P .append H) ; :: thesis: ( (P .append H) . b_{1} = (P .append H) . b_{2} implies ( b_{1} = 1 & b_{2} = len (P .append H) ) )

A18: m <= len (P .append H) by A16, A17, XXREAL_0:2;

A19: 1 <= m by ABIAN:12;

end;assume that

A16: m < n and

A17: n <= len (P .append H) ; :: thesis: ( (P .append H) . b

A18: m <= len (P .append H) by A16, A17, XXREAL_0:2;

A19: 1 <= m by ABIAN:12;

per cases
( ( m <= len P & n <= len P ) or ( m <= len P & n > len P ) or ( m > len P & n <= len P ) or ( m > len P & n > len P ) )
;

end;

suppose A20:
( m <= len P & n <= len P )
; :: thesis: ( (P .append H) . b_{1} = (P .append H) . b_{2} implies ( b_{1} = 1 & b_{2} = len (P .append H) ) )

then A21:
P . m = (P .append H) . m
by A9;

P . m <> P . n by A2, A16, A20, GLIB_001:147;

hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by A9, A20, A21; :: thesis: verum

end;P . m <> P . n by A2, A16, A20, GLIB_001:147;

hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by A9, A20, A21; :: thesis: verum

suppose A22:
( m <= len P & n > len P )
; :: thesis: ( (P .append H) . b_{1} = (P .append H) . b_{2} implies ( b_{1} = 1 & b_{2} = len (P .append H) ) )

then A23:
(P .append H) . m = P . m
by A9;

A24: not n in dom P by A11, A17, A22;

n in dom (P .append H) by A11, A17, A22;

then consider j being Element of NAT such that

A25: j < len H and

A26: n = (len P) + j by A24, GLIB_001:34;

reconsider jj = j as even Nat by A26;

reconsider j1 = jj + 1 as odd Nat ;

A27: j1 <= len H by A25, NAT_1:13;

A28: (P .append H) . n = H . (j + 1) by A6, A25, A26, GLIB_001:33;

end;A24: not n in dom P by A11, A17, A22;

n in dom (P .append H) by A11, A17, A22;

then consider j being Element of NAT such that

A25: j < len H and

A26: n = (len P) + j by A24, GLIB_001:34;

reconsider jj = j as even Nat by A26;

reconsider j1 = jj + 1 as odd Nat ;

A27: j1 <= len H by A25, NAT_1:13;

A28: (P .append H) . n = H . (j + 1) by A6, A25, A26, GLIB_001:33;

now :: thesis: ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) )

hence
( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) )
; :: thesis: verumassume A29:
(P .append H) . m = (P .append H) . n
; :: thesis: ( m = 1 & n = len (P .append H) )

(P .append H) . m in H .vertices() by A28, A27, A29, GLIB_001:87;

then A33: (P .append H) . m in (P .vertices()) /\ (H .vertices()) by A32, XBOOLE_0:def 4;

then A34: (P .append H) . n = H .last() by A5, A7, A29, A30, TARSKI:def 2;

end;A30: now :: thesis: not (P .append H) . m = P .last()

A32:
(P .append H) . m in P .vertices()
by A22, A23, GLIB_001:87;
j <> 0
by A22, A26;

then 0 + 1 < j1 by XREAL_1:8;

then A31: H . ((2 * 0) + 1) <> H . j1 by A4, A27, GLIB_001:147;

assume (P .append H) . m = P .last() ; :: thesis: contradiction

hence contradiction by A6, A25, A26, A29, A31, GLIB_001:33; :: thesis: verum

end;then 0 + 1 < j1 by XREAL_1:8;

then A31: H . ((2 * 0) + 1) <> H . j1 by A4, A27, GLIB_001:147;

assume (P .append H) . m = P .last() ; :: thesis: contradiction

hence contradiction by A6, A25, A26, A29, A31, GLIB_001:33; :: thesis: verum

(P .append H) . m in H .vertices() by A28, A27, A29, GLIB_001:87;

then A33: (P .append H) . m in (P .vertices()) /\ (H .vertices()) by A32, XBOOLE_0:def 4;

then A34: (P .append H) . n = H .last() by A5, A7, A29, A30, TARSKI:def 2;

A35: now :: thesis: not n < len (P .append H)

A37:
(P .append H) . m = P .first()
by A5, A33, A30, TARSKI:def 2;assume
n < len (P .append H)
; :: thesis: contradiction

then j1 <> len H by A14, A26;

then A36: j1 < len H by A27, XXREAL_0:1;

H . j1 = H . (len H) by A6, A25, A26, A34, GLIB_001:33;

hence contradiction by A4, A36, GLIB_001:147; :: thesis: verum

end;then j1 <> len H by A14, A26;

then A36: j1 < len H by A27, XXREAL_0:1;

H . j1 = H . (len H) by A6, A25, A26, A34, GLIB_001:33;

hence contradiction by A4, A36, GLIB_001:147; :: thesis: verum

now :: thesis: not 1 < m

hence
( m = 1 & n = len (P .append H) )
by A17, A19, A35, XXREAL_0:1; :: thesis: verumassume
1 < m
; :: thesis: contradiction

then P . m <> P . ((2 * 0) + 1) by A2, A22, GLIB_001:147;

hence contradiction by A9, A22, A37; :: thesis: verum

end;then P . m <> P . ((2 * 0) + 1) by A2, A22, GLIB_001:147;

hence contradiction by A9, A22, A37; :: thesis: verum

suppose
( m > len P & n <= len P )
; :: thesis: ( (P .append H) . b_{1} = (P .append H) . b_{2} implies ( b_{1} = 1 & b_{2} = len (P .append H) ) )

hence
( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) )
by A16, XXREAL_0:2; :: thesis: verum

end;suppose A38:
( m > len P & n > len P )
; :: thesis: ( (P .append H) . b_{1} = (P .append H) . b_{2} implies ( b_{1} = 1 & b_{2} = len (P .append H) ) )

then A39:
not n in dom P
by A11, A17;

n in dom (P .append H) by A11, A17, A38;

then consider j being Element of NAT such that

A40: j < len H and

A41: n = (len P) + j by A39, GLIB_001:34;

reconsider jj = j as even Nat by A41;

reconsider j1 = jj + 1 as odd Element of NAT ;

A42: j1 <= len H by A40, NAT_1:13;

A43: not m in dom P by A11, A18, A38;

m in dom (P .append H) by A11, A18, A38;

then consider k being Element of NAT such that

A44: k < len H and

A45: m = (len P) + k by A43, GLIB_001:34;

reconsider kk = k as even Nat by A45;

reconsider k1 = kk + 1 as odd Nat ;

k < j by A16, A45, A41, XREAL_1:7;

then A46: k1 < j1 by XREAL_1:8;

A47: (P .append H) . ((len P) + j) = H . (j + 1) by A6, A40, GLIB_001:33;

(P .append H) . ((len P) + k) = H . (k + 1) by A6, A44, GLIB_001:33;

hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by A4, A45, A41, A47, A46, A42, GLIB_001:147; :: thesis: verum

end;n in dom (P .append H) by A11, A17, A38;

then consider j being Element of NAT such that

A40: j < len H and

A41: n = (len P) + j by A39, GLIB_001:34;

reconsider jj = j as even Nat by A41;

reconsider j1 = jj + 1 as odd Element of NAT ;

A42: j1 <= len H by A40, NAT_1:13;

A43: not m in dom P by A11, A18, A38;

m in dom (P .append H) by A11, A18, A38;

then consider k being Element of NAT such that

A44: k < len H and

A45: m = (len P) + k by A43, GLIB_001:34;

reconsider kk = k as even Nat by A45;

reconsider k1 = kk + 1 as odd Nat ;

k < j by A16, A45, A41, XREAL_1:7;

then A46: k1 < j1 by XREAL_1:8;

A47: (P .append H) . ((len P) + j) = H . (j + 1) by A6, A40, GLIB_001:33;

(P .append H) . ((len P) + k) = H . (k + 1) by A6, A44, GLIB_001:33;

hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by A4, A45, A41, A47, A46, A42, GLIB_001:147; :: thesis: verum

now :: thesis: not len (P .append H) = 1

then A51:
not P .append H is trivial
by GLIB_001:126;assume
len (P .append H) = 1
; :: thesis: contradiction

then A49: 1 + 1 = (len P) + (len H) by A6, GLIB_001:28;

end;then A49: 1 + 1 = (len P) + (len H) by A6, GLIB_001:28;

now :: thesis: not len P <> 1

hence
contradiction
by A3, A49, GLIB_001:126; :: thesis: verumassume A50:
len P <> 1
; :: thesis: contradiction

1 <= len P by Th2;

then 1 < len P by A50, XXREAL_0:1;

then (len P) + (len H) <= len P by A49, NAT_1:13;

then ((len P) + (len H)) + (- (len P)) <= (len P) + (- (len P)) by XREAL_1:7;

then len H <= 0 ;

hence contradiction ; :: thesis: verum

end;1 <= len P by Th2;

then 1 < len P by A50, XXREAL_0:1;

then (len P) + (len H) <= len P by A49, NAT_1:13;

then ((len P) + (len H)) + (- (len P)) <= (len P) + (- (len P)) by XREAL_1:7;

then len H <= 0 ;

hence contradiction ; :: thesis: verum

(P .append H) .last() = P .first() by A6, A7, GLIB_001:30;

then A52: P .append H is closed by A8;

P .edgeSeq() is one-to-one by GLIB_001:def 27;

then (P .edgeSeq()) ^ (H .edgeSeq()) is one-to-one by A1, A48, FINSEQ_3:91;

then (P .append H) .edgeSeq() is one-to-one by A6, GLIB_001:85;

then P .append H is Trail-like ;

then P .append H is Path-like by A15;

hence P .append H is Cycle-like by A52, A51; :: thesis: verum