begin
theorem Th1:
theorem Th2:
for
n being
Nat holds
n c= n + 1
theorem Th3:
:: deftheorem defines ascending DICKSON:def 1 :
:: deftheorem Def2 defines weakly-ascending DICKSON:def 2 :
theorem Th4:
theorem Th5:
theorem
canceled;
theorem Th7:
theorem Th8:
begin
:: deftheorem Def3 defines quasi_ordered DICKSON:def 3 :
:: deftheorem Def4 defines EqRel DICKSON:def 4 :
theorem Th9:
definition
let R be
RelStr ;
func <=E R -> Relation of
(Class (EqRel R)) means :
Def5:
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
ex b1 being Relation of (Class (EqRel R)) st
for A, B being set holds
( [A,B] in b1 iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) )
uniqueness
for b1, b2 being Relation of (Class (EqRel R)) st ( for A, B being set holds
( [A,B] in b1 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 set holds
( [A,B] in b2 iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines <=E DICKSON:def 5 :
theorem Th10:
theorem
:: deftheorem defines \~ DICKSON:def 6 :
:: deftheorem defines \~ DICKSON:def 7 :
theorem
theorem
theorem
theorem
theorem Th16:
theorem Th17:
begin
theorem Th18:
theorem
:: deftheorem Def8 defines min-classes DICKSON:def 8 :
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem
:: deftheorem Def9 defines is_Dickson-basis_of DICKSON:def 9 :
theorem Th26:
theorem Th27:
:: deftheorem Def10 defines Dickson DICKSON:def 10 :
theorem Th28:
theorem Th29:
:: deftheorem Def11 defines mindex DICKSON:def 11 :
:: deftheorem Def12 defines mindex DICKSON:def 12 :
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem
:: deftheorem Def13 defines Dickson-bases DICKSON:def 13 :
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
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 )
:: deftheorem defines NATOrd DICKSON:def 14 :
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
:: deftheorem defines OrderedNAT DICKSON:def 15 :
theorem
theorem Th49:
theorem