:: DICKSON semantic presentation

theorem Th1: :: DICKSON:1

for b₁ being Function
for b₂ being set st dom b₁ = {b₂} holds
b₁ = b₂ .--> (b₁ . b₂)

proof end;

theorem Th2: :: DICKSON:2

for b₁ being Nat holds b₁ c= b₁ + 1

proof end;

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

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

proof end;

theorem Th3: :: DICKSON:3

for b₁ being infinite set ex b₂ being Function of NAT ,b₁ st b₂ is one-to-one

proof end;

definition

let c₁ be RelStr ;
let c₂ be sequence of c₁;
attr a₂ is ascending means :: DICKSON:def 1
for b₁ being Nat holds
( a₂ . (b₁ + 1) <> a₂ . b₁ & [(a₂ . b₁),(a₂ . (b₁ + 1))] in the InternalRel of a₁ );

end;

:: deftheorem Def1 defines ascending DICKSON:def 1 :

definition

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

end;

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

theorem Th4: :: DICKSON:4

for b₁ being non empty transitive RelStr
for b₂ being sequence of b₁ st b₂ is weakly-ascending holds
for b₃, b₄ being Nat st b₃ < b₄ holds
b₂ . b₃ <= b₂ . b₄

proof end;

theorem Th5: :: DICKSON:5

for b₁ being non empty RelStr holds
( b₁ is connected iff the InternalRel of b₁ is_strongly_connected_in the carrier of b₁ )

proof end;

theorem Th6: :: DICKSON:6

canceled;

theorem Th7: :: DICKSON:7

for b₁ being RelStr
for b₂, b₃ being set holds
( ( the InternalRel of b₁ -Seg b₃ misses b₂ & b₃ in b₂ ) iff b₃ is_minimal_wrt b₂,the InternalRel of b₁ )

proof end;

theorem Th8: :: DICKSON:8

for b₁ being non empty transitive antisymmetric RelStr
for b₂ being Element of b₁
for b₃, b₄ being set st b₃ is_minimal_wrt (the InternalRel of b₁ -Seg b₂) /\ b₄,the InternalRel of b₁ holds
b₃ is_minimal_wrt b₄,the InternalRel of b₁

proof end;

definition

let c₁ be RelStr ;
attr a₁ is quasi_ordered means :Def3: :: DICKSON:def 3
( a₁ is reflexive & a₁ is transitive );

end;

:: deftheorem Def3 defines quasi_ordered DICKSON:def 3 :

definition

let c₁ be RelStr ;
assume E10: c₁ is quasi_ordered ;
func EqRel c₁ -> Equivalence_Relation of the carrier of a₁ equals :Def4: :: DICKSON:def 4
the InternalRel of a₁ /\ (the InternalRel of a₁ ~ );
coherence

proof end;

end;

:: deftheorem Def4 defines EqRel DICKSON:def 4 :

theorem Th9: :: DICKSON:9

for b₁ being RelStr
for b₂, b₃ being Element of b₁ st b₁ is quasi_ordered holds
( b₂ in Class (EqRel b₁),b₃ iff ( b₂ <= b₃ & b₃ <= b₂ ) )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

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

theorem Th10: :: DICKSON:10

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

proof end;

theorem Th11: :: DICKSON:11

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

proof end;

definition

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

end;

:: deftheorem Def6 defines \~ DICKSON:def 6 :

registration

let c₁ be Relation;
cluster a₁ \~ -> asymmetric ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Relation of c₁;
redefine func \~ as c₂ \~ -> Relation of a₁;
coherence

proof end;

end;

definition

