:: The {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: Received July 2, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

begin

:: Facts that I could not find in MML.
theorem :: MYCIELSK:1
for x, y, z being real number st 0 <= x holds
x * (y -' z) = (x * y) -' (x * z)
proof end;

theorem Th2: :: MYCIELSK:2
for x, y, z being Nat holds
( x in y \ z iff ( z <= x & x < y ) )
proof end;

theorem Th3: :: MYCIELSK:3
for A, B, C, D, E, X being set st ( X c= A or X c= B or X c= C or X c= D or X c= E ) holds
X c= (((A \/ B) \/ C) \/ D) \/ E
proof end;

theorem Th4: :: MYCIELSK:4
for A, B, C, D, E, x being set holds
( x in (((A \/ B) \/ C) \/ D) \/ E iff ( x in A or x in B or x in C or x in D or x in E ) )
proof end;

theorem Th5: :: MYCIELSK:5
for R being symmetric RelStr
for x, y being set st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds
[y,x] in the InternalRel of R
proof end;

theorem Th6: :: MYCIELSK:6
for R being symmetric RelStr
for x, y being Element of R st x <= y holds
y <= x
proof end;

begin

theorem Th7: :: MYCIELSK:7
for X being set
for P being a_partition of X holds card P c= card X
proof end;

definition
let X be set ;
let P be a_partition of X;
let S be Subset of X;
func P | S -> a_partition of S equals :: MYCIELSK:def 1
 { (x /\ S) where x is Element of P : x meets S } ;
coherence
{ (x /\ S) where x is Element of P : x meets S } is a_partition of S
proof end;
end;

:: deftheorem defines | MYCIELSK:def 1 :
for X being set
for P being a_partition of X
for S being Subset of X holds P | S = { (x /\ S) where x is Element of P : x meets S } ;

registration
let X be set ;
cluster finite V89() for a_partition of X;
existence
ex b1 being a_partition of X st b1 is finite
proof end;
end;

registration
let X be set ;
let P be finite a_partition of X;
let S be Subset of X;
cluster P | S -> finite ;
coherence
P | S is finite
proof end;
end;

theorem Th8: :: MYCIELSK:8
for X being set
for P being finite a_partition of X
for S being Subset of X holds card (P | S) <= card P
proof end;

theorem Th9: :: MYCIELSK:9
for X being set
for P being finite a_partition of X
for S being Subset of X holds
( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
proof end;

theorem Th10: :: MYCIELSK:10
for R being RelStr
for C being Coloring of R
for S being Subset of R holds C | S is Coloring of (subrelstr S)
proof end;

begin

:: This section could be moved to DILWORTH or better yet to some
:: article with preliminaries where RelStr represents a graph.
:: But then some stuff from NECKLACE would have to be moved.
:: I decided not to move stuff around until there is much more
:: material and then a bigger reorganisation would be in place
:: 2009.08.06
definition
let R be RelStr ;
attr R is with_finite_chromatic# means :Def2: :: MYCIELSK:def 2
 ex C being Coloring of R st C is finite ;
end;

:: deftheorem Def2 defines with_finite_chromatic# MYCIELSK:def 2 :
for R being RelStr holds
( R is with_finite_chromatic# iff ex C being Coloring of R st C is finite );

registration
cluster with_finite_chromatic# for RelStr ;
existence
ex b1 being RelStr st b1 is with_finite_chromatic#
proof end;
end;

registration
cluster finite -> with_finite_chromatic# for RelStr ;
coherence
for b1 being RelStr st b1 is finite holds
b1 is with_finite_chromatic#
proof end;
end;

registration
let R be with_finite_chromatic# RelStr ;
cluster finite V89() StableSet-wise for a_partition of the carrier of R;
existence
ex b1 being Coloring of R st b1 is finite by Def2;
end;

registration
let R be with_finite_chromatic# RelStr ;
let S be Subset of R;
cluster subrelstr S -> with_finite_chromatic# ;
coherence
subrelstr S is with_finite_chromatic#
proof end;
end;

definition
let R be with_finite_chromatic# RelStr ;
func chromatic# R -> Nat means :Def3: :: MYCIELSK:def 3
( ex C being finite Coloring of R st card C = it & ( for C being finite Coloring of R holds it <= card C ) );
existence
ex b1 being Nat st
( ex C being finite Coloring of R st card C = b1 & ( for C being finite Coloring of R holds b1 <= card C ) )
proof end;
uniqueness
for b1, b2 being Nat st ex C being finite Coloring of R st card C = b1 & ( for C being finite Coloring of R holds b1 <= card C ) & ex C being finite Coloring of R st card C = b2 & ( for C being finite Coloring of R holds b2 <= card C ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines chromatic# MYCIELSK:def 3 :
for R being with_finite_chromatic# RelStr
for b2 being Nat holds
( b2 = chromatic# R iff ( ex C being finite Coloring of R st card C = b2 & ( for C being finite Coloring of R holds b2 <= card C ) ) );

registration
let R be empty RelStr ;
cluster chromatic# R -> empty ;
coherence
chromatic# R is empty
proof end;
end;

registration
let R be non empty with_finite_chromatic# RelStr ;
cluster chromatic# R -> positive ;
coherence
chromatic# R is positive
proof end;
end;

definition
let R be RelStr ;
attr R is with_finite_cliquecover# means :Def4: :: MYCIELSK:def 4
 ex C being Clique-partition of R st C is finite ;
end;

:: deftheorem Def4 defines with_finite_cliquecover# MYCIELSK:def 4 :
for R being RelStr holds
( R is with_finite_cliquecover# iff ex C being Clique-partition of R st C is finite );

registration
cluster with_finite_cliquecover# for RelStr ;
existence
ex b1 being RelStr st b1 is with_finite_cliquecover#
proof end;
end;

registration
cluster finite -> with_finite_cliquecover# for RelStr ;
coherence
for b1 being RelStr st b1 is finite holds
b1 is with_finite_cliquecover#
proof end;
end;

registration
let R be with_finite_cliquecover# RelStr ;
cluster finite V89() Clique-wise for a_partition of the carrier of R;
existence
ex b1 being Clique-partition of R st b1 is finite by Def4;
end;

registration
let R be with_finite_cliquecover# RelStr ;
let S be Subset of R;
cluster subrelstr S -> with_finite_cliquecover# ;
coherence
subrelstr S is with_finite_cliquecover#
proof end;
end;

definition
let R be with_finite_cliquecover# RelStr ;
func cliquecover# R -> Nat means :Def5: :: MYCIELSK:def 5
( ex C being finite Clique-partition of R st card C = it & ( for C being finite Clique-partition of R holds it <= card C ) );
existence
ex b1 being Nat st
( ex C being finite Clique-partition of R st card C = b1 & ( for C being finite Clique-partition of R holds b1 <= card C ) )
proof end;
uniqueness
for b1, b2 being Nat st ex C being finite Clique-partition of R st card C = b1 & ( for C being finite Clique-partition of R holds b1 <= card C ) & ex C being finite Clique-partition of R st card C = b2 & ( for C being finite Clique-partition of R holds b2 <= card C ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines cliquecover# MYCIELSK:def 5 :
for R being with_finite_cliquecover# RelStr
for b2 being Nat holds
( b2 = cliquecover# R iff ( ex C being finite Clique-partition of R st card C = b2 & ( for C being finite Clique-partition of R holds b2 <= card C ) ) );

registration
let R be empty RelStr ;
cluster cliquecover# R -> empty ;
coherence
cliquecover# R is empty
proof end;
end;

registration
let R be non empty with_finite_cliquecover# RelStr ;
cluster cliquecover# R -> positive ;
coherence
cliquecover# R is positive
proof end;
end;

:: Note: for empty RelStr clique# = 0, stability# = 0, chromatic# = 0,
:: cliquecover# = 0 follows from clusters.
theorem Th11: :: MYCIELSK:11
for R being finite RelStr holds clique# R <= card the carrier of R
proof end;

theorem :: MYCIELSK:12
for R being finite RelStr holds stability# R <= card the carrier of R
proof end;

theorem Th13: :: MYCIELSK:13
for R being finite RelStr holds chromatic# R <= card the carrier of R
proof end;

theorem :: MYCIELSK:14
for R being finite RelStr holds cliquecover# R <= card the carrier of R
proof end;

theorem Th15: :: MYCIELSK:15
for R being with_finite_clique# with_finite_chromatic# RelStr holds clique# R <= chromatic# R
proof end;

theorem :: MYCIELSK:16
for R being with_finite_stability# with_finite_cliquecover# RelStr holds stability# R <= cliquecover# R
proof end;

begin

theorem Th17: :: MYCIELSK:17
for R being RelStr
for x, y being Element of R
for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds
not a <= b
proof end;

theorem Th18: :: MYCIELSK:18
for R being RelStr
for x, y being Element of R
for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds
x <= y
proof end;

registration
let R be finite RelStr ;
cluster ComplRelStr R -> finite ;
coherence
ComplRelStr R is finite
proof end;
end;

theorem Th19: :: MYCIELSK:19
for R being symmetric RelStr
for C being Clique of R holds C is StableSet of (ComplRelStr R)
proof end;

theorem Th20: :: MYCIELSK:20
for R being symmetric RelStr
for C being Clique of (ComplRelStr R) holds C is StableSet of R
proof end;

theorem Th21: :: MYCIELSK:21
for R being RelStr
for C being StableSet of R holds C is Clique of (ComplRelStr R)
proof end;

theorem Th22: :: MYCIELSK:22
for R being RelStr
for C being StableSet of (ComplRelStr R) holds C is Clique of R
proof end;

registration
let R be with_finite_clique# RelStr ;
cluster ComplRelStr R -> with_finite_stability# ;
coherence
ComplRelStr R is with_finite_stability#
proof end;
end;

registration
let R be symmetric with_finite_stability# RelStr ;
cluster ComplRelStr R -> with_finite_clique# ;
coherence
ComplRelStr R is with_finite_clique#
proof end;
end;

theorem Th23: :: MYCIELSK:23
for R being symmetric with_finite_clique# RelStr holds clique# R = stability# (ComplRelStr R)
proof end;

theorem :: MYCIELSK:24
for R being symmetric with_finite_stability# RelStr holds stability# R = clique# (ComplRelStr R)
proof end;

theorem Th25: :: MYCIELSK:25
for R being RelStr
for C being Coloring of R holds C is Clique-partition of (ComplRelStr R)
proof end;

theorem Th26: :: MYCIELSK:26
for R being symmetric RelStr
for C being Clique-partition of (ComplRelStr R) holds C is Coloring of R
proof end;

theorem Th27: :: MYCIELSK:27
for R being symmetric RelStr
for C being Clique-partition of R holds C is Coloring of (ComplRelStr R)
proof end;

theorem Th28: :: MYCIELSK:28
for R being RelStr
for C being Coloring of (ComplRelStr R) holds C is Clique-partition of R
proof end;

registration
let R be with_finite_chromatic# RelStr ;
cluster ComplRelStr R -> with_finite_cliquecover# ;
coherence
ComplRelStr R is with_finite_cliquecover#
proof end;
end;

registration
let R be symmetric with_finite_cliquecover# RelStr ;
cluster ComplRelStr R -> with_finite_chromatic# ;
coherence
ComplRelStr R is with_finite_chromatic#
proof end;
end;

theorem Th29: :: MYCIELSK:29
for R being symmetric with_finite_chromatic# RelStr holds chromatic# R = cliquecover# (ComplRelStr R)
proof end;

theorem :: MYCIELSK:30
for R being symmetric with_finite_cliquecover# RelStr holds cliquecover# R = chromatic# (ComplRelStr R)
proof end;

begin

definition
let R be RelStr ;
let v be Element of R;
func Adjacent v -> Subset of R means :Def6: :: MYCIELSK:def 6
 for x being Element of R holds
( x in it iff ( x < v or v < x ) );
existence
ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff ( x < v or v < x ) )
proof end;
uniqueness
for b1, b2 being Subset of R st ( for x being Element of R holds
( x in b1 iff ( x < v or v < x ) ) ) & ( for x being Element of R holds
( x in b2 iff ( x < v or v < x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Adjacent MYCIELSK:def 6 :
for R being RelStr
for v being Element of R
for b3 being Subset of R holds
( b3 = Adjacent v iff for x being Element of R holds
( x in b3 iff ( x < v or v < x ) ) );

theorem Th31: :: MYCIELSK:31
for R being with_finite_chromatic# RelStr
for C being finite Coloring of R
for c being set st c in C & card C = chromatic# R holds
ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
proof end;

begin

definition
let n be Nat;
mode NatRelStr of n -> strict RelStr means :Def7: :: MYCIELSK:def 7
 the carrier of it = n;
existence
ex b1 being strict RelStr st the carrier of b1 = n
proof end;
end;

:: deftheorem Def7 defines NatRelStr MYCIELSK:def 7 :
for n being Nat
for b2 being strict RelStr holds
( b2 is NatRelStr of n iff the carrier of b2 = n );

registration
cluster -> empty for NatRelStr of 0 ;
coherence
for b1 being NatRelStr of 0 holds b1 is empty by Def7;
end;

registration
let n be non empty Nat;
cluster -> non empty for NatRelStr of n;
coherence
for b1 being NatRelStr of n holds not b1 is empty by Def7;
end;

registration
let n be Nat;
cluster -> finite for NatRelStr of n;
coherence
for b1 being NatRelStr of n holds b1 is finite by Def7;
cluster strict irreflexive for NatRelStr of n;
existence
ex b1 being NatRelStr of n st b1 is irreflexive
proof end;
end;

definition
let n be Nat;
func CompleteRelStr n -> NatRelStr of n means :Def8: :: MYCIELSK:def 8
 the InternalRel of it = [:n,n:] \ (id n);
existence
ex b1 being NatRelStr of n st the InternalRel of b1 = [:n,n:] \ (id n)
proof end;
uniqueness
for b1, b2 being NatRelStr of n st the InternalRel of b1 = [:n,n:] \ (id n) & the InternalRel of b2 = [:n,n:] \ (id n) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines CompleteRelStr MYCIELSK:def 8 :
for n being Nat
for b2 being NatRelStr of n holds
( b2 = CompleteRelStr n iff the InternalRel of b2 = [:n,n:] \ (id n) );

theorem Th32: :: MYCIELSK:32
for n being Nat
for x, y being set st x in n & y in n holds
( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y )
proof end;

registration
let n be Nat;
cluster CompleteRelStr n -> symmetric irreflexive ;
coherence
( CompleteRelStr n is irreflexive & CompleteRelStr n is symmetric )
proof end;
end;

registration
let n be Nat;
cluster [#] (CompleteRelStr n) -> clique ;
coherence
[#] (CompleteRelStr n) is connected
proof end;
end;

theorem Th33: :: MYCIELSK:33
for n being Nat holds clique# (CompleteRelStr n) = n
proof end;

theorem :: MYCIELSK:34
for n being non empty Nat holds stability# (CompleteRelStr n) = 1
proof end;

theorem Th35: :: MYCIELSK:35
for n being Nat holds chromatic# (CompleteRelStr n) = n
proof end;

theorem :: MYCIELSK:36
for n being non empty Nat holds cliquecover# (CompleteRelStr n) = 1
proof end;

begin

definition
let n be Nat;
let R be NatRelStr of n;
:: Note: no assumptions about R
func Mycielskian R -> NatRelStr of (2 * n) + 1 means :Def9: :: MYCIELSK:def 9
 the InternalRel of it = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:];
existence
ex b1 being NatRelStr of (2 * n) + 1 st the InternalRel of b1 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:]
proof end;
uniqueness
for b1, b2 being NatRelStr of (2 * n) + 1 st the InternalRel of b1 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] & the InternalRel of b2 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Mycielskian MYCIELSK:def 9 :
for n being Nat
for R being NatRelStr of n
for b3 being NatRelStr of (2 * n) + 1 holds
( b3 = Mycielskian R iff the InternalRel of b3 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] );

theorem Th37: :: MYCIELSK:37
for n being Nat
for R being NatRelStr of n holds the carrier of R c= the carrier of (Mycielskian R)
proof end;

theorem Th38: :: MYCIELSK:38
for n being Nat
for R being NatRelStr of n
for x, y being Nat holds
( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) )
proof end;

theorem Th39: :: MYCIELSK:39
for n being Nat
for R being NatRelStr of n holds the InternalRel of R c= the InternalRel of (Mycielskian R)
proof end;

theorem Th40: :: MYCIELSK:40
for n being Nat
for R being NatRelStr of n
for x, y being set st x in n & y in n & [x,y] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
proof end;

theorem Th41: :: MYCIELSK:41
for n being Nat
for R being NatRelStr of n
for x, y being Nat st [x,y] in the InternalRel of R holds
( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) )
proof end;

theorem Th42: :: MYCIELSK:42
for n being Nat
for R being NatRelStr of n
for x, y being Nat st x in n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
proof end;

theorem Th43: :: MYCIELSK:43
for n being Nat
for R being NatRelStr of n
for x, y being Nat st y in n & [(x + n),y] in the InternalRel of (Mycielskian R) holds
[x,y] in the InternalRel of R
proof end;

theorem Th44: :: MYCIELSK:44
for n being Nat
for R being NatRelStr of n
for m being Nat st n <= m & m < 2 * n holds
( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )
proof end;

theorem Th45: :: MYCIELSK:45
for n being Nat
for R being NatRelStr of n
for S being Subset of (Mycielskian R) st S = n holds
R = subrelstr S
proof end;

theorem Th46: :: MYCIELSK:46
for n being Nat
for R being irreflexive NatRelStr of n st 2 <= clique# R holds
clique# R = clique# (Mycielskian R)
proof end;

theorem Th47: :: MYCIELSK:47
for R being with_finite_chromatic# RelStr
for S being Subset of R holds chromatic# R >= chromatic# (subrelstr S)
proof end;

theorem Th48: :: MYCIELSK:48
for n being Nat
for R being irreflexive NatRelStr of n holds chromatic# (Mycielskian R) = 1 + (chromatic# R)
proof end;

Lm1: now :: thesis: for myc1, myc2 being Function st dom myc1 = NAT & myc1 . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds
myc1 . (k + 1) = Mycielskian R ) & dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds
myc2 . (k + 1) = Mycielskian R ) holds
myc1 = myc2
let myc1, myc2 be Function; :: thesis: ( dom myc1 = NAT & myc1 . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds
myc1 . (k + 1) = Mycielskian R ) & dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds
myc2 . (k + 1) = Mycielskian R ) implies myc1 = myc2 )
assume that
A1: dom myc1 = NAT and
A2: myc1 . 0 = CompleteRelStr 2 and
A3: for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds
myc1 . (k + 1) = Mycielskian R and
A4: dom myc2 = NAT and
A5: myc2 . 0 = CompleteRelStr 2 and
A6: for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds
myc2 . (k + 1) = Mycielskian R ; :: thesis: myc1 = myc2
defpred S1[ Nat] means ( myc1 . $1 is NatRelStr of (3 * (2 |^ $1)) -' 1 & myc1 . $1 = myc2 . $1 );
(3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:4
.= (2 + 1) -' 1
.= 2 by NAT_D:34 ;
then A7: S1[ 0 ] by A2, A5;
A8: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: S1[k + 1]
reconsider R = myc1 . k as NatRelStr of (3 * (2 |^ k)) -' 1 by A9;
A10: myc1 . (k + 1) = Mycielskian R by A3;
A11: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NAT_1:11, NEWTON:85;
then 2 |^ k >= 1 by XXREAL_0:2;
then A12: 3 * (2 |^ k) >= 1 by A11, XXREAL_0:2;
then A13: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:9;
2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
then 2 |^ (k + 1) >= 2 |^ k by NEWTON:6;
then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:64;
then 3 * (2 |^ (k + 1)) >= 1 by A12, XXREAL_0:2;
then A14: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:9;
(2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by A13, XREAL_0:def 2
.= ((3 * (2 * (2 |^ k))) - 2) + 1
.= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:6
.= (3 * (2 |^ (k + 1))) -' 1 by A14, XREAL_0:def 2 ;
hence S1[k + 1] by A10, A9, A6; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A7, A8);
then for x being set st x in dom myc1 holds
myc1 . x = myc2 . x by A1;
hence myc1 = myc2 by A1, A4, FUNCT_1:2; :: thesis: verum
end;

definition
let n be Nat;
func Mycielskian n -> NatRelStr of (3 * (2 |^ n)) -' 1 means :Def10: :: MYCIELSK:def 10
 ex myc being Function st
( it = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) );
existence
ex b1 being NatRelStr of (3 * (2 |^ n)) -' 1 ex myc being Function st
( b1 = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) )
proof end;
uniqueness
for b1, b2 being NatRelStr of (3 * (2 |^ n)) -' 1 st ex myc being Function st
( b1 = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) ) & ex myc being Function st
( b2 = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) ) holds
b1 = b2 by Lm1;
end;

:: deftheorem Def10 defines Mycielskian MYCIELSK:def 10 :
for n being Nat
for b2 being NatRelStr of (3 * (2 |^ n)) -' 1 holds
( b2 = Mycielskian n iff ex myc being Function st
( b2 = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) ) );

theorem Th49: :: MYCIELSK:49
( Mycielskian 0 = CompleteRelStr 2 & ( for k being Nat holds Mycielskian (k + 1) = Mycielskian (Mycielskian k) ) )
proof end;

registration
let n be Nat;
cluster Mycielskian n -> irreflexive ;
coherence
Mycielskian n is irreflexive
proof end;
end;

registration
let n be Nat;
cluster Mycielskian n -> symmetric ;
coherence
Mycielskian n is symmetric
proof end;
end;

theorem Th50: :: MYCIELSK:50
for n being Nat holds
( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) = n + 2 )
proof end;

theorem :: MYCIELSK:51
for n being Nat ex R being finite RelStr st
( clique# R = 2 & chromatic# R > n )
proof end;

theorem :: MYCIELSK:52
for n being Nat ex R being finite RelStr st
( stability# R = 2 & cliquecover# R > n )
proof end;