:: TERMORD semantic presentation

registration

cluster non trivial LoopStr ;
existence

proof end;

end;

registration

cluster add-associative right_zeroed right_complementable non trivial LoopStr ;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be bag of c₁;
attr a₂ is non-zero means :: TERMORD:def 1
a₂ <> EmptyBag a₁;

end;

:: deftheorem Def1 defines non-zero TERMORD:def 1 :

theorem Th1: :: TERMORD:1

for b₁ being set
for b₂, b₃ being bag of b₁ holds
( b₂ divides b₃ iff ex b₄ being bag of b₁ st b₃ = b₂ + b₄ )

proof end;

theorem Th2: :: TERMORD:2

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for b₃ being Series of b₁,b₂ holds (0_ b₁,b₂) *' b₃ = 0_ b₁,b₂

proof end;

registration

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr ;
let c₃, c₄ be Monomial of c₁,c₂;
cluster a₃ *' a₄ -> monomial-like ;
coherence

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let c₃, c₄ be ConstPoly of c₁,c₂;
cluster a₃ *' a₄ -> Constant ;
coherence

proof end;

end;

theorem Th3: :: TERMORD:3

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₃, b₄ being bag of b₁
for b₅, b₆ being non-zero Element of b₂ holds Monom (b₅ * b₆),(b₃ + b₄) = (Monom b₅,b₃) *' (Monom b₆,b₄)

proof end;

theorem Th4: :: TERMORD:4

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₃, b₄ being Element of b₂ holds (b₃ * b₄) | b₁,b₂ = (b₃ | b₁,b₂) *' (b₄ | b₁,b₂)

proof end;

Lemma4: for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃ being set st b₃ in field b₂ holds
b₃ is bag of b₁

proof end;

registration

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

proof end;

end;

registration

let c₁ be Nat;
cluster admissible -> admissible well_founded Relation of Bags a₁, Bags a₁;
coherence

proof end;

end;

definition

let c₁ be Ordinal;
let c₂ be TermOrder of c₁;
let c₃, c₄ be bag of c₁;
pred c₃ <= c₄,c₂ means :Def2: :: TERMORD:def 2
[a₃,a₄] in a₂;

end;

:: deftheorem Def2 defines <= TERMORD:def 2 :

definition

let c₁ be Ordinal;
let c₂ be TermOrder of c₁;
let c₃, c₄ be bag of c₁;
pred c₃ < c₄,c₂ means :Def3: :: TERMORD:def 3
( a₃ <= a₄,a₂ & a₃ <> a₄ );

end;

:: deftheorem Def3 defines < TERMORD:def 3 :

definition

let c₁ be Ordinal;
let c₂ be TermOrder of c₁;
let c₃, c₄ be bag of c₁;
func min c₃,c₄,c₂ -> bag of a₁ equals :Def4: :: TERMORD:def 4
a₃ if a₃ <= a₄,a₂
otherwise a₄;
correctness ;
func max c₃,c₄,c₂ -> bag of a₁ equals :Def5: :: TERMORD:def 5
a₃ if a₄ <= a₃,a₂
otherwise a₄;
correctness ;

end;

:: deftheorem Def4 defines min TERMORD:def 4 :

:: deftheorem Def5 defines max TERMORD:def 5 :

Lemma9: for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃ being bag of b₁ holds b₃ <= b₃,b₂

proof end;

Lemma10: for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃, b₄ being bag of b₁ st b₃ <= b₄,b₂ & b₄ <= b₃,b₂ holds
b₃ = b₄

proof end;

Lemma11: for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃ being bag of b₁ holds b₃ in field b₂

proof end;

theorem Th5: :: TERMORD:5

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃, b₄ being bag of b₁ holds
( b₃ <= b₄,b₂ iff not b₄ < b₃,b₂ )

proof end;

Lemma13: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃, b₄ being bag of b₁ holds
( b₃ <= b₄,b₂ or b₄ <= b₃,b₂ )

proof end;

theorem Th6: :: TERMORD:6

for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃ being bag of b₁ holds b₃ <= b₃,b₂ by Lemma9;

theorem Th7: :: TERMORD:7

for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃, b₄ being bag of b₁ st b₃ <= b₄,b₂ & b₄ <= b₃,b₂ holds
b₃ = b₄ by Lemma10;

theorem Th8: :: TERMORD:8

for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃, b₄, b₅ being bag of b₁ st b₃ <= b₄,b₂ & b₄ <= b₅,b₂ holds
b₃ <= b₅,b₂

proof end;

theorem Th9: :: TERMORD:9

for b₁ being Ordinal
for b₂ being admissible TermOrder of b₁
for b₃ being bag of b₁ holds EmptyBag b₁ <= b₃,b₂

proof end;

theorem Th10: :: TERMORD:10

for b₁ being Ordinal
for b₂ being admissible TermOrder of b₁
for b₃, b₄ being bag of b₁ st b₃ divides b₄ holds
b₃ <= b₄,b₂

