The abstract of the Mizar article:

Polynomial Reduction

by

Christoph Schwarzweller

Received December 20, 2002

MML identifier: POLYRED

[ Mizar article, MML identifier index ]

environ

 vocabulary POLYNOM1, POLYNOM7, BOOLE, FUNCT_1, RELAT_1, VECTSP_1, RLVECT_1,
      ORDINAL1, LATTICES, ANPROJ_1, VECTSP_2, ALGSTR_1, ARYTM_1, REALSET1,
      CAT_3, GROUP_1, BINOP_1, ARYTM_3, TERMORD, FINSEQ_4, WELLORD1, IDEAL_1,
      TARSKI, ORDERS_1, ORDERS_2, RELAT_2, DICKSON, BAGORDER, FINSUB_1,
      TRIANG_1, MCART_1, REWRITE1, INT_1, FINSEQ_1, WAYBEL_4, FINSET_1,
      ALGSTR_2, ALGSEQ_1, CARD_1, POLYRED;
 notation NUMBERS, XCMPLX_0, XREAL_0, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0,
      ZFMISC_1, RELAT_1, RELAT_2, MONOID_0, RELSET_1, FUNCT_1, FUNCT_2,
      ORDINAL1, NAT_1, ALGSTR_1, WAYBEL_0, FINSUB_1, FINSET_1, WAYBEL_4,
      REWRITE1, RLVECT_1, CARD_1, FINSEQ_1, FINSEQ_4, MCART_1, TRIANG_1,
      REALSET1, VECTSP_2, VECTSP_1, POLYNOM7, WELLORD1, WELLFND1, IDEAL_1,
      ORDERS_1, ORDERS_2, POLYNOM1, BAGORDER, TERMORD;
 constructors ORDERS_2, WAYBEL_4, MONOID_0, REWRITE1, TRIANG_1, IDEAL_1,
      TERMORD, WELLFND1, DOMAIN_1, MEMBERED, BAGORDER;
 clusters STRUCT_0, RELAT_1, FINSET_1, RELSET_1, VECTSP_1, FINSEQ_1, VECTSP_2,
      CARD_1, GCD_1, ALGSTR_1, POLYNOM1, POLYNOM2, REWRITE1, BINOM, FINSUB_1,
      ORDERS_1, POLYNOM7, BAGORDER, TERMORD, SUBSET_1, IDEAL_1, MONOID_0,
      NAT_1, XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, BOOLE;


begin :: Preliminaries

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

definition
cluster non trivial Field;
end;

definition
cluster Field-like -> domRing-like
           (left_zeroed add-right-cancelable right-distributive
            left_unital commutative associative (non empty doubleLoopStr));
end;

definition
let n be Ordinal,
    L be add-associative right_complementable left_zeroed right_zeroed
            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 LoopStr),
    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 LoopStr),
    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 LoopStr),
    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 LoopStr),
    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
            add-left-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
            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 add-left-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,a' being Element of L
holds a * p + a' * p = (a + a') * p;

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

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

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 b' being bag of n st b divides b' holds it.b' = p.(b' -' b) &
  for b' being bag of n st not(b divides b') holds it.b' = 0.L;
end;

definition
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,b' being bag of n,
    L being non empty ZeroStr,
    p being Series of n,L
holds (b*'p).(b'+b) = p.b';

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 + b' where b' is Element of Bags n : b' 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,b' being bag of n
holds b' in Support(b*'p) implies b' <= 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
            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

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

definition
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 LoopStr,
    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 LoopStr,
    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 LoopStr,
    p,q,r being Polynomial of n,L
holds (p <= q,T & q <= r,T) implies p <= r,T;

theorem :: POLYRED:28
::: theorem 5.12, p. 193
for n being Ordinal,
    T being connected TermOrder of n,
    L being non empty LoopStr,
    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 LoopStr,
    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
for n being Nat,
    T being admissible connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            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
::: according to p. 193
  for n being Ordinal,
    T being connected admissible TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    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 LoopStr),
    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 LoopStr),
    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 LoopStr),
    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
         Field-like (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
         Field-like (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
         Field-like (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
         Field-like (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;
antonym f is_irreducible_wrt p,T;
antonym f is_in_normalform_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
         Field-like (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;
antonym f is_irreducible_wrt P,T;
antonym f is_in_normalform_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
         Field-like (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
         Field-like (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
         Field-like (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
            Field-like (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
            Field-like (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 Field-like 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
            Field-like 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
            Field-like (non trivial doubleLoopStr),
    f,p,g being Polynomial of n,L,
    b,b' being bag of n st b < b',T
holds f reduces_to g,p,b,T implies
      (b' in Support g iff b' 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
            Field-like (non trivial doubleLoopStr),
    f,p,g being Polynomial of n,L,
    b,b' being bag of n st b < b',T
holds f reduces_to g,p,b,T implies f.b' = g.b';

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
            Field-like 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
            Field-like 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
         Field-like (non trivial doubleLoopStr),
    P be Subset of Polynom-Ring(n,L);
func PolyRedRel(P,T) ->
        Relation of (the carrier of Polynom-Ring(n,L)) \ {0_(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
            Field-like 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);

definition
::: 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
         Field-like 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
            Field-like (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
            Field-like 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
            Field-like 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
            Field-like 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 Field-like (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 Field-like (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 Field-like (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 LoopStr,
    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 right_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 LoopStr),
    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 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
            Field-like (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
            Field-like 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
            Field-like (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
            Field-like (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;