let G be chordal _Graph; :: thesis: for P being Path of G st not P is closed & not P is chordal holds
for x, e being set st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being set holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal )
let P be Path of G; :: thesis: ( not P is closed & not P is chordal implies for x, e being set st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being set holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal ) )
assume that
A1: not P is closed and
A2: not P is chordal ; :: thesis: for x, e being set st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being set holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal )
let x, e be set ; :: thesis: ( not x in P .vertices() & e Joins P .last() ,x,G & ( for f being set holds not f Joins P . ((len P) - 2),x,G ) implies ( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal ) )
assume that
A3: not x in P .vertices() and
A4: e Joins P .last() ,x,G and
A5: for f being set holds not f Joins P . ((len P) - 2),x,G ; :: thesis: ( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal )
reconsider Q = P .addEdge e as Path of G by A1, A3, A4, GLIB_001:152;
A6: len Q = (len P) + 2 by A4, GLIB_001:65;
defpred S1[ Nat] means ( 4 <= 2 * $1 & 2 * $1 <= (len P) + 1 implies for j being odd Nat st j + (2 * $1) = (len P) + 2 holds
for e being set holds not e Joins Q . j,x,G );
A7: now
let n be odd Nat; :: thesis: ( n <= len P implies P . n = Q . n )
assume A8: n <= len P ; :: thesis: P . n = Q . n
1 <= n by Th2;
then n in dom P by A8, FINSEQ_3:27;
hence P . n = Q . n by A4, GLIB_001:66; :: thesis: verum
end;
A9: Q .last() = x by A4, GLIB_001:64;
for k being Nat st ( for a being Nat st a < k holds
S1[a] ) holds
S1[k]
proof
let k be Nat; :: thesis: ( ( for a being Nat st a < k holds
S1[a] ) implies S1[k] )
assume A10: for a being Nat st a < k holds
S1[a] ; :: thesis: S1[k]
assume that
A11: 4 <= 2 * k and
2 * k <= (len P) + 1 ; :: thesis: for j being odd Nat st j + (2 * k) = (len P) + 2 holds
for e being set holds not e Joins Q . j,x,G
let j be odd Nat; :: thesis: ( j + (2 * k) = (len P) + 2 implies for e being set holds not e Joins Q . j,x,G )
assume A12: j + (2 * k) = (len P) + 2 ; :: thesis: for e being set holds not e Joins Q . j,x,G
j + 4 <= j + (2 * k) by A11, XREAL_1:9;
then A13: (j + 4) - 4 <= ((len P) + 2) - 4 by A12, XREAL_1:11;
A14: (len P) - 2 <= len P by XREAL_1:45;
then A15: j <= len P by A13, XXREAL_0:2;
A16: j in NAT by ORDINAL1:def 13;
let e be set ; :: thesis: not e Joins Q . j,x,G
assume A17: e Joins Q . j,x,G ; :: thesis: contradiction
per cases ( j = (len P) - 2 or j < (len P) - (2 * 1) ) by A13, XXREAL_0:1;
suppose j = (len P) - 2 ; :: thesis: contradiction
then Q . j = P . ((len P) - 2) by A7, XREAL_1:45;
hence contradiction by A5, A17; :: thesis: verum
end;
suppose A18: j < (len P) - (2 * 1) ; :: thesis: contradiction
reconsider lP2 = (len P) + 2 as odd Element of NAT ;
reconsider jj = j as odd Element of NAT by ORDINAL1:def 13;
set B = Q .cut (jj,lP2);
len P < (len P) + 2 by XREAL_1:31;
then A19: j <= (len P) + 2 by A15, XXREAL_0:2;
then A20: (Q .cut (jj,lP2)) .last() = x by A9, A6, GLIB_001:38;
A21: (len (Q .cut (jj,lP2))) + j = ((len P) + 2) + 1 by A6, A19, GLIB_001:37;
A22: now
let i be even Nat; :: thesis: ( i < (len (Q .cut (jj,lP2))) - 1 implies ( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P ) )
assume A23: i < (len (Q .cut (jj,lP2))) - 1 ; :: thesis: ( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P )
j + i < ((len (Q .cut (jj,lP2))) - 1) + j by A23, XREAL_1:10;
then A24: j + i <= ((len P) + 2) - 2 by A21, Th3;
(len (Q .cut (jj,lP2))) - 1 < len (Q .cut (jj,lP2)) by XREAL_1:46;
then A25: i < len (Q .cut (jj,lP2)) by A23, XXREAL_0:2;
A26: i in NAT by ORDINAL1:def 13;
then j + i in dom Q by A6, A19, A25, GLIB_001:37;
then A27: 1 <= j + i by FINSEQ_3:27;
(Q .cut (jj,lP2)) . (i + 1) = Q . (j + i) by A6, A19, A26, A25, GLIB_001:37;
hence ( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P ) by A7, A27, A24, FINSEQ_3:27; :: thesis: verum
end;
set C = (Q .cut (jj,lP2)) .addEdge e;
A28: (Q .cut (jj,lP2)) .first() = Q . j by A6, A19, GLIB_001:38;
A29: (Q .cut (jj,lP2)) .first() = Q . j by A6, A19, GLIB_001:38;
then A30: e Joins (Q .cut (jj,lP2)) .last() ,(Q .cut (jj,lP2)) .first() ,G by A17, A20, GLIB_000:17;
A31: now
let n be odd Nat; :: thesis: ( n <= len (Q .cut (jj,lP2)) implies ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n )
assume A32: n <= len (Q .cut (jj,lP2)) ; :: thesis: ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n
1 <= n by Th2;
then n in dom (Q .cut (jj,lP2)) by A32, FINSEQ_3:27;
hence ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n by A30, GLIB_001:66; :: thesis: verum
end;
A33: ((len P) + 3) - ((len P) - 2) < ((len P) + 3) - j by A18, XREAL_1:17;
then A34: 3 < len (Q .cut (jj,lP2)) by A21, XXREAL_0:2;
(len (Q .cut (jj,lP2))) + 2 > 5 + 2 by A21, A33, XREAL_1:10;
then A35: len ((Q .cut (jj,lP2)) .addEdge e) > 7 by A17, A20, GLIB_000:17, GLIB_001:65;
A36: now
assume ((Q .cut (jj,lP2)) .addEdge e) .length() <= 3 ; :: thesis: contradiction
then 2 * (((Q .cut (jj,lP2)) .addEdge e) .length()) <= 2 * 3 by XREAL_1:66;
then (2 * (((Q .cut (jj,lP2)) .addEdge e) .length())) + 1 <= (2 * 3) + 1 by XREAL_1:8;
hence contradiction by A35, GLIB_001:113; :: thesis: verum
end;
P .vertexAt j = P . j by A15, GLIB_001:def 8;
then P . j in P .vertices() by A16, A13, A14, GLIB_001:90, XXREAL_0:2;
then (Q .cut (jj,lP2)) .first() in P .vertices() by A7, A13, A14, A28, XXREAL_0:2;
then A37: not Q .cut (jj,lP2) is closed by A3, A20, GLIB_001:def 24;
then (Q .cut (jj,lP2)) .addEdge e is Cycle-like by A17, A34, A29, A20, Th33, GLIB_000:17;
then (Q .cut (jj,lP2)) .addEdge e is chordal by A36, Def11;
then consider m, n being odd Nat such that
A38: m + 2 < n and
A39: n <= len ((Q .cut (jj,lP2)) .addEdge e) and
A40: ((Q .cut (jj,lP2)) .addEdge e) . m <> ((Q .cut (jj,lP2)) .addEdge e) . n and
A41: ex e being set st e Joins ((Q .cut (jj,lP2)) .addEdge e) . m,((Q .cut (jj,lP2)) .addEdge e) . n,G and
A42: ( (Q .cut (jj,lP2)) .addEdge e is Cycle-like implies ( ( not m = 1 or not n = len ((Q .cut (jj,lP2)) .addEdge e) ) & ( not m = 1 or not n = (len ((Q .cut (jj,lP2)) .addEdge e)) - 2 ) & ( not m = 3 or not n = len ((Q .cut (jj,lP2)) .addEdge e) ) ) ) by Th84;
consider e being set such that
A43: e Joins ((Q .cut (jj,lP2)) .addEdge e) . m,((Q .cut (jj,lP2)) .addEdge e) . n,G by A41;
1 <= m by Th2;
then 1 - 1 <= m - 1 by XREAL_1:11;
then reconsider m1 = m - 1 as even Element of NAT by INT_1:16;
reconsider m1 = m1 as even Nat ;
A44: len ((Q .cut (jj,lP2)) .addEdge e) = (len (Q .cut (jj,lP2))) + 2 by A17, A20, GLIB_000:17, GLIB_001:65;
then m + 2 < (len (Q .cut (jj,lP2))) + 2 by A38, A39, XXREAL_0:2;
then A45: (m + 2) - 2 < ((len (Q .cut (jj,lP2))) + 2) - 2 by XREAL_1:11;
then A46: m1 < (len (Q .cut (jj,lP2))) - 1 by XREAL_1:11;
then A47: (Q .cut (jj,lP2)) . (m1 + 1) = P . (j + m1) by A22;
A48: j + m1 in dom P by A22, A46;
then A49: j + m1 <= len P by FINSEQ_3:27;
A50: ((Q .cut (jj,lP2)) .addEdge e) .last() = Q . j by A28, A30, GLIB_001:64;
now
assume A51: n = len ((Q .cut (jj,lP2)) .addEdge e) ; :: thesis: contradiction
then e Joins P . (j + m1),Q . j,G by A31, A50, A43, A45, A47;
then e Joins P . (j + m1),P . j,G by A7, A13, A14, XXREAL_0:2;
then A52: e Joins P . j,P . (j + m1),G by GLIB_000:17;
then A53: (2 + 1) - 1 < m - 1 by XREAL_1:11;
then A54: j < j + m1 by XREAL_1:31;
j + 2 < j + m1 by A53, XREAL_1:10;
hence contradiction by A1, A2, A49, A52, A54, Th92; :: thesis: verum
end;
then n < (len (Q .cut (jj,lP2))) + (2 * 1) by A44, A39, XXREAL_0:1;
then A55: n <= ((len (Q .cut (jj,lP2))) + 2) - 2 by Th3;
then A56: ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n by A31;
1 <= n by Th2;
then 1 - 1 <= n - 1 by XREAL_1:11;
then reconsider n1 = n - 1 as even Element of NAT by INT_1:16;
reconsider n1 = n1 as even Nat ;
(m + 2) - 1 < n - 1 by A38, XREAL_1:11;
then j + (m1 + 2) < j + n1 by XREAL_1:10;
then A57: (j + m1) + 2 < j + n1 ;
now
((Q .cut (jj,lP2)) .addEdge e) . m = (Q .cut (jj,lP2)) . m by A31, A45;
then A58: ((Q .cut (jj,lP2)) .addEdge e) . m = Q . (j + m1) by A7, A47, A49;
A59: len P < (len P) + 2 by XREAL_1:31;
j + m1 <= len P by A48, FINSEQ_3:27;
then consider kk being Nat such that
A60: (j + m1) + (2 * kk) = (len P) + 2 by A59, Lm2, XXREAL_0:2;
assume A61: n = len (Q .cut (jj,lP2)) ; :: thesis: contradiction
A62: now
assume 2 * kk < 3 + 1 ; :: thesis: contradiction
then 2 * kk <= 3 by NAT_1:13;
then ( 2 * kk = 0 or 2 * kk = 2 ) by Th11;
hence contradiction by A21, A38, A40, A61, A60; :: thesis: verum
end;
1 <= m by Th2;
then 1 < m by A34, A37, A30, A44, A42, A61, Th33, XXREAL_0:1;
then A63: 1 - 1 < m - 1 by XREAL_1:11;
A64: now
assume 2 * kk > (len P) + 1 ; :: thesis: contradiction
then 2 * kk >= ((len P) + 1) + 1 by NAT_1:13;
hence contradiction by A60, XREAL_1:31; :: thesis: verum
end;
A65: now
assume kk >= k ; :: thesis: contradiction
then A66: 2 * kk >= 2 * k by XREAL_1:66;
(j + (2 * kk)) + m1 > j + (2 * kk) by A63, XREAL_1:31;
hence contradiction by A12, A60, A66, XREAL_1:9; :: thesis: verum
end;
((Q .cut (jj,lP2)) .addEdge e) . n = x by A20, A31, A61;
hence contradiction by A10, A43, A60, A62, A64, A65, A58; :: thesis: verum
end;
then n < len (Q .cut (jj,lP2)) by A55, XXREAL_0:1;
then A67: n1 < (len (Q .cut (jj,lP2))) - 1 by XREAL_1:11;
then j + n1 in dom P by A22;
then A68: j + n1 <= len P by FINSEQ_3:27;
m < m + 2 by XREAL_1:31;
then m < n by A38, XXREAL_0:2;
then m1 < n1 by XREAL_1:11;
then A69: j + m1 < j + n1 by XREAL_1:10;
A70: ((Q .cut (jj,lP2)) .addEdge e) . m = (Q .cut (jj,lP2)) . m by A31, A45;
(Q .cut (jj,lP2)) . (n1 + 1) = P . (j + n1) by A22, A67;
hence contradiction by A1, A2, A43, A47, A68, A70, A56, A69, A57, Th92; :: thesis: verum
end;
end;
end;
then A71: for k being Nat st ( for a being Nat st a < k holds
S1[a] ) holds
S1[k] ;
A72: for k being Nat holds S1[k] from NAT_1:sch 4(A71);
A73: now
let n be odd Nat; :: thesis: ( n <= (len P) - 2 implies for e being set holds not e Joins Q . n,x,G )
assume A74: n <= (len P) - 2 ; :: thesis: for e being set holds not e Joins Q . n,x,G
(len P) - 2 <= ((len P) - 2) + 4 by XREAL_1:33;
then consider k being Nat such that
A75: n + (2 * k) = (len P) + 2 by A74, Lm2, XXREAL_0:2;
A76: now
assume 2 * k > (len P) + 1 ; :: thesis: contradiction
then n + (2 * k) > 1 + ((len P) + 1) by Th2, XREAL_1:10;
hence contradiction by A75; :: thesis: verum
end;
now
assume A77: 2 * k < 4 ; :: thesis: contradiction
n + 4 <= ((len P) - 2) + 4 by A74, XREAL_1:9;
hence contradiction by A75, A77, XREAL_1:10; :: thesis: verum
end;
hence for e being set holds not e Joins Q . n,x,G by A72, A75, A76; :: thesis: verum
end;
A78: now
assume Q is chordal ; :: thesis: contradiction
then consider m, n being odd Nat such that
A79: m + 2 < n and
A80: n <= len Q and
Q . m <> Q . n and
A81: ex e being set st e Joins Q . m,Q . n,G and
( Q is Cycle-like implies ( ( not m = 1 or not n = len Q ) & ( not m = 1 or not n = (len Q) - 2 ) & ( not m = 3 or not n = len Q ) ) ) by Th84;
m + 2 < (len P) + 2 by A6, A79, A80, XXREAL_0:2;
then A82: (m + 2) - 2 < ((len P) + 2) - 2 by XREAL_1:11;
m < m + 2 by XREAL_1:31;
then A83: m < n by A79, XXREAL_0:2;
per cases ( n = len Q or n < len Q ) by A80, XXREAL_0:1;
suppose A84: n = len Q ; :: thesis: contradiction
then (m + 2) - 2 < ((len P) + 2) - 2 by A6, A79, XREAL_1:11;
hence contradiction by A9, A73, A81, A84, Th3; :: thesis: verum
end;
suppose A85: n < len Q ; :: thesis: contradiction
A86: Q . m = P . m by A7, A82;
A87: n <= ((len P) + 2) - 2 by A6, A85, Th3;
then Q . n = P . n by A7;
hence contradiction by A1, A2, A79, A81, A83, A87, A86, Th92; :: thesis: verum
end;
end;
end;
Q .first() = P .first() by A4, GLIB_001:64;
then Q .first() in P .vertices() by GLIB_001:89;
hence ( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal ) by A3, A9, A78, GLIB_001:def 24; :: thesis: verum