:: BAGORDER semantic presentation

theorem Th1: :: BAGORDER:1

for b₁, b₂, b₃ being set st b₃ in b₁ & b₃ in b₂ holds
( b₁ \ {b₃} = b₂ \ {b₃} iff b₁ = b₂ )

proof end;

theorem Th2: :: BAGORDER:2

for b₁, b₂ being Nat holds
( b₂ in Seg b₁ iff ( b₂ - 1 is Nat & b₂ - 1 < b₁ ) )

proof end;

registration

let c₁ be natural-yielding Function;
let c₂ be set ;
cluster a₁ | a₂ -> natural-yielding ;
coherence

proof end;

end;

registration

let c₁ be finite-support Function;
let c₂ be set ;
cluster a₁ | a₂ -> finite-support ;
coherence

proof end;

end;

theorem Th3: :: BAGORDER:3

for b₁ being Function
for b₂ being set st b₂ in dom b₁ holds
b₁ * <*b₂*> = <*(b₁ . b₂)*>

proof end;

theorem Th4: :: BAGORDER:4

for b₁, b₂, b₃ being Function st dom b₁ = dom b₂ & rng b₁ c= dom b₃ & rng b₂ c= dom b₃ & b₁,b₂ are_fiberwise_equipotent holds
b₃ * b₁,b₃ * b₂ are_fiberwise_equipotent

proof end;

theorem Th5: :: BAGORDER:5

