:: Polynomial Reduction
:: by Christoph Schwarzweller
::
:: Received December 20, 2002
:: Copyright (c) 2002-2011 Association of Mizar Users

begin

registration

let n be Ordinal;
let R be non trivial ZeroStr ;
cluster non zero Relation-like Function-like total V42( Bags n, the carrier of R) non-zero monomial-like finite-Support Element of bool [:(Bags n), the carrier of R:];
existence
ex b₁ being Monomial of n,R st b₁ is non-zero

proof end;

end;

registration

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible V95() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr ;
existence
not for b₁ being Field holds b₁ is trivial

proof end;

end;

Lm1: for X being set
for S being Subset of X
for R being Order of X st R is being_linear-order holds
R linearly_orders S

proof end;

Lm2: for n being Ordinal
for b1, b2, b3 being bag of n st b1 <=' b2 holds
b1 + b3 <=' b2 + b3

proof end;

Lm3: for n being Ordinal
for b1, b2 being bag of n st b1 <=' b2 & b2 <=' b1 holds
b1 = b2

proof end;

Lm4: for n being Ordinal
for b1, b2 being bag of n holds
( not b1 < b2 iff b2 <=' b1 )

proof end;

Lm5: for n being Ordinal
for L being non trivial ZeroStr
for p being non-zero finite-Support Series of n,L ex b being bag of n st
( p . b <> 0. L & ( for b9 being bag of n st b < b9 holds
p . b9 = 0. L ) )

proof end;

Lm6: for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for f, g being FinSequence of the carrier of L
for n being Nat st len f = n + 1 & g = f | (Seg n) holds
Sum f = (Sum g) + (f /. (len f))

proof end;

registration

let n be Ordinal;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr ;
let p, q be non-zero finite-Support Series of n,L;
cluster p *' q -> non-zero ;
coherence
p *' q is non-zero

proof end;

end;

begin

theorem Th1: :: POLYRED:1

for X being set
for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p, q being Series of X,L holds - (p + q) = (- p) + (- q)

proof end;

theorem Th2: :: POLYRED:2

for X being set
for L being non empty left_zeroed addLoopStr
for p being Series of X,L holds (0_ (X,L)) + p = p

proof end;

theorem Th3: :: POLYRED:3

for X being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of X,L holds
( (- p) + p = 0_ (X,L) & p + (- p) = 0_ (X,L) )

proof end;

theorem Th4: :: POLYRED:4

for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p - (0_ (n,L)) = p

proof end;

theorem Th5: :: POLYRED:5

for n being Ordinal
for L being non empty left_add-cancelable right_complementable left-distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (0_ (n,L)) *' p = 0_ (n,L)

proof end;

Lm7: for n being Ordinal
for L being non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L
for q being Element of (Polynom-Ring (n,L)) st p = q holds
- p = - q

proof end;

theorem Th6: :: POLYRED:6

for n being Ordinal
for L being non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L holds
( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) )

proof end;

Lm8: for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for m being Monomial of n,L
for b being bag of n st b <> term m holds
m . b = 0. L

proof end;

theorem Th7: :: POLYRED:7

for n being Ordinal
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L
for m being Monomial of n,L
for b being bag of n holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)

proof end;

theorem Th8: :: POLYRED:8

for X being set
for L being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr
for p being Series of X,L holds (0. L) * p = 0_ (X,L)

proof end;

theorem Th9: :: POLYRED:9

for X being set
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Series of X,L
for a being Element of L holds
( - (a * p) = (- a) * p & - (a * p) = a * (- p) )

proof end;

theorem Th10: :: POLYRED:10

for X being set
for L being non empty left-distributive doubleLoopStr
for p being Series of X,L
for a, a9 being Element of L holds (a * p) + (a9 * p) = (a + a9) * p

proof end;

theorem Th11: :: POLYRED:11

for X being set
for L being non empty associative multLoopStr_0
for p being Series of X,L
for a, a9 being Element of L holds (a * a9) * p = a * (a9 * p)

proof end;

theorem Th12: :: POLYRED:12

for n being Ordinal
for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p, p9 being Series of n,L
for a being Element of L holds a * (p *' p9) = p *' (a * p9)

proof end;

begin

definition

let n be Ordinal;
let b be bag of n;
let L be non empty ZeroStr ;
let p be Series of n,L;
func b *' p -> Series of n,L means :Def1: :: POLYRED:def 1
for b9 being bag of n st b divides b9 holds
( it . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
it . b9 = 0. L ) );
existence
ex b₁ being Series of n,L st
for b9 being bag of n st b divides b9 holds
( b₁ . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
b₁ . b9 = 0. L ) )

