let G be chordal _Graph; for P being Path of G st P is open & P is chordless holds
for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )
let P be Path of G; ( P is open & P is chordless implies for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless ) )
assume that
A1:
P is open
and
A2:
P is chordless
; for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )
let x, e be object ; ( not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) implies ( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless ) )
assume that
A3:
not x in P .vertices()
and
A4:
e Joins P .last() ,x,G
and
A5:
for f being object holds not f Joins P . ((len P) - 2),x,G
; ( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )
reconsider Q = P .addEdge e as Path of G by A1, A3, A4, GLIB_001:151;
A6:
len Q = (len P) + 2
by A4, GLIB_001:64;
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 object holds not e Joins Q . j,x,G );
A9:
Q .last() = x
by A4, GLIB_001:63;
for k being Nat st ( for a being Nat st a < k holds
S1[a] ) holds
S1[k]
proof
let k be
Nat;
( ( 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]
;
S1[k]
assume that A11:
4
<= 2
* k
and
2
* k <= (len P) + 1
;
for j being odd Nat st j + (2 * k) = (len P) + 2 holds
for e being object holds not e Joins Q . j,x,G
let j be
odd Nat;
( j + (2 * k) = (len P) + 2 implies for e being object holds not e Joins Q . j,x,G )
assume A12:
j + (2 * k) = (len P) + 2
;
for e being object holds not e Joins Q . j,x,G
j + 4
<= j + (2 * k)
by A11, XREAL_1:7;
then A13:
(j + 4) - 4
<= ((len P) + 2) - 4
by A12, XREAL_1:9;
A14:
(len P) - 2
<= len P
by XREAL_1:43;
then A15:
j <= len P
by A13, XXREAL_0:2;
A16:
j in NAT
by ORDINAL1:def 12;
let e be
object ;
not e Joins Q . j,x,G
assume A17:
e Joins Q . j,
x,
G
;
contradiction
per cases
( j = (len P) - 2 or j < (len P) - (2 * 1) )
by A13, XXREAL_0:1;
suppose A18:
j < (len P) - (2 * 1)
;
contradictionreconsider lP2 =
(len P) + 2 as
odd Element of
NAT ;
reconsider jj =
j as
odd Element of
NAT by ORDINAL1:def 12;
set B =
Q .cut (
jj,
lP2);
len P < (len P) + 2
by XREAL_1:29;
then A19:
j <= (len P) + 2
by A15, XXREAL_0:2;
then A20:
(Q .cut (jj,lP2)) .last() = x
by A9, A6, GLIB_001:37;
A21:
(len (Q .cut (jj,lP2))) + j = ((len P) + 2) + 1
by A6, A19, GLIB_001:36;
A22:
now for i being even Nat st i < (len (Q .cut (jj,lP2))) - 1 holds
( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P )let i be
even Nat;
( 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
;
( (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:8;
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:44;
then A25:
i < len (Q .cut (jj,lP2))
by A23, XXREAL_0:2;
A26:
i in NAT
by ORDINAL1:def 12;
then
j + i in dom Q
by A6, A19, A25, GLIB_001:36;
then A27:
1
<= j + i
by FINSEQ_3:25;
(Q .cut (jj,lP2)) . (i + 1) = Q . (j + i)
by A6, A19, A26, A25, GLIB_001:36;
hence
(
(Q .cut (jj,lP2)) . (i + 1) = P . (j + i) &
j + i in dom P )
by A7, A27, A24, FINSEQ_3:25;
verum end; set C =
(Q .cut (jj,lP2)) .addEdge e;
A28:
(Q .cut (jj,lP2)) .first() = Q . j
by A6, A19, GLIB_001:37;
A29:
(Q .cut (jj,lP2)) .first() = Q . j
by A6, A19, GLIB_001:37;
then A30:
e Joins (Q .cut (jj,lP2)) .last() ,
(Q .cut (jj,lP2)) .first() ,
G
by A17, A20;
A31:
now for n being odd Nat st n <= len (Q .cut (jj,lP2)) holds
((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . nlet n be
odd Nat;
( 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))
;
((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:25;
hence
((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n
by A30, GLIB_001:65;
verum end; A33:
((len P) + 3) - ((len P) - 2) < ((len P) + 3) - j
by A18, XREAL_1:15;
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:8;
then A35:
len ((Q .cut (jj,lP2)) .addEdge e) > 7
by A17, A20, GLIB_000:14, GLIB_001:64;
P .vertexAt j = P . j
by A15, GLIB_001:def 8;
then
P . j in P .vertices()
by A16, A13, A14, GLIB_001:89, XXREAL_0:2;
then
(Q .cut (jj,lP2)) .first() in P .vertices()
by A7, A13, A14, A28, XXREAL_0:2;
then A37:
Q .cut (
jj,
lP2) is
open
by A3, A20;
then
(Q .cut (jj,lP2)) .addEdge e is
Cycle-like
by A17, A34, A29, A20, Th33, GLIB_000:14;
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
object 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 Th83;
consider e being
object 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:9;
then reconsider m1 =
m - 1 as
even Element of
NAT by INT_1:3;
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:14, GLIB_001:64;
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:9;
then A46:
m1 < (len (Q .cut (jj,lP2))) - 1
by XREAL_1:9;
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:25;
A50:
((Q .cut (jj,lP2)) .addEdge e) .last() = Q . j
by A28, A30, GLIB_001:63;
now not n = len ((Q .cut (jj,lP2)) .addEdge e)assume A51:
n = len ((Q .cut (jj,lP2)) .addEdge e)
;
contradictionthen
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
;
3
< m
by A17, A34, A29, A20, A37, A42, A51, Th7, Th33, GLIB_000:14, XXREAL_0:2;
then A53:
(2 + 1) - 1
< m - 1
by XREAL_1:9;
then A54:
j < j + m1
by XREAL_1:29;
j + 2
< j + m1
by A53, XREAL_1:8;
hence
contradiction
by A1, A2, A49, A52, A54, Th91;
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:9;
then reconsider n1 =
n - 1 as
even Element of
NAT by INT_1:3;
reconsider n1 =
n1 as
even Nat ;
(m + 2) - 1
< n - 1
by A38, XREAL_1:9;
then
j + (m1 + 2) < j + n1
by XREAL_1:8;
then A57:
(j + m1) + 2
< j + n1
;
now not n = len (Q .cut (jj,lP2))
((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:29;
j + m1 <= len P
by A48, FINSEQ_3:25;
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))
;
contradictionA62:
now not 2 * kk < 3 + 1end;
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:9;
((Q .cut (jj,lP2)) .addEdge e) . n = x
by A20, A31, A61;
hence
contradiction
by A10, A43, A60, A62, A64, A65, A58;
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:9;
then
j + n1 in dom P
by A22;
then A68:
j + n1 <= len P
by FINSEQ_3:25;
m < m + 2
by XREAL_1:29;
then
m < n
by A38, XXREAL_0:2;
then
m1 < n1
by XREAL_1:9;
then A69:
j + m1 < j + n1
by XREAL_1:8;
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, Th91;
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 for n being odd Nat st n <= (len P) - 2 holds
for e being object holds not e Joins Q . n,x,Glet n be
odd Nat;
( n <= (len P) - 2 implies for e being object holds not e Joins Q . n,x,G )assume A74:
n <= (len P) - 2
;
for e being object holds not e Joins Q . n,x,G
(len P) - 2
<= ((len P) - 2) + 4
by XREAL_1:31;
then consider k being
Nat such that A75:
n + (2 * k) = (len P) + 2
by A74, Lm2, XXREAL_0:2;
hence
for
e being
object holds not
e Joins Q . n,
x,
G
by A72, A75, A76;
verum end;
A78:
now not Q is chordal assume
Q is
chordal
;
contradictionthen 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
object 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 Th83;
m + 2
< (len P) + 2
by A6, A79, A80, XXREAL_0:2;
then A82:
(m + 2) - 2
< ((len P) + 2) - 2
by XREAL_1:9;
m < m + 2
by XREAL_1:29;
then A83:
m < n
by A79, XXREAL_0:2;
per cases
( n = len Q or n < len Q )
by A80, XXREAL_0:1;
suppose A85:
n < len Q
;
contradictionA86:
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, Th91;
verum end; end; end;
Q .first() = P .first()
by A4, GLIB_001:63;
then
Q .first() in P .vertices()
by GLIB_001:88;
hence
( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )
by A3, A9, A78; verum