for b₁ being FinSequence of NAT holds
( Sum b₁ = 0 iff b₁ = (len b₁) |-> 0 )

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be ManySortedSet of c₁;
func c₂,c₃ -cut c₄ -> ManySortedSet of a₃ -' a₂ means :Def1: :: BAGORDER:def 1
for b₁ being Nat st b₁ in a₃ -' a₂ holds
a₅ . b₁ = a₄ . (a₂ + b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines -cut BAGORDER:def 1 :

registration

let c₁, c₂, c₃ be Nat;
let c₄ be natural-yielding ManySortedSet of c₁;
cluster a₂,a₃ -cut a₄ -> natural-yielding ;
coherence

proof end;

end;

registration

let c₁, c₂, c₃ be Nat;
let c₄ be finite-support ManySortedSet of c₁;
cluster a₂,a₃ -cut a₄ -> finite-support ;
coherence ;

end;

theorem Th6: :: BAGORDER:6

for b₁, b₂ being Nat
for b₃, b₄ being ManySortedSet of b₁ holds
( b₃ = b₄ iff ( 0,(b₂ + 1) -cut b₃ = 0,(b₂ + 1) -cut b₄ & (b₂ + 1),b₁ -cut b₃ = (b₂ + 1),b₁ -cut b₄ ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty Nat;
func Fin c₁,c₂ -> set equals :: BAGORDER:def 2
{ b₁ where B is Subset of a₁ : ( b₁ is finite & not b₁ is empty & Card b₁ <=` a₂ ) } ;
coherence ;

end;

:: deftheorem Def2 defines Fin BAGORDER:def 2 :

registration

let c₁ be non empty set ;
let c₂ be non empty Nat;
cluster Fin a₁,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th7: :: BAGORDER:7

for b₁ being non empty transitive antisymmetric RelStr
for b₂ being finite Subset of b₁ st b₂ <> {} holds
ex b₃ being Element of b₁ st
( b₃ in b₂ & b₃ is_maximal_wrt b₂,the InternalRel of b₁ )

proof end;

theorem Th8: :: BAGORDER:8

for b₁ being non empty transitive antisymmetric RelStr
for b₂ being finite Subset of b₁ st b₂ <> {} holds
ex b₃ being Element of b₁ st
( b₃ in b₂ & b₃ is_minimal_wrt b₂,the InternalRel of b₁ )

proof end;

theorem Th9: :: BAGORDER:9

for b₁ being non empty transitive antisymmetric RelStr
for b₂ being sequence of b₁ st b₂ is descending holds
for b₃, b₄ being Nat st b₄ < b₃ holds
( b₂ . b₄ <> b₂ . b₃ & [(b₂ . b₃),(b₂ . b₄)] in the InternalRel of b₁ )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be sequence of c₁;
attr a₂ is non-increasing means :Def3: :: BAGORDER:def 3
for b₁ being Nat holds [(a₂ . (b₁ + 1)),(a₂ . b₁)] in the InternalRel of a₁;

end;

:: deftheorem Def3 defines non-increasing BAGORDER:def 3 :

theorem Th10: :: BAGORDER:10

for b₁ being non empty transitive RelStr
for b₂ being sequence of b₁ st b₂ is non-increasing holds
for b₃, b₄ being Nat st b₄ < b₃ holds
[(b₂ . b₃),(b₂ . b₄)] in the InternalRel of b₁

proof end;

theorem Th11: :: BAGORDER:11

for b₁ being non empty transitive RelStr
for b₂ being sequence of b₁ st b₁ is well_founded & b₂ is non-increasing holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₂ . b₃ = b₂ . b₄

proof end;

theorem Th12: :: BAGORDER:12

for b₁ being set
for b₂ being Element of b₁
for b₃ being finite Subset of b₁
for b₄ being Order of b₁ st b₃ = {b₂} & b₄ linearly_orders b₃ holds
SgmX b₄,b₃ = <*b₂*>

proof end;

definition

let c₁ be Ordinal;
let c₂ be bag of c₁;
func TotDegree c₂ -> Nat means :Def4: :: BAGORDER:def 4
ex b₁ being FinSequence of NAT st
( a₃ = Sum b₁ & b₁ = a₂ * (SgmX (RelIncl a₁),(support a₂)) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def4 defines TotDegree BAGORDER:def 4 :

theorem Th13: :: BAGORDER:13

for b₁ being Ordinal
for b₂ being bag of b₁
for b₃ being finite Subset of b₁
for b₄, b₅ being FinSequence of NAT st b₄ = b₂ * (SgmX (RelIncl b₁),(support b₂)) & b₅ = b₂ * (SgmX (RelIncl b₁),((support b₂) \/ b₃)) holds
Sum b₄ = Sum b₅

proof end;

theorem Th14: :: BAGORDER:14

for b₁ being Ordinal
for b₂, b₃ being bag of b₁ holds TotDegree (b₂ + b₃) = (TotDegree b₂) + (TotDegree b₃)

proof end;

theorem Th15: :: BAGORDER:15

for b₁ being Ordinal
for b₂, b₃ being bag of b₁ st b₃ divides b₂ holds
TotDegree (b₂ -' b₃) = (TotDegree b₂) - (TotDegree b₃)

proof end;

theorem Th16: :: BAGORDER:16

for b₁ being Ordinal
for b₂ being bag of b₁ holds
( TotDegree b₂ = 0 iff b₂ = EmptyBag b₁ )

proof end;

theorem Th17: :: BAGORDER:17

for b₁, b₂, b₃ being Nat holds b₁,b₂ -cut (EmptyBag b₃) = EmptyBag (b₂ -' b₁)

proof end;

theorem Th18: :: BAGORDER:18

for b₁, b₂, b₃ being Nat
for b₄, b₅ being bag of b₃ holds b₁,b₂ -cut (b₄ + b₅) = (b₁,b₂ -cut b₄) + (b₁,b₂ -cut b₅)

proof end;

theorem Th19: :: BAGORDER:19

for b₁ being set holds support (EmptyBag b₁) = {}

proof end;

theorem Th20: :: BAGORDER:20

for b₁ being set
for b₂ being bag of b₁ st support b₂ = {} holds
b₂ = EmptyBag b₁

proof end;

theorem Th21: :: BAGORDER:21

for b₁, b₂ being Ordinal
for b₃ being bag of b₁ st b₂ in b₁ holds
b₃ | b₂ is bag of b₂

proof end;

theorem Th22: :: BAGORDER:22

for b₁ being Ordinal
for b₂, b₃ being bag of b₁ st b₃ divides b₂ holds
support b₃ c= support b₂

proof end;

definition

let c₁ be set ;
mode TermOrder of a₁ is Order of Bags a₁;

end;

notation

let c₁ be Ordinal;
synonym LexOrder c₁ for BagOrder c₁;

end;

definition

let c₁ be Ordinal;
let c₂ be TermOrder of c₁;
canceled;
canceled;
attr a₂ is admissible means :Def7: :: BAGORDER:def 7
( a₂ is_strongly_connected_in Bags a₁ & ( for b₁ being bag of a₁ holds [(EmptyBag a₁),b₁] in a₂ ) & ( for b₁, b₂, b₃ being bag of a₁ st [b₁,b₂] in a₂ holds
[(b₁ + b₃),(b₂ + b₃)] in a₂ ) );

end;

:: deftheorem Def5 BAGORDER:def 5 :

:: deftheorem Def6 BAGORDER:def 6 :

:: deftheorem Def7 defines admissible BAGORDER:def 7 :

theorem Th23: :: BAGORDER:23

for b₁ being Ordinal holds LexOrder b₁ is admissible

proof end;

registration

let c₁ be Ordinal;
cluster admissible Relation of Bags a₁, Bags a₁;
existence

proof end;

end;

registration

let c₁ be Ordinal;
cluster LexOrder a₁ -> admissible ;
coherence by Th23;

end;

theorem Th24: :: BAGORDER:24

for b₁ being infinite Ordinal holds not LexOrder b₁ is well-ordering

proof end;

definition

let c₁ be Ordinal;
func InvLexOrder c₁ -> TermOrder of a₁ means :Def8: :: BAGORDER:def 8
for b₁, b₂ being bag of a₁ holds
( [b₁,b₂] in a₂ iff ( b₁ = b₂ or ex b₃ being Ordinal st
( b₃ in a₁ & b₁ . b₃ < b₂ . b₃ & ( for b₄ being Ordinal st b₃ in b₄ & b₄ in a₁ holds
b₁ . b₄ = b₂ . b₄ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines InvLexOrder BAGORDER:def 8 :

theorem Th25: :: BAGORDER:25

for b₁ being Ordinal holds InvLexOrder b₁ is admissible

proof end;

registration

let c₁ be Ordinal;
cluster InvLexOrder a₁ -> admissible ;
coherence by Th25;

end;

theorem Th26: :: BAGORDER:26

for b₁ being Ordinal holds InvLexOrder b₁ is well-ordering

proof end;

definition

let c₁ be Ordinal;
let c₂ be TermOrder of c₁;
assume E26: for b₁, b₂, b₃ being bag of c₁ st [b₁,b₂] in c₂ holds
[(b₁ + b₃),(b₂ + b₃)] in c₂ ;
func Graded c₂ -> TermOrder of a₁ means :Def9: :: BAGORDER:def 9
for b₁, b₂ being bag of a₁ holds
( [b₁,b₂] in a₃ iff ( TotDegree b₁ < TotDegree b₂ or ( TotDegree b₁ = TotDegree b₂ & [b₁,b₂] in a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Graded BAGORDER:def 9 :

theorem Th27: :: BAGORDER:27

for b₁ being Ordinal
for b₂ being TermOrder of b₁ st ( for b₃, b₄, b₅ being bag of b₁ st [b₃,b₄] in b₂ holds
[(b₃ + b₅),(b₄ + b₅)] in b₂ ) & b₂ is_strongly_connected_in Bags b₁ holds
Graded b₂ is admissible

proof end;

definition

let c₁ be Ordinal;
func GrLexOrder c₁ -> TermOrder of a₁ equals :: BAGORDER:def 10
Graded (LexOrder a₁);
coherence ;
func GrInvLexOrder c₁ -> TermOrder of a₁ equals :: BAGORDER:def 11
Graded (InvLexOrder a₁);
coherence ;

end;

:: deftheorem Def10 defines GrLexOrder BAGORDER:def 10 :

:: deftheorem Def11 defines GrInvLexOrder BAGORDER:def 11 :

theorem Th28: :: BAGORDER:28

for b₁ being Ordinal holds GrLexOrder b₁ is admissible

proof end;

registration

let c₁ be Ordinal;
cluster GrLexOrder a₁ -> admissible ;
coherence by Th28;

end;

theorem Th29: :: BAGORDER:29

for b₁ being infinite Ordinal holds not GrLexOrder b₁ is well-ordering

proof end;

theorem Th30: :: BAGORDER:30

for b₁ being Ordinal holds GrInvLexOrder b₁ is admissible

proof end;

registration

let c₁ be Ordinal;
cluster GrInvLexOrder a₁ -> admissible ;
coherence by Th30;

end;

theorem Th31: :: BAGORDER:31

for b₁ being Ordinal holds GrInvLexOrder b₁ is well-ordering

proof end;

definition

let c₁, c₂ be Nat;
let c₃ be TermOrder of (c₁ + 1);
let c₄ be TermOrder of (c₂ -' (c₁ + 1));
func BlockOrder c₁,c₂,c₃,c₄ -> TermOrder of a₂ means :Def12: :: BAGORDER:def 12
for b₁, b₂ being bag of a₂ holds
( [b₁,b₂] in a₅ iff ( ( 0,(a₁ + 1) -cut b₁ <> 0,(a₁ + 1) -cut b₂ & [(0,(a₁ + 1) -cut b₁),(0,(a₁ + 1) -cut b₂)] in a₃ ) or ( 0,(a₁ + 1) -cut b₁ = 0,(a₁ + 1) -cut b₂ & [((a₁ + 1),a₂ -cut b₁),((a₁ + 1),a₂ -cut b₂)] in a₄ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines BlockOrder BAGORDER:def 12 :

theorem Th32: :: BAGORDER:32

for b₁, b₂ being Nat
for b₃ being TermOrder of (b₁ + 1)
for b₄ being TermOrder of (b₂ -' (b₁ + 1)) st b₃ is admissible & b₄ is admissible holds
BlockOrder b₁,b₂,b₃,b₄ is admissible

proof end;

definition

let c₁ be Nat;
func NaivelyOrderedBags c₁ -> strict RelStr means :Def13: :: BAGORDER:def 13
( the carrier of a₂ = Bags a₁ & ( for b₁, b₂ being bag of a₁ holds
( [b₁,b₂] in the InternalRel of a₂ iff b₁ divides b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines NaivelyOrderedBags BAGORDER:def 13 :

theorem Th33: :: BAGORDER:33

for b₁ being Nat holds the carrier of (product (b₁ --> OrderedNAT )) = Bags b₁

proof end;

theorem Th34: :: BAGORDER:34

for b₁ being Nat holds NaivelyOrderedBags b₁ = product (b₁ --> OrderedNAT )

proof end;

theorem Th35: :: BAGORDER:35

for b₁ being Nat
for b₂ being TermOrder of b₁ st b₂ is admissible holds
( the InternalRel of (NaivelyOrderedBags b₁) c= b₂ & b₂ is well-ordering )

proof end;

definition

let c₁ be non empty connected Poset;
let c₂ be Element of Fin the carrier of c₁;
assume E34: not c₂ is empty ;
func PosetMin c₂ -> Element of a₁ means :: BAGORDER:def 14
( a₃ in a₂ & a₃ is_minimal_wrt a₂,the InternalRel of a₁ );
existence

proof end;

uniqueness

proof end;

func PosetMax c₂ -> Element of a₁ means :Def15: :: BAGORDER:def 15
( a₃ in a₂ & a₃ is_maximal_wrt a₂,the InternalRel of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines PosetMin BAGORDER:def 14 :

:: deftheorem Def15 defines PosetMax BAGORDER:def 15 :

definition

let c₁ be non empty connected Poset;
func FinOrd-Approx c₁ -> Function of NAT , bool [:(Fin the carrier of a₁),(Fin the carrier of a₁):] means :Def16: :: BAGORDER:def 16
( dom a₂ = NAT & a₂ . 0 = { [b₁,b₂] where B is Element of Fin the carrier of a₁, B is Element of Fin the carrier of a₁ : ( b₁ = {} or ( b₁ <> {} & b₂ <> {} & PosetMax b₁ <> PosetMax b₂ & [(PosetMax b₁),(PosetMax b₂)] in the InternalRel of a₁ ) ) } & ( for b₁ being Element of NAT holds a₂ . (b₁ + 1) = { [b₂,b₃] where B is Element of Fin the carrier of a₁, B is Element of Fin the carrier of a₁ : ( b₂ <> {} & b₃ <> {} & PosetMax b₂ = PosetMax b₃ & [(b₂ \ {(PosetMax b₂)}),(b₃ \ {(PosetMax b₃)})] in a₂ . b₁ ) } ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines FinOrd-Approx BAGORDER:def 16 :

theorem Th36: :: BAGORDER:36

for b₁ being non empty connected Poset
for b₂, b₃ being Element of Fin the carrier of b₁ holds
( [b₂,b₃] in union (rng (FinOrd-Approx b₁)) iff ( b₂ = {} or ( b₂ <> {} & b₃ <> {} & PosetMax b₂ <> PosetMax b₃ & [(PosetMax b₂),(PosetMax b₃)] in the InternalRel of b₁ ) or ( b₂ <> {} & b₃ <> {} & PosetMax b₂ = PosetMax b₃ & [(b₂ \ {(PosetMax b₂)}),(b₃ \ {(PosetMax b₃)})] in union (rng (FinOrd-Approx b₁)) ) ) )

proof end;

theorem Th37: :: BAGORDER:37

for b₁ being non empty connected Poset
for b₂ being Element of Fin the carrier of b₁ st b₂ <> {} holds
not [b₂,{} ] in union (rng (FinOrd-Approx b₁))

proof end;

theorem Th38: :: BAGORDER:38

for b₁ being non empty connected Poset
for b₂ being Element of Fin the carrier of b₁ holds b₂ \ {(PosetMax b₂)} is Element of Fin the carrier of b₁

proof end;

Lemma39: for b₁ being non empty connected Poset
for b₂ being Nat
for b₃ being Element of Fin the carrier of b₁ st Card b₃ = b₂ + 1 holds
Card (b₃ \ {(PosetMax b₃)}) = b₂

proof end;

theorem Th39: :: BAGORDER:39

for b₁ being non empty connected Poset holds union (rng (FinOrd-Approx b₁)) is Order of Fin the carrier of b₁

proof end;

definition

let c₁ be non empty connected Poset;
func FinOrd c₁ -> Order of Fin the carrier of a₁ equals :: BAGORDER:def 17
union (rng (FinOrd-Approx a₁));
coherence by Th39;

end;

:: deftheorem Def17 defines FinOrd BAGORDER:def 17 :

definition

let c₁ be non empty connected Poset;
func FinPoset c₁ -> Poset equals :: BAGORDER:def 18
RelStr(# (Fin the carrier of a₁),(FinOrd a₁) #);
correctness ;

end;

:: deftheorem Def18 defines FinPoset BAGORDER:def 18 :

registration

let c₁ be non empty connected Poset;
cluster FinPoset a₁ -> non empty ;
correctness ;

end;

theorem Th40: :: BAGORDER:40

for b₁ being non empty connected Poset
for b₂, b₃ being Element of (FinPoset b₁) holds
( [b₂,b₃] in the InternalRel of (FinPoset b₁) iff ex b₄, b₅ being Element of Fin the carrier of b₁ st
( b₂ = b₄ & b₃ = b₅ & ( b₄ = {} or ( b₄ <> {} & b₅ <> {} & PosetMax b₄ <> PosetMax b₅ & [(PosetMax b₄),(PosetMax b₅)] in the InternalRel of b₁ ) or ( b₄ <> {} & b₅ <> {} & PosetMax b₄ = PosetMax b₅ & [(b₄ \ {(PosetMax b₄)}),(b₅ \ {(PosetMax b₅)})] in FinOrd b₁ ) ) ) )

proof end;

registration

let c₁ be non empty connected Poset;
cluster FinPoset a₁ -> non empty connected ;
correctness

proof end;

end;

definition

let c₁ be non empty connected RelStr ;
let c₂ be non empty set ;
assume that
E42: c₁ is well_founded and
E43: c₂ c= the carrier of c₁ ;
func MinElement c₂,c₁ -> Element of a₁ means :Def19: :: BAGORDER:def 19
( a₃ in a₂ & a₃ is_minimal_wrt a₂,the InternalRel of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines MinElement BAGORDER:def 19 :

definition

let c₁ be non empty RelStr ;
let c₂ be sequence of c₁;
let c₃ be Nat;
func SeqShift c₂,c₃ -> sequence of a₁ means :Def20: :: BAGORDER:def 20
for b₁ being Nat holds a₄ . b₁ = a₂ . (b₁ + a₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines SeqShift BAGORDER:def 20 :

theorem Th41: :: BAGORDER:41

for b₁ being non empty RelStr
for b₂ being sequence of b₁
for b₃ being Nat st b₂ is descending holds
SeqShift b₂,b₃ is descending

proof end;

theorem Th42: :: BAGORDER:42

for b₁ being non empty connected Poset st b₁ is well_founded holds
FinPoset b₁ is well_founded

proof end;