:: Dickson's lemma
:: by Gilbert Lee and Piotr Rudnicki
::
:: Copyright (c) 2002-2019 Association of Mizar Users

theorem Th1: :: DICKSON:1
for g being Function
for x being set st dom g = {x} holds
g = x .--> (g . x)
proof end;

theorem :: DICKSON:2
canceled;

::\$CT
theorem Th2: :: DICKSON:3
for X being infinite set ex f being sequence of X st f is one-to-one
proof end;

definition
let R be RelStr ;
let f be sequence of R;
attr f is ascending means :: DICKSON:def 1
for n being Element of NAT holds
( f . (n + 1) <> f . n & [(f . n),(f . (n + 1))] in the InternalRel of R );
end;

:: deftheorem defines ascending DICKSON:def 1 :
for R being RelStr
for f being sequence of R holds
( f is ascending iff for n being Element of NAT holds
( f . (n + 1) <> f . n & [(f . n),(f . (n + 1))] in the InternalRel of R ) );

definition
let R be RelStr ;
let f be sequence of R;
attr f is weakly-ascending means :: DICKSON:def 2
for n being Nat holds [(f . n),(f . (n + 1))] in the InternalRel of R;
end;

:: deftheorem defines weakly-ascending DICKSON:def 2 :
for R being RelStr
for f being sequence of R holds
( f is weakly-ascending iff for n being Nat holds [(f . n),(f . (n + 1))] in the InternalRel of R );

theorem Th3: :: DICKSON:4
for R being non empty transitive RelStr
for f being sequence of R st f is weakly-ascending holds
for i, j being Nat st i < j holds
f . i <= f . j
proof end;

theorem Th4: :: DICKSON:5
for R being non empty RelStr holds
( R is connected iff the InternalRel of R is_strongly_connected_in the carrier of R )
proof end;

theorem Th5: :: DICKSON:6
for L being RelStr
for Y, a being set holds
( ( the InternalRel of L -Seg a misses Y & a in Y ) iff a is_minimal_wrt Y, the InternalRel of L )
proof end;

theorem Th6: :: DICKSON:7
for L being non empty transitive antisymmetric RelStr
for x being Element of L
for a, N being set st a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L holds
a is_minimal_wrt N, the InternalRel of L
proof end;

definition
let R be RelStr ;
attr R is quasi_ordered means :: DICKSON:def 3
( R is reflexive & R is transitive );
end;

:: deftheorem defines quasi_ordered DICKSON:def 3 :
for R being RelStr holds
( R is quasi_ordered iff ( R is reflexive & R is transitive ) );

definition
let R be RelStr ;
assume A1: R is quasi_ordered ;
func EqRel R -> Equivalence_Relation of the carrier of R equals :Def4: :: DICKSON:def 4
the InternalRel of R /\ ( the InternalRel of R ~);
coherence
the InternalRel of R /\ ( the InternalRel of R ~) is Equivalence_Relation of the carrier of R
proof end;
end;

:: deftheorem Def4 defines EqRel DICKSON:def 4 :
for R being RelStr st R is quasi_ordered holds
EqRel R = the InternalRel of R /\ ( the InternalRel of R ~);

theorem Th7: :: DICKSON:8
for R being RelStr
for x, y being Element of R st R is quasi_ordered holds
( x in Class ((),y) iff ( x <= y & y <= x ) )
proof end;

