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 & () /\ () = {(),()} & 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 & () /\ () = {(),()} & 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()) /\ () = {(),()} and
A6: H .first() = P .last() and
A7: H .last() = P .first() ; :: thesis:
set J = P .append H;
A8: (P .append H) .first() = P .first() by ;
A9: now :: thesis: for m being odd Nat st m <= len P 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 ;
hence (P .append H) . m = P . m by GLIB_001:32; :: thesis: verum
end;
A11: for m being odd Nat st m > len P & m <= len (P .append H) holds
( m in dom (P .append H) & not m in dom P )
proof
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 ; :: thesis: verum
end;
A14: ((len (P .append H)) + 1) + (- 1) = ((len P) + (len H)) + (- 1) by ;
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) )
let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len (P .append H) & (P .append H) . b1 = (P .append H) . b2 implies ( b1 = 1 & b2 = len (P .append H) ) )
assume that
A16: m < n and
A17: n <= len (P .append H) ; :: thesis: ( (P .append H) . b1 = (P .append H) . b2 implies ( b1 = 1 & b2 = len (P .append H) ) )
A18: m <= len (P .append H) by ;
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 ) ) ;
suppose A20: ( m <= len P & n <= len P ) ; :: thesis: ( (P .append H) . b1 = (P .append H) . b2 implies ( b1 = 1 & b2 = len (P .append H) ) )
then A21: P . m = (P .append H) . m by A9;
P . m <> P . n by ;
hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by A9, A20, A21; :: thesis: verum
end;
suppose A22: ( m <= len P & n > len P ) ; :: thesis: ( (P .append H) . b1 = (P .append H) . b2 implies ( b1 = 1 & b2 = len (P .append H) ) )
then A23: (P .append H) . m = P . m by A9;
A24: not n in dom P by ;
n in dom (P .append H) by ;
then consider j being Element of NAT such that
A25: j < len H and
A26: n = (len P) + j by ;
reconsider jj = j as even Nat by A26;
reconsider j1 = jj + 1 as odd Nat ;
A27: j1 <= len H by ;
A28: (P .append H) . n = H . (j + 1) by ;
now :: thesis: ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) )
assume A29: (P .append H) . m = (P .append H) . n ; :: thesis: ( m = 1 & n = len (P .append H) )
A30: now :: thesis: not (P .append H) . m = P .last()
j <> 0 by ;
then 0 + 1 < j1 by XREAL_1:8;
then A31: H . ((2 * 0) + 1) <> H . j1 by ;
assume (P .append H) . m = P .last() ; :: thesis: contradiction
hence contradiction by A6, A25, A26, A29, A31, GLIB_001:33; :: thesis: verum
end;
A32: (P .append H) . m in P .vertices() by ;
(P .append H) . m in H .vertices() by ;
then A33: (P .append H) . m in () /\ () by ;
then A34: (P .append H) . n = H .last() by ;
A35: now :: thesis: not n < len (P .append H)
assume n < len (P .append H) ; :: thesis: contradiction
then j1 <> len H by ;
then A36: j1 < len H by ;
H . j1 = H . (len H) by ;
hence contradiction by A4, A36, GLIB_001:147; :: thesis: verum
end;
A37: (P .append H) . m = P .first() by ;
now :: thesis: not 1 < m
assume 1 < m ; :: thesis: contradiction
then P . m <> P . ((2 * 0) + 1) by ;
hence contradiction by A9, A22, A37; :: thesis: verum
end;
hence ( m = 1 & n = len (P .append H) ) by ; :: thesis: verum
end;
hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) ; :: thesis: verum
end;
suppose ( m > len P & n <= len P ) ; :: thesis: ( (P .append H) . b1 = (P .append H) . b2 implies ( b1 = 1 & b2 = len (P .append H) ) )
hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by ; :: thesis: verum
end;
suppose A38: ( m > len P & n > len P ) ; :: thesis: ( (P .append H) . b1 = (P .append H) . b2 implies ( b1 = 1 & b2 = len (P .append H) ) )
then A39: not n in dom P by ;
n in dom (P .append H) by ;
then consider j being Element of NAT such that
A40: j < len H and
A41: n = (len P) + j by ;
reconsider jj = j as even Nat by A41;
reconsider j1 = jj + 1 as odd Element of NAT ;
A42: j1 <= len H by ;
A43: not m in dom P by ;
m in dom (P .append H) by ;
then consider k being Element of NAT such that
A44: k < len H and
A45: m = (len P) + k by ;
reconsider kk = k as even Nat by A45;
reconsider k1 = kk + 1 as odd Nat ;
k < j by ;
then A46: k1 < j1 by XREAL_1:8;
A47: (P .append H) . ((len P) + j) = H . (j + 1) by ;
(P .append H) . ((len P) + k) = H . (k + 1) by ;
hence ( (P .append H) . m = (P .append H) . n implies ( m = 1 & n = len (P .append H) ) ) by ; :: thesis: verum
end;
end;
end;
A48: H .edgeSeq() is one-to-one by GLIB_001:def 27;
now :: thesis: not len (P .append H) = 1
assume len (P .append H) = 1 ; :: thesis: contradiction
then A49: 1 + 1 = (len P) + (len H) by ;
now :: thesis: not len P <> 1
assume A50: len P <> 1 ; :: thesis: contradiction
1 <= len P by Th2;
then 1 < len P by ;
then (len P) + (len H) <= len P by ;
then ((len P) + (len H)) + (- (len P)) <= (len P) + (- (len P)) by XREAL_1:7;
then len H <= 0 ;
hence contradiction ; :: thesis: verum
end;
hence contradiction by A3, A49, GLIB_001:126; :: thesis: verum
end;
then A51: not P .append H is trivial by GLIB_001:126;
(P .append H) .last() = P .first() by ;
then A52: P .append H is closed by A8;
P .edgeSeq() is one-to-one by GLIB_001:def 27;
then (P .edgeSeq()) ^ () is one-to-one by ;
then (P .append H) .edgeSeq() is one-to-one by ;
then P .append H is Trail-like ;
then P .append H is Path-like by A15;
hence P .append H is Cycle-like by ; :: thesis: verum