:: Construction of {G}r\"obner Bases: Avoiding S-Polynomials -- Buchberger's
:: First Criterium
::  by Christoph Schwarzweller
::
:: Received December 10, 2004
:: Copyright (c) 2004-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, PRE_POLY, ARYTM_3, ARYTM_1, ORDINAL1, BAGORDER,
      XXREAL_0, RLVECT_1, ALGSTR_0, VECTSP_1, LATTICES, VECTSP_2, ZFMISC_1,
      VALUED_0, POLYNOM7, CAT_3, RELAT_2, POLYNOM1, BROUWER, SUPINF_2,
      XCMPLX_0, SUBSET_1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, ALGSTR_1, CARD_1,
      FUNCT_7, TERMORD, BINOP_1, POLYRED, REWRITE1, FINSEQ_1, STRUCT_0,
      FINSET_1, FUNCT_4, FUNCOP_1, ALGSEQ_1, ORDERS_2, WAYBEL_4, RUSUB_4,
      GROEB_2, MESFUNC1, GROEB_1, GROEB_3, NAT_1;
 notations TARSKI, SUBSET_1, RELAT_1, XBOOLE_0, RELAT_2, CARD_1, ORDINAL1,
      NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_4,
      FUNCOP_1, PRE_POLY, STRUCT_0, ALGSTR_0, GROUP_1, ALGSTR_1, RLVECT_1,
      VFUNCT_1, FINSET_1, XTUPLE_0, MCART_1, FINSEQ_1, VECTSP_2, VECTSP_1,
      POLYNOM7, ORDERS_2, FUNCT_7, REWRITE1, BAGORDER, TERMORD, GROEB_1,
      POLYRED, GROEB_2, WAYBEL_4, POLYNOM1;
 constructors XXREAL_0, REWRITE1, VECTSP_2, WAYBEL_4, POLYNOM2, BAGORDER,
      TERMORD, POLYRED, GROEB_1, GROEB_2, RELSET_1, PBOOLE, FUNCT_7, VFUNCT_1,
      XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, NAT_1,
      INT_1, CARD_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1,
      POLYNOM1, POLYNOM2, POLYNOM4, POLYNOM7, TERMORD, POLYRED, ORDINAL1,
      VALUED_0, ALGSTR_0, PRE_POLY, VFUNCT_1, FUNCT_2, RELSET_1, FUNCT_4;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

theorem :: GROEB_3:1
  for X being set, b1,b2 being bag of X holds (b1 + b2) / b2 = b1;

theorem :: GROEB_3:2
  for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3
  being bag of n holds b1 <= b2,T implies b1 + b3 <= b2 + b3,T;

theorem :: GROEB_3:3
  for n being Ordinal, T being TermOrder of n, b1,b2,b3 being bag
  of n holds b1 <= b2,T & b2 < b3,T implies b1 < b3,T;

theorem :: GROEB_3:4
  for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3
  being bag of n holds b1 < b2,T implies b1 + b3 < b2 + b3,T;

theorem :: GROEB_3:5
  for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3,
  b4 being bag of n holds b1 < b2,T & b3 <= b4,T implies b1 + b3 < b2 + b4,T;

theorem :: GROEB_3:6
  for n being Ordinal, T being admissible TermOrder of n, b1,b2,b3,
  b4 being bag of n holds b1 <= b2,T & b3 < b4,T implies b1 + b3 < b2 + b4,T;

begin :: More on Polynomials

