:: Polynomial Reduction
::  by Christoph Schwarzweller
::
:: Received December 20, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ORDINAL1, ZFMISC_1, STRUCT_0, VALUED_0, POLYNOM7,
      SUBSET_1, RELAT_1, SUPINF_2, POLYNOM1, VECTSP_1, ORDERS_1, TARSKI,
      PRE_POLY, ARYTM_3, FUNCT_1, ALGSEQ_1, NAT_1, FINSET_1, CARD_1, XXREAL_0,
      XBOOLE_0, RLVECT_1, ALGSTR_0, FINSEQ_1, CARD_3, PARTFUN1, ORDINAL4,
      ARYTM_1, ALGSTR_1, LATTICES, VECTSP_2, BINOP_1, CAT_3, RELAT_2, BAGORDER,
      TERMORD, XCMPLX_0, BROUWER, ORDERS_2, WELLORD1, FINSUB_1, WAYBEL_4,
      MESFUNC1, REWRITE1, INT_1, IDEAL_1, POLYRED;
 notations CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, TARSKI, XBOOLE_0, SUBSET_1,
      ZFMISC_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FINSET_1, XXREAL_0, STRUCT_0, ALGSTR_0, ALGSTR_1, WAYBEL_0, FINSUB_1,
      WAYBEL_4, REWRITE1, RLVECT_1, FINSEQ_1, XTUPLE_0, MCART_1, ORDERS_1,
      VFUNCT_1, GROUP_1, VECTSP_2, VECTSP_1, POLYNOM7, WELLORD1, WELLFND1,
      IDEAL_1, ORDERS_2, POLYNOM1, BAGORDER, TERMORD, PRE_POLY;
 constructors REWRITE1, VECTSP_2, TRIANG_1, WAYBEL_4, WELLFND1, IDEAL_1,
      BAGORDER, TERMORD, DOMAIN_1, RELSET_1, BINOP_2, FVSUM_1, VFUNCT_1,
      XTUPLE_0;
 registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSET_1, FINSUB_1, XREAL_0, NAT_1,
      CARD_1, FINSEQ_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1,
      GCD_1, POLYNOM1, POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, BAGORDER,
      TERMORD, VALUED_0, ALGSTR_0, PRE_POLY, VFUNCT_1, FUNCT_2, FUNCT_1,
      RELSET_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE;


begin :: Preliminaries

registration
  let n be Ordinal, R be non trivial ZeroStr;
  cluster non-zero for Monomial of n,R;
end;

registration
  cluster non trivial for Field;
end;

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

begin :: More on Polynomials and Monomials

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

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

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

theorem :: POLYRED:4
  for n being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr, p be Series of n, L holds p - 0_(n
  ,L) = p;

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

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

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

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

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

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

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

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

begin :: Multiplication of polynomials with bags

definition
  let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be Series of n,L;
  func b *' p -> Series of n,L means
:: 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;
end;

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

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

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

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

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

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

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

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

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

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

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

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

begin :: Orders on Polynomials

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

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

definition :: according to p. 193
  let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q
  be Polynomial of n,L;
  pred p <= q,T means
:: POLYRED:def 2

  [Support p, Support q] in FinOrd RelStr(# Bags n, T#);
end;

definition
  let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q
  be Polynomial of n,L;
  pred p < q,T means
:: POLYRED:def 3

  p <= q,T & Support p <> Support q;
end;

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

theorem :: POLYRED:24  :: according to definition 5.15, p. 194
  for n being Ordinal, T being connected TermOrder of n, L being
non trivial ZeroStr, p being non-zero Polynomial of n,L holds PosetMax(Support(
  p,T)) = HT(p,T);

theorem :: POLYRED:25

:: theorem 5.12, p. 193
  for n being Ordinal, T being connected TermOrder of n, L being
  non empty addLoopStr, p being Polynomial of n,L holds p <= p,T;

theorem :: POLYRED:26

:: theorem 5.12, p. 193
  for n being Ordinal, T being connected TermOrder of n, L being
non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T & q <= p,T iff
  Support p = Support q;

theorem :: POLYRED:27

:: theorem 5.12, p. 193
  for n being Ordinal, T being connected TermOrder of n, L being
  non empty addLoopStr, p,q,r being Polynomial of n,L holds p <= q,T & q <= r,T
  implies p <= r,T;

theorem :: POLYRED:28
  for n being Ordinal, T being connected TermOrder of n, L being
  non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T or q <= p,T;

theorem :: POLYRED:29
  for n being Ordinal, T being connected TermOrder of n, L being
non empty addLoopStr, p,q being Polynomial of n,L holds p <= q,T iff not q < p,
  T;

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

theorem :: POLYRED:31

:: according to p. 193
  for n being Nat, T being admissible connected TermOrder of n, L
  being add-associative right_complementable right_zeroed well-unital
  distributive non trivial doubleLoopStr, P being non empty Subset of
  Polynom-Ring(n,L) holds 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;

theorem :: POLYRED:32
  for n being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed non trivial addLoopStr
, 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);

