:: DICKSON semantic presentation

theorem Th1: :: DICKSON:1

for g being Function
for x being set st dom g = {x} holds
g = x .--> (g . x)

proof end;

theorem Th2: :: DICKSON:2

for n being Nat holds n c= n + 1

proof end;

scheme :: DICKSON:sch 1
FinSegRng2{ F₁() -> Nat, F₂() -> Nat, F₃( set ) -> set , P₁[ Nat] } :

{ F₃(i) where i is Nat : ( F₁() < i & i <= F₂() & P₁[i] ) } is finite

proof end;

theorem Th3: :: DICKSON:3

for X being infinite set ex f being Function of NAT ,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 Nat holds
( f . (n + 1) <> f . n & [(f . n),(f . (n + 1))] in the InternalRel of R );

end;

:: deftheorem defines ascending DICKSON:def 1 :

definition

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

end;

:: deftheorem Def2 defines weakly-ascending DICKSON:def 2 :

theorem Th4: :: 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 Th5: :: 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 :: DICKSON:6

canceled;

theorem Th7: :: DICKSON:7

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 Th8: :: DICKSON:8

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 :Def3: :: DICKSON:def 3
( R is reflexive & R is transitive );

end;

:: deftheorem Def3 defines quasi_ordered DICKSON:def 3 :

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

proof end;

end;

:: deftheorem Def4 defines EqRel DICKSON:def 4 :

theorem Th9: :: DICKSON:9

for R being RelStr
for x, y being Element of R st R is quasi_ordered holds
( x in Class (EqRel R),y iff ( x <= y & y <= x ) )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines <=E DICKSON:def 5 :

theorem Th10: :: DICKSON:10

for R being RelStr st R is quasi_ordered holds
<=E R partially_orders Class (EqRel R)

proof end;

theorem :: DICKSON:11

for R being non empty RelStr st R is quasi_ordered & R is connected holds
<=E R linearly_orders Class (EqRel R)

proof end;

definition

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

end;

:: deftheorem defines \~ DICKSON:def 6 :

registration

let R be Relation;
cluster R \~ -> asymmetric ;
coherence

proof end;

end;

definition

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

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 ;

end;

:: deftheorem defines \~ DICKSON:def 7 :

registration

let R be non empty RelStr ;
cluster R \~ -> non empty strict ;
coherence ;

end;

registration

let R be transitive RelStr ;
cluster R \~ -> strict transitive ;
coherence

proof end;

end;

registration

let R be RelStr ;
cluster R \~ -> strict antisymmetric ;
coherence

proof end;

end;

theorem :: DICKSON:12

for R being non empty Poset
for x being Element of R holds Class (EqRel R),x = {x}

proof end;

theorem :: DICKSON:13

for R being Relation holds
( R = R \~ iff R is asymmetric )

proof end;

theorem :: DICKSON:14

for R being Relation st R is transitive holds
R \~ is transitive

proof end;

theorem :: DICKSON:15

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 Th16: :: DICKSON:16

for R being RelStr st R is well_founded holds
R \~ is well_founded

proof end;

theorem Th17: :: DICKSON:17

for R being RelStr st R \~ is well_founded & R is antisymmetric holds
R is well_founded

proof end;

theorem Th18: :: DICKSON:18

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;

theorem :: DICKSON:19

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 (EqRel R),y) /\ N ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines min-classes DICKSON:def 8 :

theorem Th20: :: DICKSON:20

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 Th21: :: DICKSON:21

for R being non empty RelStr holds
( R \~ is well_founded iff for N being Subset of R st N <> {} holds
ex x being set st x in min-classes N )

proof end;

theorem Th22: :: DICKSON:22

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 Th23: :: DICKSON:23

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
not x is empty

proof end;

theorem Th24: :: DICKSON:24

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 (min-classes N) = 1 )

proof end;

theorem :: DICKSON:25

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 (min-classes N) = 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 :Def9: :: 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 Def9 defines is_Dickson-basis_of DICKSON:def 9 :

theorem Th26: :: DICKSON:26

for R being RelStr holds {} is_Dickson-basis_of {} the carrier of R,R

proof end;

theorem Th27: :: DICKSON:27

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 :Def10: :: 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 Def10 defines Dickson DICKSON:def 10 :

theorem Th28: :: DICKSON:28

for R being non empty RelStr st R \~ is well_founded & R is connected holds
R is Dickson

proof end;