proof end;

theorem Th11: :: TERMORD:11

for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃, b₄ being bag of b₁ holds
( min b₃,b₄,b₂ = b₃ or min b₃,b₄,b₂ = b₄ )

proof end;

theorem Th12: :: TERMORD:12

for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃, b₄ being bag of b₁ holds
( max b₃,b₄,b₂ = b₃ or max b₃,b₄,b₂ = b₄ )

proof end;

Lemma18: for b₁ being Ordinal
for b₂ being TermOrder of b₁
for b₃ being bag of b₁ holds
( min b₃,b₃,b₂ = b₃ & max b₃,b₃,b₂ = b₃ )

proof end;

theorem Th13: :: TERMORD:13

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃, b₄ being bag of b₁ holds
( min b₃,b₄,b₂ <= b₃,b₂ & min b₃,b₄,b₂ <= b₄,b₂ )

proof end;

theorem Th14: :: TERMORD:14

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃, b₄ being bag of b₁ holds
( b₃ <= max b₃,b₄,b₂,b₂ & b₄ <= max b₃,b₄,b₂,b₂ )

proof end;

theorem Th15: :: TERMORD:15

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃, b₄ being bag of b₁ holds
( min b₃,b₄,b₂ = min b₄,b₃,b₂ & max b₃,b₄,b₂ = max b₄,b₃,b₂ )

proof end;

