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


begin

registration
let n be Ordinal;
let R be non trivial ZeroStr ;
cluster non zero Relation-like Bags n -defined the carrier of R -valued Function-like total V46( Bags n, the carrier of R) non-zero monomial-like finite-Support for Element of bool [:(Bags n), the carrier of R:];
existence
 ex b1 being Monomial of n,R st b1 is non-zero
proofend;
end;

registration
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable almost_left_invertible V102() 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 for doubleLoopStr ;
existence
 not for b1 being Field holds b1 is trivial
proofend;
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
proofend;

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

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

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

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 &amp; ( for b9 being bag of n st b < b9 holds
p . b9 = 0. L ) )
proofend;

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 &amp; g = f | (Seg n) holds
Sum f = (Sum g) + (f /. (len f))
proofend;

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;
clusterp *' q ->  non-zero ;
coherence
 p *' q is non-zero
proofend;
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)
proofend;

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
proofend;

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) &amp; p + (- p) = 0_ (X,L) )
proofend;

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
proofend;

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)
proofend;

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
proofend;

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 &amp; - (p *' q) = p *' (- q) )
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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 &amp; - (a * p) = a * (- p) )
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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;
funcb *' 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) &amp; ( for b9 being bag of n st not b divides b9 holds
it . b9 = 0. L ) );
existence
 ex b1 being Series of n,L st
for b9 being bag of n st b divides b9 holds
( b1 . b9 = p . (b9 -' b) &amp; ( for b9 being bag of n st not b divides b9 holds
b1 . b9 = 0. L ) )
proofend;
uniqueness
 for b1, b2 being Series of n,L st ( for b9 being bag of n st b divides b9 holds
( b1 . b9 = p . (b9 -' b) &amp; ( for b9 being bag of n st not b divides b9 holds
b1 . b9 = 0. L ) ) ) &amp; ( for b9 being bag of n st b divides b9 holds
( b2 . b9 = p . (b9 -' b) &amp; ( for b9 being bag of n st not b divides b9 holds
b2 . b9 = 0. L ) ) ) holds
b1 = b2
proofend;
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, b5 being Series of n,L holds
( b5 = b *' p iff for b9 being bag of n st b divides b9 holds
( b5 . b9 = p . (b9 -' b) &amp; ( for b9 being bag of n st not b divides b9 holds
b5 . 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
proofend;

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  }
proofend;

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;
clusterb *' p ->  finite-Support ;
coherence
 b *' p is finite-Support
proofend;
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))
proofend;

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
proofend;

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
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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
proofend;
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
proofend;
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 #)
proofend;

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;
predp <= 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;
predp < q,T means :Def3: :: POLYRED:def 3
( p <= q,T &amp; 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 &amp; 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)
proofend;

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
proofend;

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
proofend;

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 &amp; q <= p,T ) iff Support p = Support q )
proofend;

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 &amp; q <= r,T holds
p <= r,T
proofend;

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 )
proofend;

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 )
proofend;

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 &amp; b <> HT (p,T) holds
p . b = 0. L
proofend;

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)
proofend;

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) &amp; q <> 0_ (n,L) ) or HT (p,T) < HT (q,T),T or ( HT (p,T) = HT (q,T) &amp; Red (p,T) < Red (q,T),T ) ) )
proofend;

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) &amp; HT (p,T) = HT (q,T) &amp; Red (p,T) <= Red (q,T),T holds
p <= q,T
proofend;

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 &amp; ( for q being Polynomial of n,L st q in P holds
p <= q,T ) )
proofend;

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) &amp; q <> 0_ (n,L) ) or HT (p,T) < HT (q,T),T or ( HT (p,T) = HT (q,T) &amp; 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
proofend;

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
proofend;

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
proofend;

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;
predf reduces_to g,p,b,T means :Def5: :: POLYRED:def 5
( f <> 0_ (n,L) &amp; p <> 0_ (n,L) &amp; b in Support f &amp; ex s being bag of n st
( s + (HT (p,T)) = b &amp; 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) &amp; p <> 0_ (n,L) &amp; b in Support f &amp; ex s being bag of n st
( s + (HT (p,T)) = b &amp; 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;
predf 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));
predf reduces_to g,P,T means :Def7: :: POLYRED:def 7
 ex p being Polynomial of n,L st
( p in P &amp; 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 &amp; 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;
predf 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));
predf 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;
predf 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;
predf 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));
predf is_top_reducible_wrt P,T means :: POLYRED:def 12
 ex p being Polynomial of n,L st
( p in P &amp; 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 &amp; 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 &amp; HT (p,T) divides b ) )
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; f reduces_to g,p,b,T holds
( b9 in Support g iff b9 in Support f )
proofend;

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 &amp; f reduces_to g,p,b,T holds
f . b9 = g . b9
proofend;

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
proofend;

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
proofend;

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 b1 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 b1 iff p reduces_to q,P,T )
proofend;
uniqueness
 for b1, b2 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 b1 iff p reduces_to q,P,T ) ) &amp; ( for p, q being Polynomial of n,L holds
( [p,q] in b2 iff p reduces_to q,P,T ) ) holds
b1 = b2
proofend;
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 b5 being Relation of (NonZero (Polynom-Ring (n,L))), the carrier of (Polynom-Ring (n,L)) holds
( b5 = PolyRedRel (P,T) iff for p, q being Polynomial of n,L holds
( [p,q] in b5 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) &amp; p <> 0_ (n,L) )
proofend;

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 &amp; ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) )
proofend;

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
proofend;
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)
proofend;

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
proofend;

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
proofend;

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)
proofend;

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 &amp; PolyRedRel (P,T) reduces h,h1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 &amp; PolyRedRel (P,T) reduces f,f1 &amp; PolyRedRel (P,T) reduces g,g1 )
proofend;

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)
proofend;

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)
proofend;

definition
let R be non empty addLoopStr ;
let I be Subset of R;
let a, b be Element of R;
preda,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
proofend;

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
proofend;

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 &amp; b,c are_congruent_mod I holds
a,c are_congruent_mod I
proofend;

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 &amp; c,d are_congruent_mod I holds
a + c,b + d are_congruent_mod I
proofend;

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 &amp; c,d are_congruent_mod I holds
a * c,b * d are_congruent_mod I
proofend;

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 &amp; g = g9 &amp; f reduces_to g,P,T holds
f9,g9 are_congruent_mod P -Ideal
proofend;

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
proofend;

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 &amp; p <> 0_ (n,L) &amp; h <> 0_ (n,L) holds
f,f + (h * p) are_convertible_wrt PolyRedRel (P,T)
proofend;

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)
proofend;

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
proofend;

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
proofend;