:: POLYRED semantic presentation

registration

let c₁ be Ordinal;
let c₂ be non trivial ZeroStr ;
cluster non-zero Relation of Bags a₁,the carrier of a₂;
existence

proof end;

end;

registration

cluster non trivial doubleLoopStr ;
existence

proof end;

end;

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

Lemma2: for b₁ being Ordinal
for b₂, b₃, b₄ being bag of b₁ st b₂ <=' b₃ holds
b₂ + b₄ <=' b₃ + b₄

proof end;

Lemma3: for b₁ being Ordinal
for b₂, b₃ being bag of b₁ st b₂ <=' b₃ & b₃ <=' b₂ holds
b₂ = b₃

proof end;

Lemma4: for b₁ being Ordinal
for b₂, b₃ being bag of b₁ holds
( not b₂ < b₃ iff b₃ <=' b₂ )

proof end;

Lemma5: for b₁ being Ordinal
for b₂ being non trivial ZeroStr
for b₃ being finite-Support non-zero Series of b₁,b₂ ex b₄ being bag of b₁ st
( b₃ . b₄ <> 0. b₂ & ( for b₅ being bag of b₁ st b₄ < b₅ holds
b₃ . b₅ = 0. b₂ ) )

proof end;

Lemma6: for b₁ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁
for b₄ being Nat st len b₂ = b₄ + 1 & b₃ = b₂ | (Seg b₄) holds
Sum b₂ = (Sum b₃) + (b₂ /. (len b₂))

proof end;

registration

let c₁ be Ordinal;
let c₂ be unital add-associative right_zeroed right_complementable distributive domRing-like left_zeroed non trivial doubleLoopStr ;
let c₃, c₄ be finite-Support non-zero Series of c₁,c₂;
cluster a₃ *' a₄ -> non-zero ;
coherence

proof end;

end;

theorem Th1: :: POLYRED:1

for b₁ being set
for b₂ being non empty Abelian add-associative right_zeroed right_complementable LoopStr
for b₃, b₄ being Series of b₁,b₂ holds - (b₃ + b₄) = (- b₃) + (- b₄)

proof end;

theorem Th2: :: POLYRED:2

for b₁ being set
for b₂ being non empty left_zeroed LoopStr
for b₃ being Series of b₁,b₂ holds (0_ b₁,b₂) + b₃ = b₃

proof end;

theorem Th3: :: POLYRED:3

for b₁ being set
for b₂ being non empty add-associative right_zeroed right_complementable LoopStr
for b₃ being Series of b₁,b₂ holds
( (- b₃) + b₃ = 0_ b₁,b₂ & b₃ + (- b₃) = 0_ b₁,b₂ )

proof end;

theorem Th4: :: POLYRED:4

for b₁ being set
for b₂ being non empty add-associative right_zeroed right_complementable LoopStr
for b₃ being Series of b₁,b₂ holds b₃ - (0_ b₁,b₂) = b₃

proof end;

theorem Th5: :: POLYRED:5

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

proof end;

Lemma12: for b₁ being Ordinal
for b₂ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being Element of (Polynom-Ring b₁,b₂) st b₃ = b₄ holds
- b₃ = - b₄

proof end;

theorem Th6: :: POLYRED:6

for b₁ being Ordinal
for b₂ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₃, b₄ being Polynomial of b₁,b₂ holds
( - (b₃ *' b₄) = (- b₃) *' b₄ & - (b₃ *' b₄) = b₃ *' (- b₄) )

proof end;

Lemma14: for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable LoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being Monomial of b₁,b₂
for b₅ being bag of b₁ st b₅ <> term b₄ holds
b₄ . b₅ = 0. b₂

proof end;

theorem Th7: :: POLYRED:7

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being Monomial of b₁,b₂
for b₅ being bag of b₁ holds (b₄ *' b₃) . ((term b₄) + b₅) = (b₄ . (term b₄)) * (b₃ . b₅)

proof end;

theorem Th8: :: POLYRED:8

for b₁ being set
for b₂ being non empty right_zeroed left-distributive add-left-cancelable doubleLoopStr
for b₃ being Series of b₁,b₂ holds (0. b₂) * b₃ = 0_ b₁,b₂

proof end;

theorem Th9: :: POLYRED:9

for b₁ being set
for b₂ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₃ being Series of b₁,b₂
for b₄ being Element of b₂ holds
( - (b₄ * b₃) = (- b₄) * b₃ & - (b₄ * b₃) = b₄ * (- b₃) )

proof end;

theorem Th10: :: POLYRED:10

for b₁ being set
for b₂ being non empty left-distributive doubleLoopStr
for b₃ being Series of b₁,b₂
for b₄, b₅ being Element of b₂ holds (b₄ * b₃) + (b₅ * b₃) = (b₄ + b₅) * b₃

proof end;

theorem Th11: :: POLYRED:11

for b₁ being set
for b₂ being non empty associative multLoopStr_0
for b₃ being Series of b₁,b₂
for b₄, b₅ being Element of b₂ holds (b₄ * b₅) * b₃ = b₄ * (b₅ * b₃)

proof end;

theorem Th12: :: POLYRED:12

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

proof end;

definition

let c₁ be Ordinal;
let c₂ be bag of c₁;
let c₃ be non empty ZeroStr ;
let c₄ be Series of c₁,c₃;
func c₂ *' c₄ -> Series of a₁,a₃ means :Def1: :: POLYRED:def 1
for b₁ being bag of a₁ st a₂ divides b₁ holds
( a₅ . b₁ = a₄ . (b₁ -' a₂) & ( for b₂ being bag of a₁ st not a₂ divides b₂ holds
a₅ . b₂ = 0. a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines *' POLYRED:def 1 :

Lemma22: for b₁ being Ordinal
for b₂, b₃ being bag of b₁
for b₄ being non empty ZeroStr
for b₅ being Series of b₁,b₄ holds (b₂ *' b₅) . (b₃ + b₂) = b₅ . b₃

proof end;

Lemma23: for b₁ being Ordinal
for b₂ being non empty ZeroStr
for b₃ being Polynomial of b₁,b₂
for b₄ being bag of b₁ holds Support (b₄ *' b₃) c= { (b₄ + b₅) where B is Element of Bags b₁ : b₅ in Support b₃ }

proof end;

registration

let c₁ be Ordinal;
let c₂ be bag of c₁;
let c₃ be non empty ZeroStr ;
let c₄ be finite-Support Series of c₁,c₃;
cluster a₂ *' a₄ -> finite-Support ;
coherence

proof end;

end;

theorem Th13: :: POLYRED:13

for b₁ being Ordinal
for b₂, b₃ being bag of b₁
for b₄ being non empty ZeroStr
for b₅ being Series of b₁,b₄ holds (b₂ *' b₅) . (b₃ + b₂) = b₅ . b₃ by Lemma22;

theorem Th14: :: POLYRED:14

for b₁ being Ordinal
for b₂ being non empty ZeroStr
for b₃ being Polynomial of b₁,b₂
for b₄ being bag of b₁ holds Support (b₄ *' b₃) c= { (b₄ + b₅) where B is Element of Bags b₁ : b₅ in Support b₃ } by Lemma23;

theorem Th15: :: POLYRED:15

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non trivial ZeroStr
for b₄ being non-zero Polynomial of b₁,b₃
for b₅ being bag of b₁ holds HT (b₅ *' b₄),b₂ = b₅ + (HT b₄,b₂)

proof end;

theorem Th16: :: POLYRED:16

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being Polynomial of b₁,b₃
for b₅, b₆ being bag of b₁ st b₆ in Support (b₅ *' b₄) holds
b₆ <= b₅ + (HT b₄,b₂),b₂

proof end;

theorem Th17: :: POLYRED:17

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being Series of b₁,b₃ holds (EmptyBag b₁) *' b₄ = b₄

proof end;

theorem Th18: :: POLYRED:18

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty ZeroStr
for b₄ being Series of b₁,b₃
for b₅, b₆ being bag of b₁ holds (b₅ + b₆) *' b₄ = b₅ *' (b₆ *' b₄)

proof end;

theorem Th19: :: POLYRED:19

for b₁ being Ordinal
for b₂ being add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being Element of b₂ holds Support (b₄ * b₃) c= Support b₃

proof end;

theorem Th20: :: POLYRED:20

for b₁ being Ordinal
for b₂ being domRing-like non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being non-zero Element of b₂ holds Support b₃ c= Support (b₄ * b₃)

proof end;

theorem Th21: :: POLYRED:21

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

proof end;

theorem Th22: :: POLYRED:22

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

proof end;

theorem Th23: :: POLYRED:23

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

proof end;

registration

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
cluster RelStr(# (Bags a₁),a₂ #) -> connected ;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂ be admissible TermOrder of c₁;
cluster RelStr(# (Bags a₁),a₂ #) -> well_founded ;
coherence

proof end;

end;

Lemma30: 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 Support b₄ in Fin the carrier of RelStr(# (Bags b₁),b₂ #)

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty ZeroStr ;
let c₄, c₅ be Polynomial of c₁,c₃;
pred c₄ <= c₅,c₂ means :Def2: :: POLYRED:def 2
[(Support a₄),(Support a₅)] in FinOrd RelStr(# (Bags a₁),a₂ #);

end;

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

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be non empty ZeroStr ;
let c₄, c₅ be Polynomial of c₁,c₃;
pred c₄ < c₅,c₂ means :Def3: :: POLYRED:def 3
( a₄ <= a₅,a₂ & Support a₄ <> Support a₅ );

end;

:: deftheorem Def3 defines < POLYRED:def 3 :

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 Support c₄,c₂ -> Element of Fin the carrier of RelStr(# (Bags a₁),a₂ #) equals :: POLYRED:def 4
Support a₄;
coherence by Lemma30;

end;

:: deftheorem Def4 defines Support POLYRED:def 4 :

theorem Th24: :: POLYRED:24

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

proof end;

theorem Th25: :: POLYRED:25

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty LoopStr
for b₄ being Polynomial of b₁,b₃ holds b₄ <= b₄,b₂

proof end;

Lemma35: 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 0_ b₁,b₃ <= b₄,b₂

proof end;

theorem Th26: :: POLYRED:26

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty LoopStr
for b₄, b₅ being Polynomial of b₁,b₃ holds
( ( b₄ <= b₅,b₂ & b₅ <= b₄,b₂ ) iff Support b₄ = Support b₅ )

proof end;

theorem Th27: :: POLYRED:27

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty LoopStr
for b₄, b₅, b₆ being Polynomial of b₁,b₃ st b₄ <= b₅,b₂ & b₅ <= b₆,b₂ holds
b₄ <= b₆,b₂

proof end;

theorem Th28: :: POLYRED:28

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty LoopStr
for b₄, b₅ being Polynomial of b₁,b₃ holds
( b₄ <= b₅,b₂ or b₅ <= b₄,b₂ )

proof end;

theorem Th29: :: POLYRED:29

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty LoopStr
for b₄, b₅ being Polynomial of b₁,b₃ holds
( b₄ <= b₅,b₂ iff not b₅ < b₄,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 [(HT b₄,b₂),b₅] in b₂ & b₅ <> HT b₄,b₂ holds
b₄ . b₅ = 0. b₃

proof end;

Lemma41: for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being Polynomial of b₁,b₃ st HT b₄,b₂ = EmptyBag b₁ holds
Red b₄,b₂ = 0_ b₁,b₃

proof end;

Lemma42: for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄, b₅ being Polynomial of b₁,b₃ holds
( b₄ < b₅,b₂ iff ( ( b₄ = 0_ b₁,b₃ & b₅ <> 0_ b₁,b₃ ) or HT b₄,b₂ < HT b₅,b₂,b₂ or ( HT b₄,b₂ = HT b₅,b₂ & Red b₄,b₂ < Red b₅,b₂,b₂ ) ) )

proof end;

theorem Th30: :: POLYRED:30

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 0_ b₁,b₃ <= b₄,b₂ by Lemma35;

Lemma43: for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄, b₅ being Polynomial of b₁,b₃ st b₅ <> 0_ b₁,b₃ & HT b₄,b₂ = HT b₅,b₂ & Red b₄,b₂ <= Red b₅,b₂,b₂ holds
b₄ <= b₅,b₂

proof end;

theorem Th31: :: POLYRED:31

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being unital add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₄ being non empty Subset of (Polynom-Ring b₁,b₃) ex b₅ being Polynomial of b₁,b₃ st
( b₅ in b₄ & ( for b₆ being Polynomial of b₁,b₃ st b₆ in b₄ holds
b₅ <= b₆,b₂ ) )

proof end;

theorem Th32: :: POLYRED:32

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄, b₅ being Polynomial of b₁,b₃ holds
( b₄ < b₅,b₂ iff ( ( b₄ = 0_ b₁,b₃ & b₅ <> 0_ b₁,b₃ ) or HT b₄,b₂ < HT b₅,b₂,b₂ or ( HT b₄,b₂ = HT b₅,b₂ & Red b₄,b₂ < Red b₅,b₂,b₂ ) ) ) by Lemma42;

theorem Th33: :: POLYRED:33

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being add-associative right_zeroed right_complementable non trivial LoopStr
for b₄ being non-zero Polynomial of b₁,b₃ holds Red b₄,b₂ < HM b₄,b₂,b₂

proof end;

theorem Th34: :: POLYRED:34

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 HM b₄,b₂ <= b₄,b₂

proof end;

theorem Th35: :: POLYRED:35

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄, c₅, c₆ be Polynomial of c₁,c₃;
let c₇ be bag of c₁;
pred c₄ reduces_to c₆,c₅,c₇,c₂ means :Def5: :: POLYRED:def 5
( a₄ <> 0_ a₁,a₃ & a₅ <> 0_ a₁,a₃ & a₇ in Support a₄ & ex b₁ being bag of a₁ st
( b₁ + (HT a₅,a₂) = a₇ & a₆ = a₄ - (((a₄ . a₇) / (HC a₅,a₂)) * (b₁ *' a₅)) ) );

end;

:: deftheorem Def5 defines reduces_to POLYRED:def 5 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄, c₅, c₆ be Polynomial of c₁,c₃;
pred c₄ reduces_to c₆,c₅,c₂ means :Def6: :: POLYRED:def 6
ex b₁ being bag of a₁ st a₄ reduces_to a₆,a₅,b₁,a₂;

end;

:: deftheorem Def6 defines reduces_to POLYRED:def 6 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄, c₅ be Polynomial of c₁,c₃;
let c₆ be Subset of (Polynom-Ring c₁,c₃);
pred c₄ reduces_to c₅,c₆,c₂ means :Def7: :: POLYRED:def 7
ex b₁ being Polynomial of a₁,a₃ st
( b₁ in a₆ & a₄ reduces_to a₅,b₁,a₂ );

end;

:: deftheorem Def7 defines reduces_to POLYRED:def 7 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄, c₅ be Polynomial of c₁,c₃;
pred c₄ is_reducible_wrt c₅,c₂ means :Def8: :: POLYRED:def 8
ex b₁ being Polynomial of a₁,a₃ st a₄ reduces_to b₁,a₅,a₂;

end;

:: deftheorem Def8 defines is_reducible_wrt POLYRED:def 8 :

notation

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄, c₅ be Polynomial of c₁,c₃;
antonym c₄ is_irreducible_wrt c₅,c₂ for c₄ is_reducible_wrt c₅,c₂;
antonym c₄ is_in_normalform_wrt c₅,c₂ for c₄ is_reducible_wrt c₅,c₂;

end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄ be Polynomial of c₁,c₃;
let c₅ be Subset of (Polynom-Ring c₁,c₃);
pred c₄ is_reducible_wrt c₅,c₂ means :: POLYRED:def 9
ex b₁ being Polynomial of a₁,a₃ st a₄ reduces_to b₁,a₅,a₂;

end;

:: deftheorem Def9 defines is_reducible_wrt POLYRED:def 9 :

notation

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄ be Polynomial of c₁,c₃;
let c₅ be Subset of (Polynom-Ring c₁,c₃);
antonym c₄ is_irreducible_wrt c₅,c₂ for c₄ is_reducible_wrt c₅,c₂;
antonym c₄ is_in_normalform_wrt c₅,c₂ for c₄ is_reducible_wrt c₅,c₂;

end;

definition

end;

:: deftheorem Def10 defines top_reduces_to POLYRED:def 10 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄, c₅ be Polynomial of c₁,c₃;
pred c₄ is_top_reducible_wrt c₅,c₂ means :: POLYRED:def 11
ex b₁ being Polynomial of a₁,a₃ st a₄ top_reduces_to b₁,a₅,a₂;

end;

:: deftheorem Def11 defines is_top_reducible_wrt POLYRED:def 11 :

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄ be Polynomial of c₁,c₃;
let c₅ be Subset of (Polynom-Ring c₁,c₃);
pred c₄ is_top_reducible_wrt c₅,c₂ means :: POLYRED:def 12
ex b₁ being Polynomial of a₁,a₃ st
( b₁ in a₅ & a₄ is_top_reducible_wrt b₁,a₂ );

end;

:: deftheorem Def12 defines is_top_reducible_wrt POLYRED:def 12 :

theorem Th36: :: POLYRED:36

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being Polynomial of b₁,b₃
for b₅ being non-zero Polynomial of b₁,b₃ holds
( b₄ is_reducible_wrt b₅,b₂ iff ex b₆ being bag of b₁ st
( b₆ in Support b₄ & HT b₅,b₂ divides b₆ ) )

proof end;

Lemma52: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄, b₅, b₆ being Polynomial of b₁,b₃
for b₇ being bag of b₁ st b₄ reduces_to b₆,b₅,b₇,b₂ holds
not b₇ in Support b₆

proof end;

theorem Th37: :: POLYRED:37

proof end;

theorem Th38: :: POLYRED:38

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃
for b₆ being non-zero Monomial of b₁,b₃ st b₄ reduces_to b₄ - (b₆ *' b₅),b₅,b₂ holds
HT (b₆ *' b₅),b₂ in Support b₄

proof end;

theorem Th39: :: POLYRED:39

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄, b₅, b₆ being Polynomial of b₁,b₃
for b₇ being bag of b₁ st b₄ reduces_to b₆,b₅,b₇,b₂ holds
not b₇ in Support b₆ by Lemma52;

theorem Th40: :: POLYRED:40

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄, b₅, b₆ being Polynomial of b₁,b₃
for b₇, b₈ being bag of b₁ st b₇ < b₈,b₂ & b₄ reduces_to b₆,b₅,b₇,b₂ holds
( b₈ in Support b₆ iff b₈ in Support b₄ )

proof end;

theorem Th41: :: POLYRED:41

proof end;

theorem Th42: :: POLYRED:42

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄, b₅, b₆ being Polynomial of b₁,b₃ st b₄ reduces_to b₆,b₅,b₂ holds
for b₇ being bag of b₁ st b₇ in Support b₆ holds
b₇ <= HT b₄,b₂,b₂

proof end;

theorem Th43: :: POLYRED:43

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄, b₅, b₆ being Polynomial of b₁,b₃ st b₄ reduces_to b₆,b₅,b₂ holds
b₆ < b₄,b₂

proof end;

definition

let c₁ be Ordinal;
let c₂ be connected TermOrder of c₁;
let c₃ be unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr ;
let c₄ be Subset of (Polynom-Ring c₁,c₃);
func PolyRedRel c₄,c₂ -> Relation of the carrier of (Polynom-Ring a₁,a₃) \ {(0_ a₁,a₃)},the carrier of (Polynom-Ring a₁,a₃) means :Def13: :: POLYRED:def 13
for b₁, b₂ being Polynomial of a₁,a₃ holds
( [b₁,b₂] in a₅ iff b₁ reduces_to b₂,a₄,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines PolyRedRel POLYRED:def 13 :

Lemma59: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄, b₅, b₆ being Polynomial of b₁,b₃ st b₄ reduces_to b₅,b₆,b₂ holds
( b₄ <> 0_ b₁,b₃ & b₆ <> 0_ b₁,b₃ )

proof end;

theorem Th44: :: POLYRED:44

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄, b₅ being Polynomial of b₁,b₃
for b₆ being Subset of (Polynom-Ring b₁,b₃) st PolyRedRel b₆,b₂ reduces b₄,b₅ holds
( b₅ <= b₄,b₂ & ( b₅ = 0_ b₁,b₃ or HT b₅,b₂ <= HT b₄,b₂,b₂ ) )

proof end;

registration

let c₁ be Nat;
let c₂ be connected admissible TermOrder of c₁;
let c₃ be non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr ;
let c₄ be Subset of (Polynom-Ring c₁,c₃);
cluster PolyRedRel a₄,a₂ -> strongly-normalizing ;
coherence

proof end;

end;

theorem Th45: :: POLYRED:45

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like left_zeroed non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being Polynomial of b₁,b₃ st b₅ in b₄ holds
PolyRedRel b₄,b₂ reduces b₆ *' b₅, 0_ b₁,b₃

proof end;

theorem Th46: :: POLYRED:46

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being Polynomial of b₁,b₃
for b₇ being non-zero Monomial of b₁,b₃ st b₅ reduces_to b₆,b₄,b₂ holds
b₇ *' b₅ reduces_to b₇ *' b₆,b₄,b₂

proof end;

theorem Th47: :: POLYRED:47

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being Polynomial of b₁,b₃
for b₇ being Monomial of b₁,b₃ st PolyRedRel b₄,b₂ reduces b₅,b₆ holds
PolyRedRel b₄,b₂ reduces b₇ *' b₅,b₇ *' b₆

proof end;

theorem Th48: :: POLYRED:48

for b₁ being Ordinal
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅ being Polynomial of b₁,b₃
for b₆ being Monomial of b₁,b₃ st PolyRedRel b₄,b₂ reduces b₅, 0_ b₁,b₃ holds
PolyRedRel b₄,b₂ reduces b₆ *' b₅, 0_ b₁,b₃

proof end;

theorem Th49: :: POLYRED:49

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆, b₇, b₈ being Polynomial of b₁,b₃ st b₅ - b₆ = b₇ & PolyRedRel b₄,b₂ reduces b₇,b₈ holds
ex b₉, b₁₀ being Polynomial of b₁,b₃ st
( b₉ - b₁₀ = b₈ & PolyRedRel b₄,b₂ reduces b₅,b₉ & PolyRedRel b₄,b₂ reduces b₆,b₁₀ )

proof end;

theorem Th50: :: POLYRED:50

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being Polynomial of b₁,b₃ st PolyRedRel b₄,b₂ reduces b₅ - b₆, 0_ b₁,b₃ holds
b₅,b₆ are_convergent_wrt PolyRedRel b₄,b₂

proof end;

theorem Th51: :: POLYRED:51

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being Polynomial of b₁,b₃ st PolyRedRel b₄,b₂ reduces b₅ - b₆, 0_ b₁,b₃ holds
b₅,b₆ are_convertible_wrt PolyRedRel b₄,b₂

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂ be Subset of c₁;
let c₃, c₄ be Element of c₁;
pred c₃,c₄ are_congruent_mod c₂ means :Def14: :: POLYRED:def 14
a₃ - a₄ in a₂;

end;

:: deftheorem Def14 defines are_congruent_mod POLYRED:def 14 :

theorem Th52: :: POLYRED:52

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive left_zeroed doubleLoopStr
for b₂ being non empty right-ideal Subset of b₁
for b₃ being Element of b₁ holds b₃,b₃ are_congruent_mod b₂

proof end;

theorem Th53: :: POLYRED:53

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for b₂ being non empty right-ideal Subset of b₁
for b₃, b₄ being Element of b₁ st b₃,b₄ are_congruent_mod b₂ holds
b₄,b₃ are_congruent_mod b₂

proof end;

theorem Th54: :: POLYRED:54

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being non empty add-closed Subset of b₁
for b₃, b₄, b₅ being Element of b₁ st b₃,b₄ are_congruent_mod b₂ & b₄,b₅ are_congruent_mod b₂ holds
b₃,b₅ are_congruent_mod b₂

proof end;

theorem Th55: :: POLYRED:55

for b₁ being unital associative Abelian add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr
for b₂ being non empty add-closed Subset of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st b₃,b₄ are_congruent_mod b₂ & b₅,b₆ are_congruent_mod b₂ holds
b₃ + b₅,b₄ + b₆ are_congruent_mod b₂

proof end;

theorem Th56: :: POLYRED:56

for b₁ being non empty commutative add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being non empty add-closed right-ideal Subset of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st b₃,b₄ are_congruent_mod b₂ & b₅,b₆ are_congruent_mod b₂ holds
b₃ * b₅,b₄ * b₆ are_congruent_mod b₂

proof end;

Lemma69: for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅ being non-zero Polynomial of b₁,b₃
for b₆ being Polynomial of b₁,b₃
for b₇, b₈ being Element of (Polynom-Ring b₁,b₃) st b₅ = b₇ & b₆ = b₈ & b₅ reduces_to b₆,b₄,b₂ holds
b₇,b₈ are_congruent_mod b₄ -Ideal

proof end;

theorem Th57: :: POLYRED:57

for b₁ being Ordinal
for b₂ being connected TermOrder of b₁
for b₃ being unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non trivial doubleLoopStr
for b₄ being Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being Element of (Polynom-Ring b₁,b₃) st b₅,b₆ are_convertible_wrt PolyRedRel b₄,b₂ holds
b₅,b₆ are_congruent_mod b₄ -Ideal

proof end;

Lemma71: for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being non empty Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆, b₇ being Element of (Polynom-Ring b₁,b₃) st b₆ in b₄ & b₆ <> 0_ b₁,b₃ & b₇ <> 0_ b₁,b₃ holds
b₅,b₅ + (b₇ * b₆) are_convertible_wrt PolyRedRel b₄,b₂

proof end;

theorem Th58: :: POLYRED:58

for b₁ being Nat
for b₂ being connected admissible TermOrder of b₁
for b₃ being non empty unital associative commutative Abelian add-associative right_zeroed right_complementable distributive Field-like non degenerated doubleLoopStr
for b₄ being non empty Subset of (Polynom-Ring b₁,b₃)
for b₅, b₆ being Element of (Polynom-Ring b₁,b₃) st b₅,b₆ are_congruent_mod b₄ -Ideal holds
b₅,b₆ are_convertible_wrt PolyRedRel b₄,b₂

proof end;

theorem Th59: :: POLYRED:59

proof end;

theorem Th60: :: POLYRED:60

proof end;