definition
let R be RelStr ;
func <=E R -> Relation of (Class ()) means :Def5: :: DICKSON:def 5
for A, B being object holds
( [A,B] in it iff ex a, b being Element of R st
( A = Class ((),a) & B = Class ((),b) & a <= b ) );
existence
ex b1 being Relation of (Class ()) st
for A, B being object holds
( [A,B] in b1 iff ex a, b being Element of R st
( A = Class ((),a) & B = Class ((),b) & a <= b ) )
proof end;
uniqueness
for b1, b2 being Relation of (Class ()) st ( for A, B being object holds
( [A,B] in b1 iff ex a, b being Element of R st
( A = Class ((),a) & B = Class ((),b) & a <= b ) ) ) & ( for A, B being object holds
( [A,B] in b2 iff ex a, b being Element of R st
( A = Class ((),a) & B = Class ((),b) & a <= b ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines <=E DICKSON:def 5 :
for R being RelStr
for b2 being Relation of (Class ()) holds
( b2 = <=E R iff for A, B being object holds
( [A,B] in b2 iff ex a, b being Element of R st
( A = Class ((),a) & B = Class ((),b) & a <= b ) ) );

theorem Th8: :: DICKSON:9
for R being RelStr st R is quasi_ordered holds
<=E R partially_orders Class ()
proof end;

theorem :: DICKSON:10
for R being non empty RelStr st R is quasi_ordered & R is connected holds
<=E R linearly_orders Class ()
proof end;

definition
let R be Relation;
func R \~ -> Relation equals :: DICKSON:def 6
R \ (R ~);
correctness
coherence
R \ (R ~) is Relation
;
;
end;

:: deftheorem defines \~ DICKSON:def 6 :
for R being Relation holds R \~ = R \ (R ~);

registration
let R be Relation;
coherence
R \~ is asymmetric
proof end;
end;

definition
let X be set ;
let R be Relation of X;
:: original: \~
redefine func R \~ -> Relation of X;
coherence
R \~ is Relation of X
proof end;
end;

definition
let R be RelStr ;
func R \~ -> strict RelStr equals :: DICKSON:def 7
RelStr(# the carrier of R,( the InternalRel of R \~) #);
correctness
coherence
RelStr(# the carrier of R,( the InternalRel of R \~) #) is strict RelStr
;
;
end;

:: deftheorem defines \~ DICKSON:def 7 :
for R being RelStr holds R \~ = RelStr(# the carrier of R,( the InternalRel of R \~) #);

registration
let R be non empty RelStr ;
cluster R \~ -> non empty strict ;
coherence
not R \~ is empty
;
end;

registration
let R be transitive RelStr ;
coherence
R \~ is transitive
proof end;
end;

registration
let R be RelStr ;
coherence
proof end;
end;

theorem :: DICKSON:11
for R being non empty Poset
for x being Element of R holds Class ((),x) = {x}
proof end;

theorem :: DICKSON:12
for R being Relation holds
( R = R \~ iff R is asymmetric )
proof end;

theorem :: DICKSON:13
for R being Relation st R is transitive holds
R \~ is transitive
proof end;

theorem :: DICKSON:14
for R being Relation
for a, b being set st R is antisymmetric holds
( [a,b] in R \~ iff ( [a,b] in R & a <> b ) )
proof end;

theorem Th14: :: DICKSON:15
for R being RelStr st R is well_founded holds
R \~ is well_founded
proof end;

theorem Th15: :: DICKSON:16
for R being RelStr st R \~ is well_founded & R is antisymmetric holds
R is well_founded
proof end;

theorem Th16: :: DICKSON:17
for L being RelStr
for N being set
for x being Element of (L \~) holds
( x is_minimal_wrt N, the InternalRel of (L \~) iff ( x in N & ( for y being Element of L st y in N & [y,x] in the InternalRel of L holds
[x,y] in the InternalRel of L ) ) )
proof end;

:: Proposition 4.31 - see WELLFND1:15
:: Omitting Example 4.32, Exercise 4.33, Exercise 4.34
theorem :: DICKSON:18
for R, S being non empty RelStr
for m being Function of R,S st R is quasi_ordered & S is antisymmetric & S \~ is well_founded & ( for a, b being Element of R holds
( ( a <= b implies m . a <= m . b ) & ( m . a = m . b implies [a,b] in EqRel R ) ) ) holds
R \~ is well_founded
proof end;

definition
let R be non empty RelStr ;
let N be Subset of R;
func min-classes N -> Subset-Family of R means :Def8: :: DICKSON:def 8
for x being set holds
( x in it iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((),y)) /\ N ) );
existence
ex b1 being Subset-Family of R st
for x being set holds
( x in b1 iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((),y)) /\ N ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of R st ( for x being set holds
( x in b1 iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((),y)) /\ N ) ) ) & ( for x being set holds
( x in b2 iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((),y)) /\ N ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines min-classes DICKSON:def 8 :
for R being non empty RelStr
for N being Subset of R
for b3 being Subset-Family of R holds
( b3 = min-classes N iff for x being set holds
( x in b3 iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((),y)) /\ N ) ) );

theorem Th18: :: DICKSON:19
for R being non empty RelStr
for N being Subset of R
for x being set st R is quasi_ordered & x in min-classes N holds
for y being Element of (R \~) st y in x holds
y is_minimal_wrt N, the InternalRel of (R \~)
proof end;

theorem Th19: :: DICKSON:20
for R being non empty RelStr holds
( R \~ is well_founded iff for N being Subset of R st N <> {} holds
ex x being object st x in min-classes N )
proof end;

theorem Th20: :: DICKSON:21
for R being non empty RelStr
for N being Subset of R
for y being Element of (R \~) st y is_minimal_wrt N, the InternalRel of (R \~) holds
not min-classes N is empty
proof end;

theorem Th21: :: DICKSON:22
for R being non empty RelStr
for N being Subset of R
for x being set st x in min-classes N holds
not x is empty
proof end;

theorem Th22: :: DICKSON:23
for R being non empty RelStr st R is quasi_ordered holds
( ( R is connected & R \~ is well_founded ) iff for N being non empty Subset of R holds card () = 1 )
proof end;

theorem :: DICKSON:24
for R being non empty Poset holds
( the InternalRel of R well_orders the carrier of R iff for N being non empty Subset of R holds card () = 1 )
proof end;

definition
let R be RelStr ;
let N be Subset of R;
let B be set ;
pred B is_Dickson-basis_of N,R means :: DICKSON:def 9
( B c= N & ( for a being Element of R st a in N holds
ex b being Element of R st
( b in B & b <= a ) ) );
end;

:: deftheorem defines is_Dickson-basis_of DICKSON:def 9 :
for R being RelStr
for N being Subset of R
for B being set holds
( B is_Dickson-basis_of N,R iff ( B c= N & ( for a being Element of R st a in N holds
ex b being Element of R st
( b in B & b <= a ) ) ) );

theorem :: DICKSON:25
for R being RelStr holds {} is_Dickson-basis_of {} the carrier of R,R ;

theorem Th25: :: DICKSON:26
for R being non empty RelStr
for N being non empty Subset of R
for B being set st B is_Dickson-basis_of N,R holds
not B is empty
proof end;

definition
let R be RelStr ;
attr R is Dickson means :: DICKSON:def 10
for N being Subset of R ex B being set st
( B is_Dickson-basis_of N,R & B is finite );
end;

:: deftheorem defines Dickson DICKSON:def 10 :
for R being RelStr holds
( R is Dickson iff for N being Subset of R ex B being set st
( B is_Dickson-basis_of N,R & B is finite ) );

theorem Th26: :: DICKSON:27
for R being non empty RelStr st R \~ is well_founded & R is connected holds
R is Dickson
proof end;

theorem Th27: :: DICKSON:28
for R, S being RelStr st the InternalRel of R c= the InternalRel of S & R is Dickson & the carrier of R = the carrier of S holds
S is Dickson
proof end;

definition
let f be Function;
let b be set ;
assume that
A1: dom f = NAT and
A2: b in rng f ;
func f mindex b -> Element of NAT means :Def11: :: DICKSON:def 11
( f . it = b & ( for i being Element of NAT st f . i = b holds
it <= i ) );
existence
ex b1 being Element of NAT st
( f . b1 = b & ( for i being Element of NAT st f . i = b holds
b1 <= i ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st f . b1 = b & ( for i being Element of NAT st f . i = b holds
b1 <= i ) & f . b2 = b & ( for i being Element of NAT st f . i = b holds
b2 <= i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines mindex DICKSON:def 11 :
for f being Function
for b being set st dom f = NAT & b in rng f holds
for b3 being Element of NAT holds
( b3 = f mindex b iff ( f . b3 = b & ( for i being Element of NAT st f . i = b holds
b3 <= i ) ) );

definition
let R be non empty 1-sorted ;
let f be sequence of R;
let b be set ;
let m be Element of NAT ;
assume A1: ex j being Element of NAT st
( m < j & f . j = b ) ;
func f mindex (b,m) -> Element of NAT means :Def12: :: DICKSON:def 12
( f . it = b & m < it & ( for i being Element of NAT st m < i & f . i = b holds
it <= i ) );
existence
ex b1 being Element of NAT st
( f . b1 = b & m < b1 & ( for i being Element of NAT st m < i & f . i = b holds
b1 <= i ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st f . b1 = b & m < b1 & ( for i being Element of NAT st m < i & f . i = b holds
b1 <= i ) & f . b2 = b & m < b2 & ( for i being Element of NAT st m < i & f . i = b holds
b2 <= i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines mindex DICKSON:def 12 :
for R being non empty 1-sorted
for f being sequence of R
for b being set
for m being Element of NAT st ex j being Element of NAT st
( m < j & f . j = b ) holds
for b5 being Element of NAT holds
( b5 = f mindex (b,m) iff ( f . b5 = b & m < b5 & ( for i being Element of NAT st m < i & f . i = b holds
b5 <= i ) ) );

theorem Th28: :: DICKSON:29
for R being non empty RelStr st R is Dickson holds
for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j )
proof end;

theorem Th29: :: DICKSON:30
for R being RelStr
for N being Subset of R
for x being Element of (R \~) st R is quasi_ordered & x in N & ( the InternalRel of R -Seg x) /\ N c= Class ((),x) holds
x is_minimal_wrt N, the InternalRel of (R \~)
proof end;

theorem Th30: :: DICKSON:31
for R being non empty RelStr st R is quasi_ordered & ( for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j ) ) holds
for N being non empty Subset of R holds
( min-classes N is finite & not min-classes N is empty )
proof end;

theorem Th31: :: DICKSON:32
for R being non empty RelStr st R is quasi_ordered & ( for N being non empty Subset of R holds
( min-classes N is finite & not min-classes N is empty ) ) holds
R is Dickson
proof end;

theorem Th32: :: DICKSON:33
for R being non empty RelStr st R is quasi_ordered & R is Dickson holds
R \~ is well_founded
proof end;

theorem :: DICKSON:34
for R being non empty Poset
for N being non empty Subset of R st R is Dickson holds
ex B being set st
( B is_Dickson-basis_of N,R & ( for C being set st C is_Dickson-basis_of N,R holds
B c= C ) )
proof end;

definition
let R be non empty RelStr ;
let N be Subset of R;
assume A1: R is Dickson ;
func Dickson-bases (N,R) -> non empty Subset-Family of R means :Def13: :: DICKSON:def 13
for B being set holds
( B in it iff B is_Dickson-basis_of N,R );
existence
ex b1 being non empty Subset-Family of R st
for B being set holds
( B in b1 iff B is_Dickson-basis_of N,R )
proof end;
uniqueness
for b1, b2 being non empty Subset-Family of R st ( for B being set holds
( B in b1 iff B is_Dickson-basis_of N,R ) ) & ( for B being set holds
( B in b2 iff B is_Dickson-basis_of N,R ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines Dickson-bases DICKSON:def 13 :
for R being non empty RelStr
for N being Subset of R st R is Dickson holds
for b3 being non empty Subset-Family of R holds
( b3 = Dickson-bases (N,R) iff for B being set holds
( B in b3 iff B is_Dickson-basis_of N,R ) );

theorem Th34: :: DICKSON:35
for R being non empty RelStr
for s being sequence of R st R is Dickson holds
ex t being sequence of R st
( t is subsequence of s & t is weakly-ascending )
proof end;

theorem Th35: :: DICKSON:36
for R being RelStr st R is empty holds
R is Dickson
proof end;

theorem Th36: :: DICKSON:37
for M, N being RelStr st M is Dickson & N is Dickson & M is quasi_ordered & N is quasi_ordered holds
( [:M,N:] is quasi_ordered & [:M,N:] is Dickson )
proof end;

theorem Th37: :: DICKSON:38
for R, S being RelStr st R,S are_isomorphic & R is Dickson & R is quasi_ordered holds
( S is quasi_ordered & S is Dickson )
proof end;

theorem Th38: :: DICKSON:39
for p being RelStr-yielding ManySortedSet of
for z being Element of holds p . z, product p are_isomorphic
proof end;

registration
let X be set ;
let p be RelStr-yielding ManySortedSet of X;
let Y be Subset of X;
coherence
p | Y is RelStr-yielding
proof end;
end;

theorem Th39: :: DICKSON:40
for n being non zero Nat
for p being RelStr-yielding ManySortedSet of n holds
( not product p is empty iff p is non-Empty )
proof end;

theorem Th40: :: DICKSON:41
for n being non zero Nat
for p being RelStr-yielding ManySortedSet of Segm (n + 1)
for ns being Subset of (Segm (n + 1))
for ne being Element of Segm (n + 1) st ns = n & ne = n holds
[:(product (p | ns)),(p . ne):], product p are_isomorphic
proof end;

theorem Th41: :: DICKSON:42
for n being non zero Nat
for p being RelStr-yielding ManySortedSet of Segm n st ( for i being Element of Segm n holds
( p . i is Dickson & p . i is quasi_ordered ) ) holds
( product p is quasi_ordered & product p is Dickson )
proof end;

Lm1: for p being RelStr-yielding ManySortedSet of {} holds
( not product p is empty & product p is quasi_ordered & product p is Dickson & product p is antisymmetric )

proof end;

registration
let p be RelStr-yielding ManySortedSet of {} ;
cluster product p -> non empty ;
coherence
not product p is empty
by Lm1;
coherence by Lm1;
coherence by Lm1;
coherence by Lm1;
end;

definition
func NATOrd -> Relation of NAT equals :: DICKSON:def 14
{ [x,y] where x, y is Element of NAT : x <= y } ;
correctness
coherence
{ [x,y] where x, y is Element of NAT : x <= y } is Relation of NAT
;
proof end;
end;

:: deftheorem defines NATOrd DICKSON:def 14 :
NATOrd = { [x,y] where x, y is Element of NAT : x <= y } ;

theorem Th42: :: DICKSON:43

theorem Th43: :: DICKSON:44
proof end;

theorem Th44: :: DICKSON:45
proof end;

theorem Th45: :: DICKSON:46
proof end;

definition
func OrderedNAT -> non empty RelStr equals :: DICKSON:def 15
RelStr(# NAT,NATOrd #);
correctness
coherence
RelStr(# NAT,NATOrd #) is non empty RelStr
;
;
end;

:: deftheorem defines OrderedNAT DICKSON:def 15 :

Lm2: now :: thesis:
for x, y being Element of OrderedNAT st not x <= y holds
y <= x by Th44;
hence OrderedNAT is connected by WAYBEL_0:def 29; :: thesis: verum
end;

registration
coherence by Lm2;
coherence
proof end;
coherence
proof end;
coherence by Th43;
coherence by Th45;
coherence
proof end;
end;

Lm3: now :: thesis: for n being Element of NAT holds
( not product () is empty & product () is Dickson & product () is quasi_ordered & product () is antisymmetric )
let n be Element of NAT ; :: thesis: ( not product () is empty & product () is Dickson & product () is quasi_ordered & product () is antisymmetric )
set pp = product ();
per cases ( n is zero or not n is zero ) ;
suppose n is zero ; :: thesis: ( not product () is empty & product () is Dickson & product () is quasi_ordered & product () is antisymmetric )
then n = 0 ;
then n is empty ;
hence ( not product () is empty & product () is Dickson & product () is quasi_ordered & product () is antisymmetric ) ; :: thesis: verum
end;
suppose not n is zero ; :: thesis: ( not product () is empty & product () is Dickson & product () is quasi_ordered & product () is antisymmetric )
then reconsider n9 = n as non zero Element of NAT ;
reconsider p = n9 --> OrderedNAT as RelStr-yielding ManySortedSet of Segm n9 ;
thus not product () is empty ; :: thesis: ( product () is Dickson & product () is quasi_ordered & product () is antisymmetric )
for i being Element of Segm n9 holds
( p . i is Dickson & p . i is quasi_ordered ) ;
hence ( product () is Dickson & product () is quasi_ordered ) by Th41; :: thesis:
product p is antisymmetric ;
hence product () is antisymmetric ; :: thesis: verum
end;
end;
end;

registration
let n be Element of NAT ;
cluster product () -> non empty ;
coherence
not product () is empty
;
coherence
product () is Dickson
by Lm3;
coherence by Lm3;
coherence by Lm3;
end;

theorem :: DICKSON:47
for M being RelStr st M is Dickson & M is quasi_ordered holds
( is quasi_ordered & is Dickson ) by Th36;

:: Omitting Exercise 4.50
theorem Th47: :: DICKSON:48
for R, S being non empty RelStr st R is Dickson & S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds
S \~ is well_founded
proof end;

theorem :: DICKSON:49
for R being non empty RelStr st R is quasi_ordered holds
( R is Dickson iff for S being non empty RelStr st S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds
S \~ is well_founded )
proof end;