theorem :: POLYRED:33  :: exercise 5.16, p. 194
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed non trivial
  addLoopStr, p being non-zero Polynomial of n,L holds Red(p,T) < HM(p,T),T;

theorem :: POLYRED:34  :: exercise 5.16, p. 194
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed non trivial addLoopStr, p
  being Polynomial of n,L holds HM(p,T) <= p,T;

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

begin :: Polynomial Reduction

definition :: definition 5.18 (i), p. 195
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be
  Polynomial of n,L, b be bag of n;
  pred f reduces_to g,p,b,T means
:: 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;

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

  ex b being bag of n st f reduces_to g,p ,b,T;
end;

definition :: definition 5.18 (iii), p. 196
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, f,g be
  Polynomial of n,L, P be Subset of Polynom-Ring(n,L);
  pred f reduces_to g,P,T means
:: POLYRED:def 7

  ex p being Polynomial of n,L st p in P & f reduces_to g,p,T;
end;

definition :: definition 5.18 (iv), p. 196
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, f,p be
  Polynomial of n,L;
  pred f is_reducible_wrt p,T means
:: POLYRED:def 8

  ex g being Polynomial of n,L st f reduces_to g,p,T;
end;

notation :: definition 5.18 (iv), p. 196
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, 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 :: definition 5.18 (v), p. 196
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, f be
  Polynomial of n,L, 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;

notation :: definition 5.18 (v), p. 196
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, f be
  Polynomial of n,L, 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 :: following definition 5.18, p. 196
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, 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;

definition :: following definition 5.18, p. 196
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, 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;

definition :: following definition 5.18, p. 196
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
  distributive almost_left_invertible non trivial doubleLoopStr, f be
  Polynomial of n,L, 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;

theorem :: POLYRED:36 :: lemma 5.20 (i), p. 197
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, f
  being Polynomial of n,L, 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;

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

theorem :: POLYRED:38 :: lemma 5.20 (ii), p. 197
  for n being Ordinal, T being admissible connected TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non degenerated non
empty doubleLoopStr, f,p being Polynomial of n,L, m being non-zero Monomial of
  n,L holds f reduces_to f-m*'p,p,T implies HT(m*'p,T) in Support f;

theorem :: POLYRED:39 :: lemma 5.20 (iii), p. 197
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive almost_left_invertible non degenerated non empty
  doubleLoopStr, f,p,g being Polynomial of n,L, b being bag of n holds f
  reduces_to g,p,b,T implies not(b in Support g);

theorem :: POLYRED:40  :: lemma 5.20 (iii), p. 197
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, f,p,g being Polynomial of n,L, b,b9 being bag of n st b < b9,T
  holds f reduces_to g,p,b,T implies (b9 in Support g iff b9 in Support f);

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

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

theorem :: POLYRED:43  :: lemma 5.20 (iv), p. 197
  for n being Ordinal, T being connected admissible TermOrder of n
, L being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, f,p,g being Polynomial of n,L holds f reduces_to g,p,
  T implies g < f,T;

begin :: Polynomial Reduction Relation

definition
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_complementable right_zeroed commutative associative well-unital
distributive almost_left_invertible non trivial doubleLoopStr, 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
:: POLYRED:def 13

  for p,q being Polynomial of n,L holds [p,q] in it iff p reduces_to q,P,T;
end;

theorem :: POLYRED:44 :: lemma 5.20 (v), p. 197
  for n being Ordinal, T being connected admissible TermOrder of n, L
  being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, f,g being Polynomial of n,L, P being Subset of
Polynom-Ring(n,L) holds PolyRedRel(P,T) reduces f,g implies g <= f,T & (g = 0_(
  n,L) or HT(g,T) <= HT(f,T),T);