let c₁ be RelStr ;
func c₁ \~ -> strict RelStr equals :: DICKSON:def 7
RelStr(# the carrier of a₁,(the InternalRel of a₁ \~ ) #);
correctness ;

end;

:: deftheorem Def7 defines \~ DICKSON:def 7 :

registration

let c₁ be non empty RelStr ;
cluster a₁ \~ -> non empty strict ;
coherence ;

end;

registration

let c₁ be transitive RelStr ;
cluster a₁ \~ -> strict transitive ;
coherence

proof end;

end;

registration

let c₁ be RelStr ;
cluster a₁ \~ -> strict antisymmetric ;
coherence

proof end;

end;

theorem Th12: :: DICKSON:12

for b₁ being non empty Poset
for b₂ being Element of b₁ holds Class (EqRel b₁),b₂ = {b₂}

proof end;

theorem Th13: :: DICKSON:13

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

proof end;

theorem Th14: :: DICKSON:14

for b₁ being Relation st b₁ is transitive holds
b₁ \~ is transitive

proof end;

theorem Th15: :: DICKSON:15

for b₁ being Relation
for b₂, b₃ being set st b₁ is antisymmetric holds
( [b₂,b₃] in b₁ \~ iff ( [b₂,b₃] in b₁ & b₂ <> b₃ ) )

proof end;

theorem Th16: :: DICKSON:16

for b₁ being RelStr st b₁ is well_founded holds
b₁ \~ is well_founded

proof end;

theorem Th17: :: DICKSON:17

for b₁ being RelStr st b₁ \~ is well_founded & b₁ is antisymmetric holds
b₁ is well_founded

proof end;

theorem Th18: :: DICKSON:18

for b₁ being RelStr
for b₂ being set
for b₃ being Element of (b₁ \~ ) holds
( b₃ is_minimal_wrt b₂,the InternalRel of (b₁ \~ ) iff ( b₃ in b₂ & ( for b₄ being Element of b₁ st b₄ in b₂ & [b₄,b₃] in the InternalRel of b₁ holds
[b₃,b₄] in the InternalRel of b₁ ) ) )

proof end;

theorem Th19: :: DICKSON:19

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₁ is quasi_ordered & b₂ is antisymmetric & b₂ \~ is well_founded & ( for b₄, b₅ being Element of b₁ holds
( ( b₄ <= b₅ implies b₃ . b₄ <= b₃ . b₅ ) & ( b₃ . b₄ = b₃ . b₅ implies [b₄,b₅] in EqRel b₁ ) ) ) holds
b₁ \~ is well_founded

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
func min-classes c₂ -> Subset-Family of a₁ means :Def8: :: DICKSON:def 8
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being Element of (a₁ \~ ) st
( b₂ is_minimal_wrt a₂,the InternalRel of (a₁ \~ ) & b₁ = (Class (EqRel a₁),b₂) /\ a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th20: :: DICKSON:20

for b₁ being non empty RelStr
for b₂ being Subset of b₁
for b₃ being set st b₁ is quasi_ordered & b₃ in min-classes b₂ holds
for b₄ being Element of (b₁ \~ ) st b₄ in b₃ holds
b₄ is_minimal_wrt b₂,the InternalRel of (b₁ \~ )

proof end;

theorem Th21: :: DICKSON:21

for b₁ being non empty RelStr holds
( b₁ \~ is well_founded iff for b₂ being Subset of b₁ st b₂ <> {} holds
ex b₃ being set st b₃ in min-classes b₂ )

proof end;

theorem Th22: :: DICKSON:22

for b₁ being non empty RelStr
for b₂ being Subset of b₁
for b₃ being Element of (b₁ \~ ) st b₃ is_minimal_wrt b₂,the InternalRel of (b₁ \~ ) holds
not min-classes b₂ is empty

proof end;

theorem Th23: :: DICKSON:23

for b₁ being non empty RelStr
for b₂ being Subset of b₁
for b₃ being set st b₁ is quasi_ordered & b₃ in min-classes b₂ holds
not b₃ is empty

proof end;

theorem Th24: :: DICKSON:24

for b₁ being non empty RelStr st b₁ is quasi_ordered holds
( ( b₁ is connected & b₁ \~ is well_founded ) iff for b₂ being non empty Subset of b₁ holds Card (min-classes b₂) = 1 )

proof end;

theorem Th25: :: DICKSON:25

for b₁ being non empty Poset holds
( the InternalRel of b₁ well_orders the carrier of b₁ iff for b₂ being non empty Subset of b₁ holds Card (min-classes b₂) = 1 )

proof end;

definition

let c₁ be RelStr ;
let c₂ be Subset of c₁;
let c₃ be set ;
pred c₃ is_Dickson-basis_of c₂,c₁ means :Def9: :: DICKSON:def 9
( a₃ c= a₂ & ( for b₁ being Element of a₁ st b₁ in a₂ holds
ex b₂ being Element of a₁ st
( b₂ in a₃ & b₂ <= b₁ ) ) );

end;

:: deftheorem Def9 defines is_Dickson-basis_of DICKSON:def 9 :

theorem Th26: :: DICKSON:26

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

proof end;

theorem Th27: :: DICKSON:27

for b₁ being non empty RelStr
for b₂ being non empty Subset of b₁
for b₃ being set st b₃ is_Dickson-basis_of b₂,b₁ holds
not b₃ is empty

proof end;

definition

let c₁ be RelStr ;
attr a₁ is Dickson means :Def10: :: DICKSON:def 10
for b₁ being Subset of a₁ ex b₂ being set st
( b₂ is_Dickson-basis_of b₁,a₁ & b₂ is finite );

end;

:: deftheorem Def10 defines Dickson DICKSON:def 10 :

theorem Th28: :: DICKSON:28

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

proof end;

theorem Th29: :: DICKSON:29

for b₁, b₂ being RelStr st the InternalRel of b₁ c= the InternalRel of b₂ & b₁ is Dickson & the carrier of b₁ = the carrier of b₂ holds
b₂ is Dickson

proof end;

definition

let c₁ be Function;
let c₂ be set ;
assume that
E29: dom c₁ = NAT and
E30: c₂ in rng c₁ ;
func c₁ mindex c₂ -> Nat means :Def11: :: DICKSON:def 11
( a₁ . a₃ = a₂ & ( for b₁ being Nat st a₁ . b₁ = a₂ holds
a₃ <= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines mindex DICKSON:def 11 :

definition

let c₁ be non empty 1-sorted ;
let c₂ be sequence of c₁;
let c₃ be set ;
let c₄ be Nat;
assume E30: ex b₁ being Nat st
( c₄ < b₁ & c₂ . b₁ = c₃ ) ;
func c₂ mindex c₃,c₄ -> Nat means :Def12: :: DICKSON:def 12
( a₂ . a₅ = a₃ & a₄ < a₅ & ( for b₁ being Nat st a₄ < b₁ & a₂ . b₁ = a₃ holds
a₅ <= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines mindex DICKSON:def 12 :

theorem Th30: :: DICKSON:30

for b₁ being non empty RelStr st b₁ is quasi_ordered & b₁ is Dickson holds
for b₂ being sequence of b₁ ex b₃, b₄ being Nat st
( b₃ < b₄ & b₂ . b₃ <= b₂ . b₄ )

proof end;

theorem Th31: :: DICKSON:31

for b₁ being RelStr
for b₂ being Subset of b₁
for b₃ being Element of (b₁ \~ ) st b₁ is quasi_ordered & b₃ in b₂ & (the InternalRel of b₁ -Seg b₃) /\ b₂ c= Class (EqRel b₁),b₃ holds
b₃ is_minimal_wrt b₂,the InternalRel of (b₁ \~ )

proof end;

theorem Th32: :: DICKSON:32

for b₁ being non empty RelStr st b₁ is quasi_ordered & ( for b₂ being sequence of b₁ ex b₃, b₄ being Nat st
( b₃ < b₄ & b₂ . b₃ <= b₂ . b₄ ) ) holds
for b₂ being non empty Subset of b₁ holds
( min-classes b₂ is finite & not min-classes b₂ is empty )

proof end;

theorem Th33: :: DICKSON:33

for b₁ being non empty RelStr st b₁ is quasi_ordered & ( for b₂ being non empty Subset of b₁ holds
( min-classes b₂ is finite & not min-classes b₂ is empty ) ) holds
b₁ is Dickson

proof end;

theorem Th34: :: DICKSON:34

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

proof end;

theorem Th35: :: DICKSON:35

for b₁ being non empty Poset
for b₂ being non empty Subset of b₁ st b₁ is Dickson holds
ex b₃ being set st
( b₃ is_Dickson-basis_of b₂,b₁ & ( for b₄ being set st b₄ is_Dickson-basis_of b₂,b₁ holds
b₃ c= b₄ ) )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Subset of c₁;
assume E36: c₁ is Dickson ;
func Dickson-bases c₂,c₁ -> non empty Subset-Family of a₁ means :Def13: :: DICKSON:def 13
for b₁ being set holds
( b₁ in a₃ iff b₁ is_Dickson-basis_of a₂,a₁ );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th36: :: DICKSON:36

for b₁ being non empty RelStr
for b₂ being sequence of b₁ st b₁ is Dickson holds
ex b₃ being sequence of b₁ st
( b₃ is subsequence of b₂ & b₃ is weakly-ascending )

proof end;

theorem Th37: :: DICKSON:37

for b₁ being RelStr st b₁ is empty holds
b₁ is Dickson

proof end;

theorem Th38: :: DICKSON:38

for b₁, b₂ being RelStr st b₁ is Dickson & b₂ is Dickson & b₁ is quasi_ordered & b₂ is quasi_ordered holds
( [:b₁,b₂:] is quasi_ordered & [:b₁,b₂:] is Dickson )

proof end;

theorem Th39: :: DICKSON:39

for b₁, b₂ being RelStr st b₁,b₂ are_isomorphic & b₁ is Dickson & b₁ is quasi_ordered holds
( b₂ is quasi_ordered & b₂ is Dickson )

proof end;

theorem Th40: :: DICKSON:40

for b₁ being RelStr-yielding ManySortedSet of 1
for b₂ being Element of 1 holds b₁ . b₂, product b₁ are_isomorphic

proof end;

registration

let c₁ be set ;
let c₂ be RelStr-yielding ManySortedSet of c₁;
let c₃ be Subset of c₁;
cluster a₂ | a₃ -> RelStr-yielding ;
coherence

proof end;

end;

theorem Th41: :: DICKSON:41

for b₁ being non empty Nat
for b₂ being RelStr-yielding ManySortedSet of b₁ holds
( not product b₂ is empty iff b₂ is non-Empty )

proof end;

theorem Th42: :: DICKSON:42

for b₁ being non empty Nat
for b₂ being RelStr-yielding ManySortedSet of b₁ + 1
for b₃ being Subset of (b₁ + 1)
for b₄ being Element of b₁ + 1 st b₃ = b₁ & b₄ = b₁ holds
[:(product (b₂ | b₃)),(b₂ . b₄):], product b₂ are_isomorphic

proof end;

theorem Th43: :: DICKSON:43

for b₁ being non empty Nat
for b₂ being RelStr-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds
( b₂ . b₃ is Dickson & b₂ . b₃ is quasi_ordered ) ) holds
( product b₂ is quasi_ordered & product b₂ is Dickson )

proof end;

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

proof end;

registration

let c₁ be RelStr-yielding ManySortedSet of {} ;
cluster product a₁ -> non empty ;
coherence by Lemma45;
cluster product a₁ -> antisymmetric ;
coherence by Lemma45;
cluster product a₁ -> quasi_ordered ;
coherence by Lemma45;
cluster product a₁ -> Dickson ;
coherence by Lemma45;

end;

definition

func NATOrd -> Relation of NAT equals :: DICKSON:def 14
{ [b₁,b₂] where B is Element of NAT , B is Element of NAT : b₁ <= b₂ } ;
correctness

proof end;

end;

:: deftheorem Def14 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 Def15 defines OrderedNAT DICKSON:def 15 :

E50: now

now

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

end;

hence OrderedNAT is connected by WAYBEL_0:def 29;

end;

registration

cluster OrderedNAT -> non empty connected ;
coherence by Lemma50;
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;

E51: now

let c₁ be Nat;
set c₂ = product (c₁ --> OrderedNAT );

per cases ;

suppose c₁ is empty ;

hence ( not product (c₁ --> OrderedNAT ) is empty & product (c₁ --> OrderedNAT ) is Dickson & product (c₁ --> OrderedNAT ) is quasi_ordered & product (c₁ --> OrderedNAT ) is antisymmetric ) by Lemma45;

end;

suppose not c₁ is empty ;

then reconsider c₃ = c₁ as non empty Nat ;
set c₄ = c₃ --> OrderedNAT ;
not product (c₃ --> OrderedNAT ) is empty ;
hence not product (c₁ --> OrderedNAT ) is empty ;
for b₁ being Element of c₃ holds
( (c₃ --> OrderedNAT ) . b₁ is Dickson & (c₃ --> OrderedNAT ) . b₁ is quasi_ordered ) by FUNCOP_1:13;
hence ( product (c₁ --> OrderedNAT ) is Dickson & product (c₁ --> OrderedNAT ) is quasi_ordered ) by Th43;
product (c₃ --> OrderedNAT ) is antisymmetric ;
hence product (c₁ --> OrderedNAT ) is antisymmetric ;

end;

registration

let c₁ be Nat;
cluster product (a₁ --> OrderedNAT ) -> non empty ;
coherence by Lemma51;
cluster product (a₁ --> OrderedNAT ) -> Dickson ;
coherence by Lemma51;
cluster product (a₁ --> OrderedNAT ) -> quasi_ordered ;
coherence by Lemma51;
cluster product (a₁ --> OrderedNAT ) -> antisymmetric ;
coherence by Lemma51;

end;

theorem Th48: :: DICKSON:48

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

theorem Th49: :: DICKSON:49

for b₁, b₂ being non empty RelStr st b₁ is Dickson & b₁ is quasi_ordered & b₂ is quasi_ordered & the InternalRel of b₁ c= the InternalRel of b₂ & the carrier of b₁ = the carrier of b₂ holds
b₂ \~ is well_founded

proof end;

theorem Th50: :: DICKSON:50

for b₁ being non empty RelStr st b₁ is quasi_ordered holds
( b₁ is Dickson iff for b₂ being non empty RelStr st b₂ is quasi_ordered & the InternalRel of b₁ c= the InternalRel of b₂ & the carrier of b₁ = the carrier of b₂ holds
b₂ \~ is well_founded )

proof end;