defpred S1[ finite _Graph] means ( G is chordal implies ex S being VertexScheme of G st S is perfect );
A1:
now let k be non
zero Nat;
:: thesis: ( ( for Gk being finite _Graph st Gk .order() < k holds
S1[Gk] ) implies for Gk1 being finite _Graph st Gk1 .order() = k holds
S1[Gk1] )assume A2:
for
Gk being
finite _Graph st
Gk .order() < k holds
S1[
Gk]
;
:: thesis: for Gk1 being finite _Graph st Gk1 .order() = k holds
S1[Gk1]let Gk1 be
finite _Graph;
:: thesis: ( Gk1 .order() = k implies S1[Gk1] )assume A3:
Gk1 .order() = k
;
:: thesis: S1[Gk1]thus
S1[
Gk1]
:: thesis: verumproof
assume A4:
Gk1 is
chordal
;
:: thesis: ex S being VertexScheme of Gk1 st S is perfect
per cases
( k = 1 or k <> 1 )
;
suppose
k <> 1
;
:: thesis: ex S being VertexScheme of Gk1 st S is perfect then reconsider G =
Gk1 as
finite non
trivial chordal _Graph by A3, A4, GLIB_000:29;
consider x being
Vertex of
G such that A6:
x is
simplicial
by Th103;
consider H being
removeVertex of
G,
x;
A7:
not
(the_Vertices_of G) \ {x} is
empty
by GLIB_000:23;
then A8:
the_Vertices_of H = (the_Vertices_of G) \ {x}
by GLIB_000:def 39;
H .order() =
card ((the_Vertices_of G) \ {x})
by A7, GLIB_000:def 39
.=
(G .order() ) - (card {x})
by CARD_2:63
.=
k - 1
by A3, CARD_2:60
;
then
H .order() < k
by XREAL_1:148;
then consider T being
VertexScheme of
H such that A9:
T is
perfect
by A2;
set S =
<*x*> ^ T;
rng T = (the_Vertices_of G) \ {x}
by A8, Def12;
then
rng (<*x*> ^ T) = ((the_Vertices_of G) \ {x}) \/ (rng <*x*>)
by FINSEQ_1:44;
then
rng (<*x*> ^ T) = ((the_Vertices_of G) \ {x}) \/ {x}
by FINSEQ_1:55;
then
rng (<*x*> ^ T) = {x} \/ (the_Vertices_of G)
by XBOOLE_1:39;
then A10:
rng (<*x*> ^ T) = the_Vertices_of G
by XBOOLE_1:12;
then reconsider S =
<*x*> ^ T as
FinSequence of
the_Vertices_of G by FINSEQ_1:def 4;
{x} /\ (rng T) =
{x} /\ ((the_Vertices_of G) \ {x})
by A8, Def12
.=
({x} /\ (the_Vertices_of G)) \ {x}
by XBOOLE_1:49
.=
{x} \ {x}
by XBOOLE_1:28
.=
{}
by XBOOLE_1:37
;
then
{x} misses rng T
by XBOOLE_0:def 7;
then A11:
rng <*x*> misses rng T
by FINSEQ_1:55;
A12:
<*x*> is
one-to-one
by FINSEQ_3:102;
T is
one-to-one
by Def12;
then
S is
one-to-one
by A11, A12, FINSEQ_3:98;
then reconsider S =
S as
VertexScheme of
Gk1 by A10, Def12;
take
S
;
:: thesis: S is perfect let n be non
zero Nat;
:: according to CHORD:def 13 :: thesis: ( n <= len S implies for Gf being inducedSubgraph of Gk1,(S .followSet n)
for v being Vertex of Gf st v = S . n holds
v is simplicial )assume A13:
n <= len S
;
:: thesis: for Gf being inducedSubgraph of Gk1,(S .followSet n)
for v being Vertex of Gf st v = S . n holds
v is simplicial let Gf be
inducedSubgraph of
Gk1,
(S .followSet n);
:: thesis: for v being Vertex of Gf st v = S . n holds
v is simplicial let v be
Vertex of
Gf;
:: thesis: ( v = S . n implies v is simplicial )assume A14:
v = S . n
;
:: thesis: v is simplicial A15:
1
<= n
by NAT_1:14;
per cases
( 1 = n or 1 < n )
by A15, XXREAL_0:1;
suppose A18:
1
< n
;
:: thesis: v is simplicial then
1
+ (- 1) < n + (- 1)
by XREAL_1:10;
then reconsider n1 =
n - 1 as non
zero Element of
NAT by INT_1:16;
len <*x*> = 1
by FINSEQ_1:56;
then A19:
S . n = T . n1
by A13, A18, FINSEQ_1:37;
n + (- 1) <= (len S) + (- 1)
by A13, XREAL_1:9;
then
n1 <= ((len <*x*>) + (len T)) + (- 1)
by FINSEQ_1:35;
then A20:
n1 <= (1 + (len T)) + (- 1)
by FINSEQ_1:56;
A21:
T .followSet n1 = S .followSet (n1 + 1)
by Th17;
not
T .followSet n1 is
empty
by A20, Th107;
then
Gf is
inducedSubgraph of
H,
(T .followSet n1)
by A8, A21, Th30;
hence
v is
simplicial
by A9, A14, A19, A20, Def13;
:: thesis: verum end; end;
end; end;
for G being finite _Graph holds S1[G]
from CHORD:sch 1(A1);
then consider S being VertexScheme of G such that
A22:
S is perfect
;
take
S
; :: thesis: S is perfect
thus
S is perfect
by A22; :: thesis: verum