:: by Gilbert Lee and Piotr Rudnicki

::

:: Received March 12, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

::$CT

:: 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 ) );

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;

end;
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;

for n being Nat holds [(f . n),(f . (n + 1))] in the InternalRel of R;

:: 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 );

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

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 )

( 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 )

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

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;

:: deftheorem defines quasi_ordered DICKSON:def 3 :

for R being RelStr holds

( R is quasi_ordered iff ( R is reflexive & R is transitive ) );

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 ;

the InternalRel of R /\ ( the InternalRel of R ~) is Equivalence_Relation of the carrier of R

end;
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 ~);

the InternalRel of R /\ ( the InternalRel of R ~) is Equivalence_Relation of the carrier of R

proof 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 ~);

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 ((EqRel R),y) iff ( x <= y & y <= x ) )

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 ;

ex b_{1} being Relation of (Class (EqRel R)) st

for A, B being object holds

( [A,B] in b_{1} iff ex a, b being Element of R st

( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )

for b_{1}, b_{2} being Relation of (Class (EqRel R)) st ( for A, B being object holds

( [A,B] in b_{1} iff ex a, b being Element of R st

( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) & ( for A, B being object holds

( [A,B] in b_{2} iff ex a, b being Element of R st

( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) holds

b_{1} = b_{2}

end;
func <=E R -> Relation of (Class (EqRel R)) 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 ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) );

existence for A, B being object 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 ) );

ex b

for A, B being object holds

( [A,B] in b

( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )

proof end;

uniqueness for b

( [A,B] in b

( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) & ( for A, B being object holds

( [A,B] in b

( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) holds

b

proof end;

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

for R being RelStr

for b_{2} being Relation of (Class (EqRel R)) holds

( b_{2} = <=E R iff for A, B being object holds

( [A,B] in b_{2} iff ex a, b being Element of R st

( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) );

for R being RelStr

for b

( b

( [A,B] in b

( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) );

theorem :: DICKSON:10

for R being non empty RelStr st R is quasi_ordered & R is connected holds

<=E R linearly_orders Class (EqRel R)

<=E R linearly_orders Class (EqRel R)

proof end;

registration
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

end;
let R be Relation of X;

:: original: \~

redefine func R \~ -> Relation of X;

coherence

R \~ is Relation of X

proof end;

definition

let R be RelStr ;

coherence

RelStr(# the carrier of R,( the InternalRel of R \~) #) is strict RelStr ;

;

end;
func R \~ -> strict RelStr equals :: DICKSON:def 7

RelStr(# the carrier of R,( the InternalRel of R \~) #);

correctness RelStr(# the carrier of R,( the InternalRel of R \~) #);

coherence

RelStr(# the carrier of R,( the InternalRel of R \~) #) is strict RelStr ;

;

:: deftheorem defines \~ DICKSON:def 7 :

for R being RelStr holds R \~ = RelStr(# the carrier of R,( the InternalRel of R \~) #);

for R being RelStr holds R \~ = RelStr(# the carrier of R,( the InternalRel of R \~) #);

registration
end;

registration
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 ) )

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: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 ) ) )

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

:: 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

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;

ex b_{1} being Subset-Family of R st

for x being set holds

( x in b_{1} iff ex y being Element of (R \~) st

( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) )

for b_{1}, b_{2} being Subset-Family of R st ( for x being set holds

( x in b_{1} iff ex y being Element of (R \~) st

( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) ) & ( for x being set holds

( x in b_{2} iff ex y being Element of (R \~) st

( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for x being set holds

( x in b

( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) )

proof end;

uniqueness for b

( x in b

( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) ) & ( for x being set holds

( x in b

( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) ) holds

b

proof end;

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

for R being non empty RelStr

for N being Subset of R

for b_{3} being Subset-Family of R holds

( b_{3} = min-classes N iff for x being set holds

( x in b_{3} iff ex y being Element of (R \~) st

( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) );

for R being non empty RelStr

for N being Subset of R

for b

( b

( x in b

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

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 )

( 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

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

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

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

( 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 ;

end;
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 ) ) );

( 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 ) ) );

:: 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 ) ) ) );

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 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

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 ;

end;
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 );

for N being Subset of R ex B being set st

( B is_Dickson-basis_of N,R & B is finite );

:: 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 ) );

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 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

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 ;

ex b_{1} being Element of NAT st

( f . b_{1} = b & ( for i being Element of NAT st f . i = b holds

b_{1} <= i ) )

for b_{1}, b_{2} being Element of NAT st f . b_{1} = b & ( for i being Element of NAT st f . i = b holds

b_{1} <= i ) & f . b_{2} = b & ( for i being Element of NAT st f . i = b holds

b_{2} <= i ) holds

b_{1} = b_{2}

end;
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 ( f . it = b & ( for i being Element of NAT st f . i = b holds

it <= i ) );

ex b

( f . b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being Element of NAT holds

( b_{3} = f mindex b iff ( f . b_{3} = b & ( for i being Element of NAT st f . i = b holds

b_{3} <= i ) ) );

for f being Function

for b being set st dom f = NAT & b in rng f holds

for b

( b

b

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 ) ;

ex b_{1} being Element of NAT st

( f . b_{1} = b & m < b_{1} & ( for i being Element of NAT st m < i & f . i = b holds

b_{1} <= i ) )

for b_{1}, b_{2} being Element of NAT st f . b_{1} = b & m < b_{1} & ( for i being Element of NAT st m < i & f . i = b holds

b_{1} <= i ) & f . b_{2} = b & m < b_{2} & ( for i being Element of NAT st m < i & f . i = b holds

b_{2} <= i ) holds

b_{1} = b_{2}

end;
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 ( f . it = b & m < it & ( for i being Element of NAT st m < i & f . i = b holds

it <= i ) );

ex b

( f . b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being Element of NAT holds

( b_{5} = f mindex (b,m) iff ( f . b_{5} = b & m < b_{5} & ( for i being Element of NAT st m < i & f . i = b holds

b_{5} <= i ) ) );

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 b

( b

b

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 )

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 ((EqRel R),x) holds

x is_minimal_wrt N, the InternalRel of (R \~)

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 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 )

( 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

( min-classes N is finite & not min-classes N is empty ) ) holds

R is Dickson

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 ) )

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 ;

ex b_{1} being non empty Subset-Family of R st

for B being set holds

( B in b_{1} iff B is_Dickson-basis_of N,R )

for b_{1}, b_{2} being non empty Subset-Family of R st ( for B being set holds

( B in b_{1} iff B is_Dickson-basis_of N,R ) ) & ( for B being set holds

( B in b_{2} iff B is_Dickson-basis_of N,R ) ) holds

b_{1} = b_{2}

end;
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 for B being set holds

( B in it iff B is_Dickson-basis_of N,R );

ex b

for B being set holds

( B in b

proof end;

uniqueness for b

( B in b

( B in b

b

proof 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 b_{3} being non empty Subset-Family of R holds

( b_{3} = Dickson-bases (N,R) iff for B being set holds

( B in b_{3} iff B is_Dickson-basis_of N,R ) );

for R being non empty RelStr

for N being Subset of R st R is Dickson holds

for b

( b

( B in b

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 )

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 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 )

( [: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 )

( S is quasi_ordered & S is Dickson )

proof end;

theorem Th38: :: DICKSON:39

for p being RelStr-yielding ManySortedSet of {0}

for z being Element of {0} holds p . z, product p are_isomorphic

for z being Element of {0} 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

end;
let p be RelStr-yielding ManySortedSet of X;

let Y be Subset of X;

coherence

p | Y is RelStr-yielding

proof 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 )

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

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 )

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 {} ;

coherence

not product p is empty by Lm1;

coherence

product p is antisymmetric by Lm1;

coherence

product p is quasi_ordered by Lm1;

coherence

product p is Dickson by Lm1;

end;
coherence

not product p is empty by Lm1;

coherence

product p is antisymmetric by Lm1;

coherence

product p is quasi_ordered by Lm1;

coherence

product p is Dickson by Lm1;

definition

coherence

{ [x,y] where x, y is Element of NAT : x <= y } is Relation of NAT;

end;

::: RelIncl omega;

func NATOrd -> Relation of NAT equals :: DICKSON:def 14

{ [x,y] where x, y is Element of NAT : x <= y } ;

correctness { [x,y] where x, y is Element of NAT : x <= y } ;

coherence

{ [x,y] where x, y is Element of NAT : x <= y } is Relation of NAT;

proof end;

:: deftheorem defines NATOrd DICKSON:def 14 :

NATOrd = { [x,y] where x, y is Element of NAT : x <= y } ;

NATOrd = { [x,y] where x, y is Element of NAT : x <= y } ;

Lm2: now :: thesis: OrderedNAT is connected

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;
y <= x by Th44;

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

registration

coherence

OrderedNAT is connected by Lm2;

coherence

OrderedNAT is Dickson

OrderedNAT is quasi_ordered

OrderedNAT is antisymmetric by Th43;

coherence

OrderedNAT is transitive by Th45;

coherence

OrderedNAT is well_founded

end;
OrderedNAT is connected by Lm2;

coherence

OrderedNAT is Dickson

proof end;

coherence OrderedNAT is quasi_ordered

proof end;

coherence OrderedNAT is antisymmetric by Th43;

coherence

OrderedNAT is transitive by Th45;

coherence

OrderedNAT is well_founded

proof end;

Lm3: now :: thesis: for n being Element of NAT holds

( not product (n --> OrderedNAT) is empty & product (n --> OrderedNAT) is Dickson & product (n --> OrderedNAT) is quasi_ordered & product (n --> OrderedNAT) is antisymmetric )

( not product (n --> OrderedNAT) is empty & product (n --> OrderedNAT) is Dickson & product (n --> OrderedNAT) is quasi_ordered & product (n --> OrderedNAT) is antisymmetric )

let n be Element of NAT ; :: thesis: ( not product (b_{1} --> OrderedNAT) is empty & product (b_{1} --> OrderedNAT) is Dickson & product (b_{1} --> OrderedNAT) is quasi_ordered & product (b_{1} --> OrderedNAT) is antisymmetric )

set pp = product (n --> OrderedNAT);

end;
set pp = product (n --> OrderedNAT);

per cases
( n is zero or not n is zero )
;

end;

suppose
n is zero
; :: thesis: ( not product (b_{1} --> OrderedNAT) is empty & product (b_{1} --> OrderedNAT) is Dickson & product (b_{1} --> OrderedNAT) is quasi_ordered & product (b_{1} --> OrderedNAT) is antisymmetric )

then
n = 0
;

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

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

suppose
not n is zero
; :: thesis: ( not product (b_{1} --> OrderedNAT) is empty & product (b_{1} --> OrderedNAT) is Dickson & product (b_{1} --> OrderedNAT) is quasi_ordered & product (b_{1} --> OrderedNAT) 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 (n --> OrderedNAT) is empty ; :: thesis: ( product (n --> OrderedNAT) is Dickson & product (n --> OrderedNAT) is quasi_ordered & product (n --> OrderedNAT) is antisymmetric )

for i being Element of Segm n9 holds

( p . i is Dickson & p . i is quasi_ordered ) ;

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

product p is antisymmetric ;

hence product (n --> OrderedNAT) is antisymmetric ; :: thesis: verum

end;
reconsider p = n9 --> OrderedNAT as RelStr-yielding ManySortedSet of Segm n9 ;

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

for i being Element of Segm n9 holds

( p . i is Dickson & p . i is quasi_ordered ) ;

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

product p is antisymmetric ;

hence product (n --> OrderedNAT) is antisymmetric ; :: thesis: verum

registration

let n be Element of NAT ;

coherence

not product (n --> OrderedNAT) is empty ;

coherence

product (n --> OrderedNAT) is Dickson by Lm3;

coherence

product (n --> OrderedNAT) is quasi_ordered by Lm3;

coherence

product (n --> OrderedNAT) is antisymmetric by Lm3;

end;
coherence

not product (n --> OrderedNAT) is empty ;

coherence

product (n --> OrderedNAT) is Dickson by Lm3;

coherence

product (n --> OrderedNAT) is quasi_ordered by Lm3;

coherence

product (n --> OrderedNAT) is antisymmetric by Lm3;

theorem :: DICKSON:47

for M being RelStr st M is Dickson & M is quasi_ordered holds

( [:M,OrderedNAT:] is quasi_ordered & [:M,OrderedNAT:] is Dickson ) by Th36;

( [:M,OrderedNAT:] is quasi_ordered & [:M,OrderedNAT:] 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

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 )

( 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;