registration :: theorem 5.21, p. 198
  let n be Nat, T be connected admissible TermOrder of n, L be Abelian
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive almost_left_invertible non degenerated non empty
  doubleLoopStr, P be Subset of Polynom-Ring(n,L);
  cluster PolyRedRel(P,T) -> strongly-normalizing;
end;

theorem :: POLYRED:45  :: lemma 5.24 (i), p. 200
  for n being Nat, T being admissible connected TermOrder of n, L
being add-associative right_complementable left_zeroed right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
  trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,h being
  Polynomial of n,L holds f in P implies PolyRedRel(P,T) reduces h*'f,0_(n,L);

theorem :: POLYRED:46  :: lemma 5.24 (ii), p. 200
  for n being Ordinal, T being connected admissible TermOrder of n
, L being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being
  Polynomial of n,L, m being non-zero Monomial of n,L holds f reduces_to g,P,T
  implies m*'f reduces_to m*'g,P,T;

theorem :: POLYRED:47  :: lemma 5.24 (iii), p. 200
  for n being Ordinal, T being connected admissible TermOrder of n
, L being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being
  Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,g
  implies PolyRedRel(P,T) reduces m*'f,m*'g;

theorem :: POLYRED:48 :: lemma 5.24 (iii), p. 200
  for n being Ordinal, T being connected admissible TermOrder of n, L
  being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f being
Polynomial of n,L, m being Monomial of n,L holds PolyRedRel(P,T) reduces f,0_(n
  ,L) implies PolyRedRel(P,T) reduces m*'f,0_(n,L);

theorem :: POLYRED:49  :: lemma 5.25 (i), p. 200
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g,h,h1 being Polynomial
of n,L holds (f - g = h & PolyRedRel(P,T) reduces h,h1) implies ex f1,g1 being
Polynomial of n,L st f1 - g1 = h1 & PolyRedRel(P,T) reduces f,f1 & PolyRedRel(P
  ,T) reduces g,g1;

theorem :: POLYRED:50  :: lemma 5.25 (ii), p. 200
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,
  L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convergent_wrt
  PolyRedRel(P,T);

theorem :: POLYRED:51  :: lemma 5.25 (ii), p. 200
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,
  L holds PolyRedRel(P,T) reduces f-g,0_(n,L) implies f,g are_convertible_wrt
  PolyRedRel(P,T);

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

  a - b in I;
end;

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

theorem :: POLYRED:53
  for R being add-associative right_zeroed right_complementable
well-unital right-distributive non empty doubleLoopStr, I being right-ideal
  non empty Subset of R, a,b being Element of R holds a,b are_congruent_mod I
  implies b,a are_congruent_mod I;

theorem :: POLYRED:54
  for R being add-associative right_zeroed right_complementable
non empty addLoopStr, I being add-closed non empty Subset of R, a,b,c being
Element of R holds a,b are_congruent_mod I & b,c are_congruent_mod I implies a,
  c are_congruent_mod I;

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

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

theorem :: POLYRED:57  :: lemma 5.26, p. 202
  for n being Ordinal, T being connected TermOrder of n, L being
  Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non trivial
  doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Element of
  Polynom-Ring(n,L) holds f,g are_convertible_wrt PolyRedRel(P,T) implies f,g
  are_congruent_mod P-Ideal;

theorem :: POLYRED:58 :: lemma 5.26, p. 202
  for n being Nat, T being admissible connected TermOrder of n, L being
  Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, P being non empty Subset of Polynom-Ring(n,L), f,g
being Element of Polynom-Ring(n,L) holds f,g are_congruent_mod P-Ideal implies
  f,g are_convertible_wrt PolyRedRel(P,T);

theorem :: POLYRED:59  :: lemma 5.26, p. 202
  for n being Ordinal, T being connected TermOrder of n, L being
  Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being Polynomial of n,
  L holds PolyRedRel(P,T) reduces f,g implies f-g in P-Ideal;

theorem :: POLYRED:60 :: lemma 5.26, p. 202
  for n being Ordinal, T being connected TermOrder of n, L being Abelian
  add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, P
being Subset of Polynom-Ring(n,L), f being Polynomial of n,L holds PolyRedRel(P
  ,T) reduces f,0_(n,L) implies f in P-Ideal;