theorem Th16: :: TERMORD:16

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃, b₄ being bag of b₁ holds
( min b₃,b₄,b₂ = b₃ iff max b₃,b₄,b₂ = b₄ )

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty ZeroStr ;
let c₄ be Polynomial of c₁,c₃;
func HT c₄,c₂ -> Element of Bags a₁ means :Def6: :: TERMORD:def 6
( ( Support a₄ = {} & a₅ = EmptyBag a₁ ) or ( a₅ in Support a₄ & ( for b₁ being bag of a₁ st b₁ in Support a₄ holds
b₁ <= a₅,a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines HT TERMORD:def 6 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty ZeroStr ;
let c₄ be Polynomial of c₁,c₃;
func HC c₄,c₂ -> Element of a₃ equals :: TERMORD:def 7
a₄ . (HT a₄,a₂);
correctness ;

end;

:: deftheorem Def7 defines HC TERMORD:def 7 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty ZeroStr ;
let c₄ be Polynomial of c₁,c₃;
func HM c₄,c₂ -> Monomial of a₁,a₃ equals :: TERMORD:def 8
Monom (HC a₄,a₂),(HT a₄,a₂);
correctness ;

end;

:: deftheorem Def8 defines HM TERMORD:def 8 :

Lemma22: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being Polynomial of b₁,b₃ holds
( HC b₄,b₂ = 0. b₃ iff b₄ = 0_ b₁,b₃ )

proof end;

Lemma23: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ holds (HM b₄,b₂) . (HT b₄,b₂) = b₄ . (HT b₄,b₂)

proof end;

Lemma24: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ st HC b₄,b₂ <> 0. b₃ holds
HT b₄,b₂ in Support (HM b₄,b₂)

proof end;

Lemma25: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ st HC b₄,b₂ = 0. b₃ holds
Support (HM b₄,b₂) = {}

proof end;

registration

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non trivial ZeroStr ;
let c₄ be non-zero Polynomial of c₁,c₃;
cluster HM a₄,a₂ -> non-zero ;
coherence

proof end;

cluster HC a₄,a₂ -> non-zero ;
coherence

proof end;

end;

Lemma26: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being Monomial of b₁,b₃ holds
( HT b₄,b₂ = term b₄ & HC b₄,b₂ = coefficient b₄ & HM b₄,b₂ = b₄ )

proof end;

theorem Th17: :: TERMORD:17

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being Polynomial of b₁,b₃ holds
( HC b₄,b₂ = 0. b₃ iff b₄ = 0_ b₁,b₃ ) by Lemma22;

theorem Th18: :: TERMORD:18

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ holds (HM b₄,b₂) . (HT b₄,b₂) = b₄ . (HT b₄,b₂) by Lemma23;

theorem Th19: :: TERMORD:19

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃
for b₅ being bag of b₁ st b₅ <> HT b₄,b₂ holds
(HM b₄,b₂) . b₅ = 0. b₃

proof end;

Lemma28: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ holds
( Support (HM b₄,b₂) = {} or Support (HM b₄,b₂) = {(HT b₄,b₂)} )

proof end;

theorem Th20: :: TERMORD:20

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ holds Support (HM b₄,b₂) c= Support b₄

proof end;

theorem Th21: :: TERMORD:21

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ holds
( Support (HM b₄,b₂) = {} or Support (HM b₄,b₂) = {(HT b₄,b₂)} ) by Lemma28;

theorem Th22: :: TERMORD:22

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ holds
( term (HM b₄,b₂) = HT b₄,b₂ & coefficient (HM b₄,b₂) = HC b₄,b₂ )

proof end;

theorem Th23: :: TERMORD:23

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being Monomial of b₁,b₃ holds
( HT b₄,b₂ = term b₄ & HC b₄,b₂ = coefficient b₄ & HM b₄,b₂ = b₄ ) by Lemma26;

theorem Th24: :: TERMORD:24

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being ConstPoly of b₁,b₃ holds
( HT b₄,b₂ = EmptyBag b₁ & HC b₄,b₂ = b₄ . (EmptyBag b₁) )

proof end;

theorem Th25: :: TERMORD:25

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being Element of b₃ holds
( HT (b₄ | b₁,b₃),b₂ = EmptyBag b₁ & HC (b₄ | b₁,b₃),b₂ = b₄ )

proof end;

theorem Th26: :: TERMORD:26

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ holds HT (HM b₄,b₂),b₂ = HT b₄,b₂

proof end;

theorem Th27: :: TERMORD:27

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being Polynomial of b₁,b₃ holds HC (HM b₄,b₂),b₂ = HC b₄,b₂

proof end;

theorem Th28: :: TERMORD:28

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being Polynomial of b₁,b₃ holds HM (HM b₄,b₂),b₂ = HM b₄,b₂ by Lemma26;

Lemma30: for b₁ being set
for b₂ being Subset of b₁
for b₃ being Order of b₁ st b₃ is_linear-order holds
b₃ linearly_orders b₂

proof end;

Lemma31: for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable unital distributive left_zeroed non trivial doubleLoopStr
for b₄, b₅ being non-zero Polynomial of b₁,b₃ holds (b₄ *' b₅) . ((HT b₄,b₂) + (HT b₅,b₂)) = (b₄ . (HT b₄,b₂)) * (b₅ . (HT b₅,b₂))

proof end;

theorem Th29: :: TERMORD:29

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable unital distributive left_zeroed non trivial domRing-like doubleLoopStr
for b₄, b₅ being non-zero Polynomial of b₁,b₃ holds (HT b₄,b₂) + (HT b₅,b₂) in Support (b₄ *' b₅)

proof end;

theorem Th30: :: TERMORD:30

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for b₃, b₄ being Polynomial of b₁,b₂ holds Support (b₃ *' b₄) c= { (b₅ + b₆) where B is Element of Bags b₁, B is Element of Bags b₁ : ( b₅ in Support b₃ & b₆ in Support b₄ ) }

proof end;

theorem Th31: :: TERMORD:31

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₄, b₅ being non-zero Polynomial of b₁,b₃ holds HT (b₄ *' b₅),b₂ = (HT b₄,b₂) + (HT b₅,b₂)

proof end;

theorem Th32: :: TERMORD:32

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₄, b₅ being non-zero Polynomial of b₁,b₃ holds HC (b₄ *' b₅),b₂ = (HC b₄,b₂) * (HC b₅,b₂)

proof end;

theorem Th33: :: TERMORD:33

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable unital distributive non trivial domRing-like doubleLoopStr
for b₄, b₅ being non-zero Polynomial of b₁,b₃ holds HM (b₄ *' b₅),b₂ = (HM b₄,b₂) *' (HM b₅,b₂)

proof end;

theorem Th34: :: TERMORD:34

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty right_zeroed LoopStr
for b₄, b₅ being Polynomial of b₁,b₃ holds HT (b₄ + b₅),b₂ <= max (HT b₄,b₂),(HT b₅,b₂),b₂,b₂

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₄ be Polynomial of c₁,c₃;
func Red c₄,c₂ -> Polynomial of a₁,a₃ equals :: TERMORD:def 9
a₄ - (HM a₄,a₂);
coherence ;

end;

:: deftheorem Def9 defines Red TERMORD:def 9 :

Lemma36: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃ holds not HT b₄,b₂ in Support (Red b₄,b₂)

proof end;

Lemma37: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being bag of b₁ st b₅ in Support b₄ & b₅ <> HT b₄,b₂ holds
b₅ in Support (Red b₄,b₂)

proof end;

Lemma38: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃ holds Support (Red b₄,b₂) = (Support b₄) \ {(HT b₄,b₂)}

proof end;

theorem Th35: :: TERMORD:35

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃ holds Support (Red b₄,b₂) c= Support b₄

proof end;

theorem Th36: :: TERMORD:36

Lemma39: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃ holds (Red b₄,b₂) . (HT b₄,b₂) = 0. b₃

proof end;

Lemma40: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being bag of b₁ st b₅ <> HT b₄,b₂ holds
(Red b₄,b₂) . b₅ = b₄ . b₅

proof end;

theorem Th37: :: TERMORD:37

proof end;

theorem Th38: :: TERMORD:38

proof end;

theorem Th39: :: TERMORD:39

theorem Th40: :: TERMORD:40