proof end;

uniqueness
for b₁, b₂ being Series of n,L st ( for b9 being bag of n st b divides b9 holds
( b₁ . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
b₁ . b9 = 0. L ) ) ) & ( for b9 being bag of n st b divides b9 holds
( b₂ . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
b₂ . b9 = 0. L ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines *' POLYRED:def 1 :
for n being Ordinal
for b being bag of n
for L being non empty ZeroStr
for p, b₅ being Series of n,L holds
( b₅ = b *' p iff for b9 being bag of n st b divides b9 holds
( b₅ . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
b₅ . b9 = 0. L ) ) );

Lm9: for n being Ordinal
for b, b9 being bag of n
for L being non empty ZeroStr
for p being Series of n,L holds (b *' p) . (b9 + b) = p . b9

proof end;

Lm10: for n being Ordinal
for L being non empty ZeroStr
for p being Polynomial of n,L
for b being bag of n holds Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p }

proof end;

registration

let n be Ordinal;
let b be bag of n;
let L be non empty ZeroStr ;
let p be finite-Support Series of n,L;
cluster b *' p -> finite-Support ;
coherence
b *' p is finite-Support

proof end;

end;

theorem :: POLYRED:13

for n being Ordinal
for b, b9 being bag of n
for L being non empty ZeroStr
for p being Series of n,L holds (b *' p) . (b9 + b) = p . b9 by Lm9;

theorem :: POLYRED:14

for n being Ordinal
for L being non empty ZeroStr
for p being Polynomial of n,L
for b being bag of n holds Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p } by Lm10;

theorem Th15: :: POLYRED:15

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L
for b being bag of n holds HT ((b *' p),T) = b + (HT (p,T))

proof end;

theorem Th16: :: POLYRED:16

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L
for b, b9 being bag of n st b9 in Support (b *' p) holds
b9 <= b + (HT (p,T)),T

proof end;

theorem :: POLYRED:17

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Series of n,L holds (EmptyBag n) *' p = p

proof end;

theorem Th18: :: POLYRED:18

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Series of n,L
for b1, b2 being bag of n holds (b1 + b2) *' p = b1 *' (b2 *' p)

proof end;

theorem Th19: :: POLYRED:19

for n being Ordinal
for L being non trivial right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L holds Support (a * p) c= Support p

proof end;

theorem :: POLYRED:20

for n being Ordinal
for L being non trivial domRing-like doubleLoopStr
for p being Polynomial of n,L
for a being non zero Element of L holds Support p c= Support (a * p)

proof end;

theorem Th21: :: POLYRED:21

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for a being non zero Element of L holds HT ((a * p),T) = HT (p,T)

proof end;

theorem Th22: :: POLYRED:22

for n being Ordinal
for L being non trivial right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L
for b being bag of n
for a being Element of L holds a * (b *' p) = (Monom (a,b)) *' p

proof end;

theorem :: POLYRED:23

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being non-zero Polynomial of n,L
for q being Polynomial of n,L
for m being non-zero Monomial of n,L st HT (p,T) in Support q holds
HT ((m *' p),T) in Support (m *' q)

proof end;

begin

registration

let n be Ordinal;
let T be connected TermOrder of n;
cluster RelStr(# (Bags n),T #) -> connected ;
coherence
RelStr(# (Bags n),T #) is connected

proof end;

end;

registration

let n be Nat;
let T be admissible TermOrder of n;
cluster RelStr(# (Bags n),T #) -> well_founded ;
coherence
RelStr(# (Bags n),T #) is well_founded

proof end;

end;

Lm11: for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds Support p in Fin the carrier of RelStr(# (Bags n),T #)

proof end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p, q be Polynomial of n,L;
pred p <= q,T means :Def2: :: POLYRED:def 2
[(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #);

end;

:: deftheorem Def2 defines <= POLYRED:def 2 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p, q being Polynomial of n,L holds
( p <= q,T iff [(Support p),(Support q)] in FinOrd RelStr(# (Bags n),T #) );

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p, q be Polynomial of n,L;
pred p < q,T means :Def3: :: POLYRED:def 3
( p <= q,T & Support p <> Support q );

end;

:: deftheorem Def3 defines < POLYRED:def 3 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p, q being Polynomial of n,L holds
( p < q,T iff ( p <= q,T & Support p <> Support q ) );

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty ZeroStr ;
let p be Polynomial of n,L;
func Support (p,T) -> Element of Fin the carrier of RelStr(# (Bags n),T #) equals :: POLYRED:def 4
Support p;
coherence
Support p is Element of Fin the carrier of RelStr(# (Bags n),T #) by Lm11;

end;

:: deftheorem defines Support POLYRED:def 4 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds Support (p,T) = Support p;

theorem Th24: :: POLYRED:24

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L holds PosetMax (Support (p,T)) = HT (p,T)

proof end;

theorem Th25: :: POLYRED:25

for n being Ordinal
for T being connected TermOrder of n
for L being non empty addLoopStr
for p being Polynomial of n,L holds p <= p,T

proof end;

Lm12: for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds 0_ (n,L) <= p,T

proof end;

theorem Th26: :: POLYRED:26

for n being Ordinal
for T being connected TermOrder of n
for L being non empty addLoopStr
for p, q being Polynomial of n,L holds
( ( p <= q,T & q <= p,T ) iff Support p = Support q )

proof end;

theorem Th27: :: POLYRED:27

for n being Ordinal
for T being connected TermOrder of n
for L being non empty addLoopStr
for p, q, r being Polynomial of n,L st p <= q,T & q <= r,T holds
p <= r,T

proof end;

theorem Th28: :: POLYRED:28

for n being Ordinal
for T being connected TermOrder of n
for L being non empty addLoopStr
for p, q being Polynomial of n,L holds
( p <= q,T or q <= p,T )

proof end;

theorem Th29: :: POLYRED:29

for n being Ordinal
for T being connected TermOrder of n
for L being non empty addLoopStr
for p, q being Polynomial of n,L holds
( p <= q,T iff not q < p,T )

proof end;

Lm13: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st [(HT (p,T)),b] in T & b <> HT (p,T) holds
p . b = 0. L

proof end;

Lm14: for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L st HT (p,T) = EmptyBag n holds
Red (p,T) = 0_ (n,L)

proof end;

Lm15: for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L holds
( p < q,T iff ( ( p = 0_ (n,L) & q <> 0_ (n,L) ) or HT (p,T) < HT (q,T),T or ( HT (p,T) = HT (q,T) & Red (p,T) < Red (q,T),T ) ) )

proof end;

theorem :: POLYRED:30

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds 0_ (n,L) <= p,T by Lm12;

Lm16: for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L st q <> 0_ (n,L) & HT (p,T) = HT (q,T) & Red (p,T) <= Red (q,T),T holds
p <= q,T

proof end;

theorem Th31: :: POLYRED:31

for n being Nat
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for P being non empty Subset of (Polynom-Ring (n,L)) ex p being Polynomial of n,L st
( p in P & ( for q being Polynomial of n,L st q in P holds
p <= q,T ) )

proof end;

theorem :: POLYRED:32

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of n,L holds
( p < q,T iff ( ( p = 0_ (n,L) & q <> 0_ (n,L) ) or HT (p,T) < HT (q,T),T or ( HT (p,T) = HT (q,T) & Red (p,T) < Red (q,T),T ) ) ) by Lm15;

theorem Th33: :: POLYRED:33

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being non-zero Polynomial of n,L holds Red (p,T) < HM (p,T),T

proof end;

theorem Th34: :: POLYRED:34

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds HM (p,T) <= p,T

proof end;

theorem Th35: :: POLYRED:35

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being non-zero Polynomial of n,L holds Red (p,T) < p,T

proof end;

begin

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f, p, g be Polynomial of n,L;
let b be bag of n;
pred f reduces_to g,p,b,T means :Def5: :: POLYRED:def 5
( f <> 0_ (n,L) & p <> 0_ (n,L) & b in Support f & ex s being bag of n st
( s + (HT (p,T)) = b & g = f - (((f . b) / (HC (p,T))) * (s *' p)) ) );

end;

:: deftheorem Def5 defines reduces_to POLYRED:def 5 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L
for b being bag of n holds
( f reduces_to g,p,b,T iff ( f <> 0_ (n,L) & p <> 0_ (n,L) & b in Support f & ex s being bag of n st
( s + (HT (p,T)) = b & g = f - (((f . b) / (HC (p,T))) * (s *' p)) ) ) );

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f, p, g be Polynomial of n,L;
pred f reduces_to g,p,T means :Def6: :: POLYRED:def 6
ex b being bag of n st f reduces_to g,p,b,T;

end;

:: deftheorem Def6 defines reduces_to POLYRED:def 6 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L holds
( f reduces_to g,p,T iff ex b being bag of n st f reduces_to g,p,b,T );

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f, g be Polynomial of n,L;
let P be Subset of (Polynom-Ring (n,L));
pred f reduces_to g,P,T means :Def7: :: POLYRED:def 7
ex p being Polynomial of n,L st
( p in P & f reduces_to g,p,T );

end;

:: deftheorem Def7 defines reduces_to POLYRED:def 7 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) holds
( f reduces_to g,P,T iff ex p being Polynomial of n,L st
( p in P & f reduces_to g,p,T ) );

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f, p be Polynomial of n,L;
pred f is_reducible_wrt p,T means :Def8: :: POLYRED:def 8
ex g being Polynomial of n,L st f reduces_to g,p,T;

end;

:: deftheorem Def8 defines is_reducible_wrt POLYRED:def 8 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p being Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex g being Polynomial of n,L st f reduces_to g,p,T );

notation

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f, p be Polynomial of n,L;
antonym f is_irreducible_wrt p,T for f is_reducible_wrt p,T;
antonym f is_in_normalform_wrt p,T for f is_reducible_wrt p,T;

end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f be Polynomial of n,L;
let P be Subset of (Polynom-Ring (n,L));
pred f is_reducible_wrt P,T means :: POLYRED:def 9
ex g being Polynomial of n,L st f reduces_to g,P,T;

end;

:: deftheorem defines is_reducible_wrt POLYRED:def 9 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) holds
( f is_reducible_wrt P,T iff ex g being Polynomial of n,L st f reduces_to g,P,T );

notation

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f be Polynomial of n,L;
let P be Subset of (Polynom-Ring (n,L));
antonym f is_irreducible_wrt P,T for f is_reducible_wrt P,T;
antonym f is_in_normalform_wrt P,T for f is_reducible_wrt P,T;

end;

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f, p, g be Polynomial of n,L;
pred f top_reduces_to g,p,T means :: POLYRED:def 10
f reduces_to g,p, HT (f,T),T;

end;

:: deftheorem defines top_reduces_to POLYRED:def 10 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L holds
( f top_reduces_to g,p,T iff f reduces_to g,p, HT (f,T),T );

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f, p be Polynomial of n,L;
pred f is_top_reducible_wrt p,T means :: POLYRED:def 11
ex g being Polynomial of n,L st f top_reduces_to g,p,T;

end;

:: deftheorem defines is_top_reducible_wrt POLYRED:def 11 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p being Polynomial of n,L holds
( f is_top_reducible_wrt p,T iff ex g being Polynomial of n,L st f top_reduces_to g,p,T );

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let f be Polynomial of n,L;
let P be Subset of (Polynom-Ring (n,L));
pred f is_top_reducible_wrt P,T means :: POLYRED:def 12
ex p being Polynomial of n,L st
( p in P & f is_top_reducible_wrt p,T );

end;

:: deftheorem defines is_top_reducible_wrt POLYRED:def 12 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) holds
( f is_top_reducible_wrt P,T iff ex p being Polynomial of n,L st
( p in P & f is_top_reducible_wrt p,T ) );

theorem :: POLYRED:36

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of n st
( b in Support f & HT (p,T) divides b ) )

proof end;

Lm17: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L
for b being bag of n st f reduces_to g,p,b,T holds
not b in Support g

proof end;

theorem Th37: :: POLYRED:37

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds 0_ (n,L) is_irreducible_wrt p,T

proof end;

theorem :: POLYRED:38

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, p being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to f - (m *' p),p,T holds
HT ((m *' p),T) in Support f

proof end;

theorem :: POLYRED:39

for n being Ordinal
for T being connected TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L
for b being bag of n st f reduces_to g,p,b,T holds
not b in Support g by Lm17;

theorem Th40: :: POLYRED:40

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L
for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
( b9 in Support g iff b9 in Support f )

proof end;

theorem Th41: :: POLYRED:41

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L
for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
f . b9 = g . b9

proof end;

theorem Th42: :: POLYRED:42

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of n st b in Support g holds
b <= HT (f,T),T

proof end;

theorem Th43: :: POLYRED:43

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
g < f,T

proof end;

begin

definition

let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ;
let P be Subset of (Polynom-Ring (n,L));
func PolyRedRel (P,T) -> Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) means :Def13: :: POLYRED:def 13
for p, q being Polynomial of n,L holds
( [p,q] in it iff p reduces_to q,P,T );
existence
ex b₁ being Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) st
for p, q being Polynomial of n,L holds
( [p,q] in b₁ iff p reduces_to q,P,T )

proof end;

uniqueness
for b₁, b₂ being Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) st ( for p, q being Polynomial of n,L holds
( [p,q] in b₁ iff p reduces_to q,P,T ) ) & ( for p, q being Polynomial of n,L holds
( [p,q] in b₂ iff p reduces_to q,P,T ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines PolyRedRel POLYRED:def 13 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for b₅ being Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) holds
( b₅ = PolyRedRel (P,T) iff for p, q being Polynomial of n,L holds
( [p,q] in b₅ iff p reduces_to q,P,T ) );

Lm18: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g, p being Polynomial of n,L st f reduces_to g,p,T holds
( f <> 0_ (n,L) & p <> 0_ (n,L) )

proof end;

theorem :: POLYRED:44

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
( g <= f,T & ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) )

proof end;

registration

let n be Nat;
let T be connected admissible TermOrder of n;
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let P be Subset of (Polynom-Ring (n,L));
cluster PolyRedRel (P,T) -> strongly-normalizing ;
coherence
PolyRedRel (P,T) is strongly-normalizing

proof end;

end;

theorem Th45: :: POLYRED:45

for n being Nat
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed left_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, h being Polynomial of n,L st f in P holds
PolyRedRel (P,T) reduces h *' f, 0_ (n,L)

proof end;

theorem Th46: :: POLYRED:46

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to g,P,T holds
m *' f reduces_to m *' g,P,T

proof end;

theorem Th47: :: POLYRED:47

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L
for m being Monomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces m *' f,m *' g

proof end;

theorem :: POLYRED:48

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f being Polynomial of n,L
for m being Monomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
PolyRedRel (P,T) reduces m *' f, 0_ (n,L)

proof end;

theorem Th49: :: POLYRED:49

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g, h, h1 being Polynomial of n,L st f - g = h & PolyRedRel (P,T) reduces h,h1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )

proof end;

theorem Th50: :: POLYRED:50

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convergent_wrt PolyRedRel (P,T)

proof end;

theorem Th51: :: POLYRED:51

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convertible_wrt PolyRedRel (P,T)

proof end;

definition

let R be non empty addLoopStr ;
let I be Subset of R;
let a, b be Element of R;
pred a,b are_congruent_mod I means :Def14: :: POLYRED:def 14
a - b in I;

end;

:: deftheorem Def14 defines are_congruent_mod POLYRED:def 14 :
for R being non empty addLoopStr
for I being Subset of R
for a, b being Element of R holds
( a,b are_congruent_mod I iff a - b in I );

theorem :: POLYRED:52

for R being non empty right_complementable right-distributive add-associative right_zeroed left_zeroed doubleLoopStr
for I being non empty right-ideal Subset of R
for a being Element of R holds a,a are_congruent_mod I

proof end;

theorem Th53: :: POLYRED:53

for R being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for I being non empty right-ideal Subset of R
for a, b being Element of R st a,b are_congruent_mod I holds
b,a are_congruent_mod I

proof end;

theorem Th54: :: POLYRED:54

for R being non empty right_complementable add-associative right_zeroed addLoopStr
for I being non empty add-closed Subset of R
for a, b, c being Element of R st a,b are_congruent_mod I & b,c are_congruent_mod I holds
a,c are_congruent_mod I

proof end;

theorem :: POLYRED:55

for R being non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for I being non empty add-closed Subset of R
for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds
a + c,b + d are_congruent_mod I

proof end;

theorem :: POLYRED:56

for R being non empty right_complementable commutative distributive add-associative right_zeroed doubleLoopStr
for I being non empty add-closed right-ideal Subset of R
for a, b, c, d being Element of R st a,b are_congruent_mod I & c,d are_congruent_mod I holds
a * c,b * d are_congruent_mod I

proof end;

Lm19: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f being non-zero Polynomial of n,L
for g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 & f reduces_to g,P,T holds
f9,g9 are_congruent_mod P -Ideal

proof end;

theorem Th57: :: POLYRED:57

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Element of (Polynom-Ring (n,L)) st f,g are_convertible_wrt PolyRedRel (P,T) holds
f,g are_congruent_mod P -Ideal

proof end;

Lm20: for n being Nat
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being non empty Subset of (Polynom-Ring (n,L))
for f, p, h being Element of (Polynom-Ring (n,L)) st p in P & p <> 0_ (n,L) & h <> 0_ (n,L) holds
f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)

proof end;

theorem :: POLYRED:58

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being non empty Subset of (Polynom-Ring (n,L))
for f, g being Element of (Polynom-Ring (n,L)) st f,g are_congruent_mod P -Ideal holds
f,g are_convertible_wrt PolyRedRel (P,T)

proof end;

theorem Th59: :: POLYRED:59

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
f - g in P -Ideal

proof end;

theorem :: POLYRED:60

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f being Polynomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f in P -Ideal

proof end;