theorem :: GROEB_3:7
  for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
  m1,m2 being non-zero Monomial of n,L holds term(m1*'m2) = term(m1) + term(m2)
;

theorem :: GROEB_3:8
  for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
  p being Polynomial of n,L, m being non-zero Monomial of n,L, b being bag of n
  holds b in Support(p) iff term(m) + b in Support(m*'p);

theorem :: GROEB_3:9
  for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
p being Polynomial of n,L, m being non-zero Monomial of n,L holds Support(m*'p)
  = { term(m) + b where b is Element of Bags n : b in Support p };

theorem :: GROEB_3:10
  for n being Ordinal, L being add-associative
  right_complementable left_zeroed right_zeroed well-unital distributive
  domRing-like non trivial doubleLoopStr, p being Polynomial of n,L, m being
  non-zero Monomial of n,L holds card Support(p) = card Support(m*'p);

theorem :: GROEB_3:11
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed non trivial addLoopStr
  holds Red(0_(n,L),T) = 0_(n,L);

theorem :: GROEB_3:12
  for n being Ordinal, L being Abelian add-associative
  right_zeroed right_complementable commutative well-unital distributive non
  trivial doubleLoopStr, p,q being Polynomial of n,L holds p - q = 0_(n,L)
  implies p = q;

theorem :: GROEB_3:13
  for X being set, L being add-associative right_zeroed
  right_complementable non empty addLoopStr holds -(0_(X,L)) = 0_(X,L);

theorem :: GROEB_3:14
  for X being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr, f being Series of X,L holds 0_(X,L
  ) - f = -f;

theorem :: GROEB_3:15
  for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial doubleLoopStr,
  p being Polynomial of n,L holds p - Red(p,T) = HM(p,T);

registration
  let n be Ordinal, L be add-associative right_complementable right_zeroed
  non empty addLoopStr, p be Polynomial of n,L;
  cluster Support p -> finite;
end;

definition
  let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n,L;
  redefine func {p,q} -> Subset of Polynom-Ring(n,L);
end;

begin :: Restriction and Splitting of Polynomials

definition
  let X be set, L be non empty ZeroStr, s be Series of X,L, Y be Subset of
  Bags X;
  func s|Y -> Series of X,L equals
:: GROEB_3:def 1
  s +* ((Support s \ Y) --> 0.L);
end;

registration
  let n be Ordinal, L be non empty ZeroStr, p be Polynomial of n,L, Y be
  Subset of Bags n;
  cluster p|Y -> finite-Support;
end;

theorem :: GROEB_3:16
  for X being set, L being non empty ZeroStr, s being Series of X,
L, Y being Subset of Bags X holds Support s|Y = (Support s) /\ Y & for b being
  bag of X st b in Support s|Y holds (s|Y).b = s.b;

theorem :: GROEB_3:17
  for X being set, L being non empty ZeroStr, s being Series of X,L, Y
  being Subset of Bags X holds Support(s|Y) c= Support s;

theorem :: GROEB_3:18
  for X being set, L being non empty ZeroStr, s being Series of X,L
  holds s|(Support s) = s & s|({} Bags X) = 0_(X,L);

definition
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
  L, i be Nat such that
 i <= card(Support p);
  func Upper_Support(p,T,i) -> finite Subset of Bags n means
:: GROEB_3:def 2

  it c=
Support p & card it = i & for b,b9 being bag of n st b in it & b9 in Support p
  & b <= b9,T holds b9 in it;
end;

definition
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
  L, i be Nat;
  func Lower_Support(p,T,i) -> finite Subset of Bags n equals
:: GROEB_3:def 3
  Support(p) \ Upper_Support(p,T,i);
end;

theorem :: GROEB_3:19
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
  being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Upper_Support(p,T,i) \/ Lower_Support(p,T,i) = Support p & Upper_Support(p,T,i)
  /\ Lower_Support(p,T,i) = {};

theorem :: GROEB_3:20
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b,
  b9 being bag of n st b in Upper_Support(p,T,i) & b9 in Lower_Support(p,T,i)
  holds b9 < b,T;

theorem :: GROEB_3:21
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L holds Upper_Support(p,T,0) = {} & Lower_Support(p,T,0)
  = Support p;

theorem :: GROEB_3:22
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L holds Upper_Support(p,T,card(Support p)) = Support p &
  Lower_Support(p,T,card(Support p)) = {};

theorem :: GROEB_3:23
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non trivial addLoopStr, p
being non-zero Polynomial of n,L, i being Element of NAT st 1 <= i & i <= card(
  Support p) holds HT(p,T) in Upper_Support(p,T,i);

theorem :: GROEB_3:24
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
  being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Lower_Support(p,T,i) c= Support p & card Lower_Support(p,T,i) = card(Support p)
- i & for b,b9 being bag of n st b in Lower_Support(p,T,i) & b9 in Support p &
  b9 <= b,T holds b9 in Lower_Support(p,T,i);

definition
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n,
  L, i be Nat;
  func Up(p,T,i) -> Polynomial of n,L equals
:: GROEB_3:def 4
  p|(Upper_Support(p,T,i));
  func Low(p,T,i) -> Polynomial of n,L equals
:: GROEB_3:def 5
  p|(Lower_Support(p,T,i));
end;

theorem :: GROEB_3:25
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
  being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
Support Up(p,T,i) = Upper_Support(p,T,i) & Support Low(p,T,i) = Lower_Support(p
  ,T,i);

theorem :: GROEB_3:26
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
  being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
  Support(Up(p,T,i)) c= Support(p) & Support(Low(p,T,i)) c= Support(p);

theorem :: GROEB_3:27
  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, i being Element of NAT st 1 <= i & i <= card(Support p
  ) holds Support(Low(p,T,i)) c= Support(Red(p,T));

theorem :: GROEB_3:28
  for n be Ordinal, T be connected TermOrder of n, L be
add-associative right_zeroed right_complementable non empty addLoopStr, p be
Polynomial of n,L, i be Element of NAT st i <= card(Support p) for b being bag
of n st b in Support p holds (b in Support Up(p,T,i) or b in Support Low(p,T,i)
  ) & not(b in Support Up(p,T,i) /\ Support Low(p,T,i));

theorem :: GROEB_3:29
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b,
b9 being bag of n st b in Support Low(p,T,i) & b9 in Support Up(p,T,i) holds b
  < b9,T;

theorem :: GROEB_3:30
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st 1 <= i & i <= card(Support p
  ) holds HT(p,T) in Support Up(p,T,i);

theorem :: GROEB_3:31
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
  being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b
being bag of n st b in Support Low(p,T,i) holds Low(p,T,i).b = p.b & Up(p,T,i).
  b = 0.L;

theorem :: GROEB_3:32
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
  being Polynomial of n,L, i being Element of NAT st i <= card(Support p) for b
being bag of n st b in Support Up(p,T,i) holds Up(p,T,i).b = p.b & Low(p,T,i).b
  = 0.L;

theorem :: GROEB_3:33
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
  being Polynomial of n,L, i being Element of NAT st i <= card(Support p) holds
  Up(p,T,i) + Low(p,T,i) = p;

theorem :: GROEB_3:34
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
  being Polynomial of n,L holds Up(p,T,0) = 0_(n,L) & Low(p,T,0) = p;

theorem :: GROEB_3:35
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable Abelian non empty
  doubleLoopStr, p being Polynomial of n,L holds Up(p,T,card(Support p)) = p &
  Low(p,T,card(Support p)) = 0_(n,L);

theorem :: GROEB_3:36
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable Abelian non trivial
doubleLoopStr, p being non-zero Polynomial of n,L holds Up(p,T,1) = HM(p,T) &
  Low(p,T,1) = Red(p,T);

registration
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_zeroed right_complementable non trivial addLoopStr, p be non-zero
  Polynomial of n,L;
  cluster Up(p,T,0) -> monomial-like;
end;

registration
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
  right_zeroed right_complementable Abelian non trivial doubleLoopStr, p be
  non-zero Polynomial of n,L;
  cluster Up(p,T,1) -> non-zero monomial-like;
  cluster Low(p,T,card(Support p)) -> monomial-like;
end;

theorem :: GROEB_3:37
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non trivial addLoopStr, p
  being Polynomial of n,L, j being Element of NAT st j = card(Support p) - 1
  holds Low(p,T,j) is non-zero Monomial of n,L;

theorem :: GROEB_3:38
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_zeroed right_complementable non empty
  addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
  Support p) holds HT(Low(p,T,i+1),T) <= HT(Low(p,T,i),T), T;

theorem :: GROEB_3:39
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable non empty addLoopStr, p
being Polynomial of n,L, i being Element of NAT st 0 < i & i < card(Support p)
  holds HT(Low(p,T,i),T) < HT(p,T),T;

theorem :: GROEB_3:40
  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 Polynomial of n,
  L, m being non-zero Monomial of n,L, i being Element of NAT st i <= card(
Support p) for b being bag of n holds term(m) + b in Support Low(m*'p,T,i) iff
  b in Support Low(p,T,i);

theorem :: GROEB_3:41
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_zeroed right_complementable non empty
  addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
  Support p) holds Support Low(p,T,i+1) c= Support Low(p,T,i);

theorem :: GROEB_3:42
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_zeroed right_complementable non empty
  addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
Support p) holds Support Low(p,T,i) \ Support Low(p,T,i+1) = {HT(Low(p,T,i),T)}
;

theorem :: GROEB_3:43
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_zeroed right_complementable non trivial
  addLoopStr, p being Polynomial of n,L, i being Element of NAT st i < card(
  Support p) holds Low(p,T,i+1) = Red(Low(p,T,i),T);

theorem :: GROEB_3:44
  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 Polynomial of n,
  L, m being non-zero Monomial of n,L, i being Element of NAT st i <= card(
  Support p) holds Low(m*'p,T,i) = m *' Low(p,T,i);

begin

theorem :: GROEB_3:45
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
  trivial doubleLoopStr, f,g,p being Polynomial of n,L st f reduces_to g,p,T
  holds -f reduces_to -g,p,T;

theorem :: GROEB_3:46
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, f,f1,g,p being Polynomial of n,L st f reduces_to f1,{p}
  ,T & for b1 being bag of n st b1 in Support g holds not(HT(p,T) divides b1)
  holds f + g reduces_to f1 + g,{p},T;

theorem :: GROEB_3:47
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
  trivial doubleLoopStr, f,g being non-zero Polynomial of n,L holds f*'g
  reduces_to Red(f,T)*'g,{g},T;

theorem :: GROEB_3:48
  for n being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,g being non-zero Polynomial of n,L, p being Polynomial of n,L
  st p.(HT(f*'g,T)) = 0.L holds f*'g+p reduces_to Red(f,T)*'g+p,{g},T;

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

theorem :: GROEB_3:50
  for n being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, f,f1,g,p being Polynomial of n,L st PolyRedRel({p},T) reduces f
  ,f1 & for b1 being bag of n st b1 in Support g holds not(HT(p,T) divides b1)
  holds PolyRedRel({p},T) reduces f+g,f1+g;

theorem :: GROEB_3:51
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, f,g being non-zero Polynomial of n,L holds PolyRedRel({
  g},T) reduces f*'g,0_(n,L);

begin :: The Criterium

theorem :: GROEB_3:52
  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, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint
  for b1,b2 being bag of n st b1 in Support Red(p1,T) & b2 in Support Red(p2,T)
  holds not(HT(p1,T) + b2 = HT(p2,T) + b1);

theorem :: GROEB_3:53
  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, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint
  holds S-Poly(p1,p2,T) = HM(p2,T) *' Red(p1,T) - HM(p1,T) *' Red(p2,T);

theorem :: GROEB_3:54
  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, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T) are_disjoint
  holds S-Poly(p1,p2,T) = Red(p1,T) *' p2 - Red(p2,T) *' p1;

theorem :: GROEB_3:55
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
trivial doubleLoopStr, p1,p2 being non-zero Polynomial of n,L st HT(p1,T),HT(
  p2,T) are_disjoint & Red(p1,T) is non-zero & Red(p2,T) is non-zero holds
PolyRedRel({p1},T) reduces HM(p2,T)*'Red(p1,T) - HM(p1,T)*'Red(p2,T), p2 *' Red
  (p1,T);

theorem :: GROEB_3:56
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
  trivial doubleLoopStr, p1,p2 being Polynomial of n,L st HT(p1,T),HT(p2,T)
  are_disjoint holds PolyRedRel({p1,p2},T) reduces S-Poly(p1,p2,T),0_(n,L);

:: theorem 5.66, p. 222 (Buchberger's first criterium)

theorem :: GROEB_3:57
  for n being Element of NAT, T being connected admissible 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, G being Subset of Polynom-Ring(n,L)
  holds G is_Groebner_basis_wrt T implies (for g1,g2 being Polynomial of n,L st
  g1 in G & g2 in G & not(HT(g1,T),HT(g2,T) are_disjoint) holds PolyRedRel(G,T)
  reduces S-Poly(g1,g2,T),0_(n,L));

:: theorem 5.68 (i) ==> (ii), p. 223

theorem :: GROEB_3:58
  for n being Element of NAT, T being connected admissible TermOrder of
  n, L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
degenerated non trivial doubleLoopStr, G being Subset of Polynom-Ring(n,L) st
not(0_(n,L) in G) holds (for g1,g2 being Polynomial of n,L st g1 in G & g2 in G
& not(HT(g1,T),HT(g2,T) are_disjoint) holds PolyRedRel(G,T) reduces S-Poly(g1,
g2,T),0_(n,L)) implies (for g1,g2,h being Polynomial of n,L st g1 in G & g2 in
G & not(HT(g1,T),HT(g2,T) are_disjoint) & h is_a_normal_form_of S-Poly(g1,g2,T)
  ,PolyRedRel(G,T) holds h = 0_(n,L));

:: theorem 5.68 (ii) ==> (iii), p. 223

theorem :: GROEB_3:59
  for n being Element of NAT, T being connected admissible 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, G being Subset of Polynom-Ring(n,L) st
not(0_(n,L) in G) holds (for g1,g2,h being Polynomial of n,L st g1 in G & g2 in
G & not(HT(g1,T),HT(g2,T) are_disjoint) & h is_a_normal_form_of S-Poly(g1,g2,T)
  ,PolyRedRel(G,T) holds h = 0_(n,L)) implies G is_Groebner_basis_wrt T;

:: theorem 5.68 (iii) ==> (i), p. 223