theorem Th29: :: DICKSON:29

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 -> Nat means :Def11: :: DICKSON:def 11
( f . it = b & ( for i being Nat st f . i = b holds
it <= i ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines mindex DICKSON:def 11 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines mindex DICKSON:def 12 :

theorem Th30: :: DICKSON:30

for R being non empty RelStr st R is quasi_ordered & 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 Th31: :: DICKSON:31

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 (EqRel R),x holds
x is_minimal_wrt N,the InternalRel of (R \~ )

proof end;

theorem Th32: :: DICKSON:32

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 Th33: :: DICKSON:33

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 Th34: :: DICKSON:34

for R being non empty RelStr st R is quasi_ordered & R is Dickson holds
R \~ is well_founded

proof end;

theorem :: DICKSON:35

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Dickson-bases DICKSON:def 13 :

theorem Th36: :: DICKSON:36

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 Th37: :: DICKSON:37

for R being RelStr st R is empty holds
R is Dickson

proof end;

theorem Th38: :: DICKSON:38

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 Th39: :: DICKSON:39

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 Th40: :: DICKSON:40

for p being RelStr-yielding ManySortedSet of 1
for z being Element of 1 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;
cluster p | Y -> RelStr-yielding ;
coherence

proof end;

end;

theorem Th41: :: DICKSON:41

for n being non empty Nat
for p being RelStr-yielding ManySortedSet of n holds
( not product p is empty iff p is non-Empty )

proof end;

theorem Th42: :: DICKSON:42

for n being non empty Nat
for p being RelStr-yielding ManySortedSet of n + 1
for ns being Subset of (n + 1)
for ne being Element of n + 1 st ns = n & ne = n holds
[:(product (p | ns)),(p . ne):], product p are_isomorphic

proof end;

theorem Th43: :: DICKSON:43

for n being non empty Nat
for p being RelStr-yielding ManySortedSet of n st ( for i being Element of 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 by Lm1;
cluster product p -> antisymmetric ;
coherence by Lm1;
cluster product p -> quasi_ordered ;
coherence by Lm1;
cluster product p -> Dickson ;
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

proof end;

end;

:: deftheorem defines NATOrd DICKSON:def 14 :

theorem Th44: :: DICKSON:44

NATOrd is_reflexive_in NAT

proof end;

theorem Th45: :: DICKSON:45

NATOrd is_antisymmetric_in NAT

proof end;

theorem Th46: :: DICKSON:46

NATOrd is_strongly_connected_in NAT

proof end;

theorem Th47: :: DICKSON:47

NATOrd is_transitive_in NAT

proof end;

definition

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

end;

:: deftheorem defines OrderedNAT DICKSON:def 15 :

Lm2: now

now

let x, y be Element of OrderedNAT ; :: thesis:
assume not x <= y ; :: thesis:
then not [x,y] in NATOrd by ORDERS_2:def 9;
then [y,x] in NATOrd by Th46, RELAT_2:def 7;
hence y <= x by ORDERS_2:def 9; :: thesis:

end;

hence OrderedNAT is connected by WAYBEL_0:def 29; :: thesis:

end;

registration

cluster OrderedNAT -> non empty connected ;
coherence by Lm2;
cluster OrderedNAT -> non empty Dickson ;
coherence

proof end;

cluster OrderedNAT -> non empty quasi_ordered ;
coherence

proof end;

cluster OrderedNAT -> non empty antisymmetric ;
coherence by Th45, ORDERS_2:def 6;
cluster OrderedNAT -> non empty transitive ;
coherence by Th47, ORDERS_2:def 5;
cluster OrderedNAT -> non empty well_founded ;
coherence

proof end;

end;

Lm3: now

let n be Nat; :: thesis:
set pp = product (n --> OrderedNAT );

per cases ;

suppose n is empty ; :: thesis:

hence ( not product (n --> OrderedNAT ) is empty & product (n --> OrderedNAT ) is Dickson & product (n --> OrderedNAT ) is quasi_ordered & product (n --> OrderedNAT ) is antisymmetric ) by Lm1; :: thesis:

end;

suppose not n is empty ; :: thesis:

then reconsider n' = n as non empty Nat ;
set p = n' --> OrderedNAT ;
not product (n' --> OrderedNAT ) is empty ;
hence not product (n --> OrderedNAT ) is empty ; :: thesis:
for i being Element of n' holds
( (n' --> OrderedNAT ) . i is Dickson & (n' --> OrderedNAT ) . i is quasi_ordered ) by FUNCOP_1:13;
hence ( product (n --> OrderedNAT ) is Dickson & product (n --> OrderedNAT ) is quasi_ordered ) by Th43; :: thesis:
product (n' --> OrderedNAT ) is antisymmetric ;
hence product (n --> OrderedNAT ) is antisymmetric ; :: thesis:

end;

registration

let n be Nat;
cluster product (n --> OrderedNAT ) -> non empty ;
coherence by Lm3;
cluster product (n --> OrderedNAT ) -> Dickson ;
coherence by Lm3;
cluster product (n --> OrderedNAT ) -> quasi_ordered ;
coherence by Lm3;
cluster product (n --> OrderedNAT ) -> antisymmetric ;
coherence by Lm3;

end;

theorem :: DICKSON:48

for M being RelStr st M is Dickson & M is quasi_ordered holds
( [:M,OrderedNAT :] is quasi_ordered & [:M,OrderedNAT :] is Dickson ) by Th38;

theorem Th49: :: DICKSON:49

for R, S being non empty RelStr st R is Dickson & R is quasi_ordered & 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:50

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;