The Mizar article:

Construction of Gr\"obner bases. S-Polynomials and Standard Representations

by
Christoph Schwarzweller

Received June 11, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: GROEB_2
[ 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,
      GROUP_1, BINOP_1, ARYTM_3, TERMORD, IDEAL_1, RELAT_2, DICKSON, MCART_1,
      FINSEQ_1, FINSEQ_4, REWRITE1, BINOM, TARSKI, FINSET_1, PBOOLE, POLYRED,
      CAT_3, SQUARE_1, ALGSEQ_1, BAGORDER, ORDERS_1, RFINSEQ, WAYBEL_4,
      FINSEQ_7, GROEB_1, GROEB_2;
 notation TARSKI, SUBSET_1, RELAT_1, XBOOLE_0, RELAT_2, RELSET_1, FUNCT_1,
      ORDINAL1, ALGSTR_1, RLVECT_1, FINSEQ_4, FINSET_1, MCART_1, REALSET1,
      FINSEQ_1, VECTSP_2, VECTSP_1, POLYNOM7, REAL_1, BINOM, PBOOLE, ORDERS_1,
      POLYNOM1, IDEAL_1, REWRITE1, BAGORDER, STRUCT_0, TERMORD, POLYRED,
      GROUP_1, SQUARE_1, BINARITH, TOPREAL1, NUMBERS, XREAL_0, NAT_1, GROEB_1,
      RFINSEQ, FINSEQ_7, WAYBEL_4;
 constructors REWRITE1, REAL_1, IDEAL_1, TERMORD, POLYRED, CQC_LANG, TOPREAL1,
      GROEB_1, FINSEQ_7, WELLFND1, WAYBEL_4, MONOID_0, MEMBERED, BINARITH,
      BAGORDER;
 clusters STRUCT_0, RELAT_1, FINSET_1, RELSET_1, VECTSP_1, FINSEQ_1, VECTSP_2,
      GCD_1, ALGSTR_1, POLYNOM1, POLYNOM2, NAT_1, INT_1, BINOM, POLYNOM7,
      TERMORD, IDEAL_1, SUBSET_1, POLYRED, RFINSEQ, XBOOLE_0, MEMBERED,
      NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 theorems TARSKI, RELSET_1, FINSEQ_1, ZFMISC_1, VECTSP_1, POLYNOM1, REAL_1,
      FINSEQ_4, RLVECT_1, NAT_1, MCART_1, POLYNOM7, REWRITE1, AXIOMS, XBOOLE_0,
      IDEAL_1, TERMORD, INT_1, FUNCT_1, FINSET_1, XBOOLE_1, PBOOLE, BINARITH,
      SEQM_3, VECTSP_2, POLYRED, SQUARE_1, FUNCT_2, BINOM, FINSEQ_3, RELAT_1,
      RELAT_2, WAYBEL_4, BAGORDER, RFINSEQ, FINSEQ_5, XCMPLX_0, TOPREAL1,
      ALGSTR_1, FINSEQ_7, GROEB_1, XCMPLX_1;
 schemes NAT_1, FUNCT_1, BINOM;

begin :: Preliminaries

theorem
 for X being set,
    p being FinSequence of X
st p <> {} holds p|1 = <*p/.1*> by FINSEQ_5:23;

theorem Th2:
for L being non empty LoopStr,
    p being FinSequence of L,
    n,m being Nat
st m <= n holds (p|n)|m = p|m
proof
let L be non empty LoopStr,
    p be FinSequence of L,
    n,m be Nat;
assume A1: m <= n;
set q = p|n;
A2: dom q = dom(p|(Seg n)) by TOPREAL1:def 1
        .= dom p /\ (Seg n) by FUNCT_1:68;
A3: Seg m c= Seg n by A1,FINSEQ_1:7;
A4: dom(q|m) = dom(q|(Seg m)) by TOPREAL1:def 1
           .= (dom p /\ (Seg n)) /\ (Seg m) by A2,FUNCT_1:68
           .= dom p /\ ((Seg n) /\ (Seg m)) by XBOOLE_1:16
           .= dom p /\ (Seg m) by A3,XBOOLE_1:28
           .= dom(p|(Seg m)) by FUNCT_1:68
           .= dom(p|m) by TOPREAL1:def 1;
 now let x be set;
  assume A5: x in dom(p|m);
  then reconsider x' = x as Nat;
  A6: x' in dom(p|(Seg m)) by A5,TOPREAL1:def 1;
  A7: x' in dom(q|(Seg m)) by A4,A5,TOPREAL1:def 1;
  A8: (q|m).x' = (q|(Seg m)).x' by TOPREAL1:def 1
              .= q.x' by A7,FUNCT_1:68;
   x' in dom(p) /\ (Seg m) by A6,FUNCT_1:68;
  then x' in dom p & x' in Seg m by XBOOLE_0:def 3;
  then x' in dom(p) /\ (Seg n) by A3,XBOOLE_0:def 3;
  then A9: x' in dom(p|(Seg n)) by FUNCT_1:68;
  A10: q.x' = (p|(Seg n)).x' by TOPREAL1:def 1
          .= p.x' by A9,FUNCT_1:68;
   (p|m).x' = (p|(Seg m)).x' by TOPREAL1:def 1
          .= p.x' by A6,FUNCT_1:68;
  hence (p|m).x = (q|m).x by A8,A10;
  end;
hence thesis by A4,FUNCT_1:9;
end;

theorem
 for L being add-associative right_zeroed
            right_complementable (non empty LoopStr),
    p being FinSequence of L,
    n being Nat
st for k being Nat st k in dom p & k > n holds p.k = 0.L
holds Sum p = Sum(p|n)
proof
let L be add-associative right_zeroed right_complementable
         (non empty LoopStr),
    p be FinSequence of L,
    n be Nat;
assume A1: for k being Nat st k in dom p & k > n holds p.k = 0.L;
defpred P[Nat] means
  for p being FinSequence of L,
      n being Nat
  st len p = $1 &
     for k being Nat st k in dom p & k > n holds p.k = 0.L
  holds Sum p = Sum(p|n);
A2: P[0]
    proof let p be FinSequence of L,
            n be Nat;
    assume len p = 0 &
           for k being Nat st k in dom p & k > n holds p.k = 0.L;
    then len p <= n by NAT_1:18;
    hence Sum p = Sum(p|n) by TOPREAL1:2;
    end;
A3: now let k be Nat;
    assume A4: P[k];
     now let p be FinSequence of L,
            n be Nat;
      assume A5: len p = k+1 &
             for l being Nat st l in dom p & l > n holds p.l = 0.L;
      set q = p|(Seg k);
      reconsider q as FinSequence of L by FINSEQ_1:23;
      A6: dom p = Seg(k+1) by A5,FINSEQ_1:def 3;
      A7: k <= len p by A5,NAT_1:29;
      then A8: len q = k by FINSEQ_1:21;
      A9: k <= k + 1 by NAT_1:29;
       dom q = Seg(k) by A7,FINSEQ_1:21;
      then A10: dom q c= dom p by A6,A9,FINSEQ_1:7;
      A11: k + 1 in dom p by A6,FINSEQ_1:6;
      then A12: q^<*p/.(k+1)*> = q^<*p.(k+1)*> by FINSEQ_4:def 4
                              .= p by A5,FINSEQ_3:61;
      A13: q = p|k by TOPREAL1:def 1;
       now per cases;
      case k < n;
        then A14: k + 1 <= n by NAT_1:38;
        A15: dom(p|n) = dom(p|(Seg n)) by TOPREAL1:def 1;
        A16: now let u be set;
             assume u in dom(p|n);
             then A17: u in dom(p|(Seg n)) by TOPREAL1:def 1;
              dom(p|(Seg n)) c= dom p by FUNCT_1:76;
             hence u in dom p by A17;
             end;
         now let u be set;
          assume A18: u in dom p;
          then A19: u in Seg(k+1) by A5,FINSEQ_1:def 3;
          reconsider u' = u as Nat by A18;
           1 <= u' & u' <= k + 1 by A19,FINSEQ_1:3;
          then 1 <= u' & u' <= n by A14,AXIOMS:22;
          then u' in Seg n by FINSEQ_1:3;
          then u' in dom(p) /\ (Seg n) by A18,XBOOLE_0:def 3;
          hence u in dom(p|n) by A15,FUNCT_1:68;
          end;
        then A20: dom(p|n) = dom p by A16,TARSKI:2;
         for x being set st x in dom(p|(Seg n)) holds (p|(Seg n)).x = p.x
          by FUNCT_1:68;
        then p|(Seg n) = p by A15,A20,FUNCT_1:9;
        hence Sum(p|n) = Sum p by TOPREAL1:def 1;
      case A21: n <= k;
        A22: now let l be Nat;
             assume A23: l in dom q & l > n;
             then A24: p.l = 0.L by A5,A10;
             thus q.l = q/.l by A23,FINSEQ_4:def 4
                     .= p/.l by A13,A23,TOPREAL1:1
                     .= 0.L by A10,A23,A24,FINSEQ_4:def 4;
             end;
         k + 1 > n by A21,NAT_1:38;
        then A25: 0.L = p.(k+1) by A5,A11
                     .= p/.(k+1) by A11,FINSEQ_4:def 4;
        thus Sum p = Sum q + Sum(<*p/.(k+1)*>) by A12,RLVECT_1:58
                  .= Sum q + p/.(k+1) by RLVECT_1:61
                  .= Sum q by A25,RLVECT_1:def 7
                  .= Sum(q|n) by A4,A8,A22
                  .= Sum(p|n) by A13,A21,Th2;
        end;
      hence Sum p = Sum(p|n);
      end;
    hence P[k+1];
    end;
A26: for k being Nat holds P[k] from Ind(A2,A3);
consider k being Nat such that A27: len p = k;
thus thesis by A1,A26,A27;
end;

theorem
 for L being add-associative right_zeroed Abelian (non empty LoopStr),
    f being FinSequence of L,
    i,j being Nat
holds Sum Swap(f,i,j) = Sum f
proof
let L be add-associative right_zeroed Abelian (non empty LoopStr),
    f be FinSequence of L,
    i,j be Nat;
per cases;
suppose not(1 <= i & i <= len f & 1 <= j & j <= len f);
  hence thesis by FINSEQ_7:def 2;
suppose A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
  then i in Seg(len f) & j in Seg(len f) by FINSEQ_1:3;
  then A2: i in dom f & j in dom f by FINSEQ_1:def 3;
   now per cases by REAL_1:def 5;
  case i = j;
    hence thesis by FINSEQ_7:21;
  case A3: i < j;
    then Swap(f, i, j) =
       (f|(i-'1))^<*f/.j*>^(f/^i)|(j-'i-'1)^<*f/.i*>^(f/^j) by A1,FINSEQ_7:29;
    then A4: Sum(Swap(f, i, j))
       = Sum(f|(i-'1)^<*f/.j*>^(f/^i)|(j-'i-'1)^<*f/.i*>)
         + Sum(f/^j) by RLVECT_1:58
      .= (Sum(f|(i-'1)^<*f/.j*>^(f/^i)|(j-'i-'1)) + Sum(<*f/.i*>))
         + Sum(f/^j) by RLVECT_1:58
      .= ((Sum(f|(i-'1)^<*f/.j*>) + Sum((f/^i)|(j-'i-'1))) + Sum(<*f/.i*>))
         + Sum(f/^j) by RLVECT_1:58
      .= (((Sum(f|(i-'1)) + Sum(<*f/.j*>)) + Sum((f/^i)|(j-'i-'1)))
         + Sum(<*f/.i*>)) + Sum(f/^j) by RLVECT_1:58
      .= (((Sum(f|(i-'1)) + Sum(<*f/.j*>)) + Sum(<*f/.i*>))
         + Sum((f/^i)|(j-'i-'1))) + Sum(f/^j) by RLVECT_1:def 6
      .= (((Sum(f|(i-'1)) + Sum(<*f/.i*>)) + Sum(<*f/.j*>))
         + Sum((f/^i)|(j-'i-'1))) + Sum(f/^j) by RLVECT_1:def 6
      .= ((Sum((f|(i-'1))^(<*f/.i*>)) + Sum(<*f/.j*>))
         + Sum((f/^i)|(j-'i-'1))) + Sum(f/^j) by RLVECT_1:58
      .= ((Sum((f|(i-'1))^(<*f/.i*>)) + Sum((f/^i)|(j-'i-'1)))
         + Sum(<*f/.j*>)) + Sum(f/^j) by RLVECT_1:def 6
      .= (Sum((f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1)))
         + Sum(<*f/.j*>)) + Sum(f/^j) by RLVECT_1:58
      .= Sum((f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>))
         + Sum(f/^j) by RLVECT_1:58
      .= Sum((f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)^(f/^j))
         by RLVECT_1:58;
          (f|(i-'1))^(<*f/.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)^(f/^j)
       = (f|(i-'1))^(<*f.i*>)^((f/^i)|(j-'i-'1))^(<*f/.j*>)^(f/^j)
          by A2,FINSEQ_4:def 4
      .= (f|(i-'1))^(<*f.i*>)^((f/^i)|(j-'i-'1))^(<*f.j*>)^(f/^j)
          by A2,FINSEQ_4:def 4
      .= f by A1,A3,FINSEQ_7:1;
      hence thesis by A4;
  case A5: i > j;
    then Swap(f, j, i) =
       (f|(j-'1))^<*f/.i*>^(f/^j)|(i-'j-'1)^<*f/.j*>^(f/^i) by A1,FINSEQ_7:29;
    then A6: Sum(Swap(f, j, i))
       = Sum(f|(j-'1)^<*f/.i*>^(f/^j)|(i-'j-'1)^<*f/.j*>)
         + Sum(f/^i) by RLVECT_1:58
      .= (Sum(f|(j-'1)^<*f/.i*>^(f/^j)|(i-'j-'1)) + Sum(<*f/.j*>))
         + Sum(f/^i) by RLVECT_1:58
      .= ((Sum(f|(j-'1)^<*f/.i*>) + Sum((f/^j)|(i-'j-'1))) + Sum(<*f/.j*>))
         + Sum(f/^i) by RLVECT_1:58
      .= (((Sum(f|(j-'1)) + Sum(<*f/.i*>)) + Sum((f/^j)|(i-'j-'1)))
         + Sum(<*f/.j*>)) + Sum(f/^i) by RLVECT_1:58
      .= (((Sum(f|(j-'1)) + Sum(<*f/.i*>)) + Sum(<*f/.j*>))
         + Sum((f/^j)|(i-'j-'1))) + Sum(f/^i) by RLVECT_1:def 6
      .= (((Sum(f|(j-'1)) + Sum(<*f/.j*>)) + Sum(<*f/.i*>))
         + Sum((f/^j)|(i-'j-'1))) + Sum(f/^i) by RLVECT_1:def 6
      .= ((Sum((f|(j-'1))^(<*f/.j*>)) + Sum(<*f/.i*>))
         + Sum((f/^j)|(i-'j-'1))) + Sum(f/^i) by RLVECT_1:58
      .= ((Sum((f|(j-'1))^(<*f/.j*>)) + Sum((f/^j)|(i-'j-'1)))
         + Sum(<*f/.i*>)) + Sum(f/^i) by RLVECT_1:def 6
      .= (Sum((f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1)))
         + Sum(<*f/.i*>)) + Sum(f/^i) by RLVECT_1:58
      .= Sum((f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>))
         + Sum(f/^i) by RLVECT_1:58
      .= Sum((f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)^(f/^i))
         by RLVECT_1:58;
          (f|(j-'1))^(<*f/.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)^(f/^i)
       = (f|(j-'1))^(<*f.j*>)^((f/^j)|(i-'j-'1))^(<*f/.i*>)^(f/^i)
          by A2,FINSEQ_4:def 4
      .= (f|(j-'1))^(<*f.j*>)^((f/^j)|(i-'j-'1))^(<*f.i*>)^(f/^i)
          by A2,FINSEQ_4:def 4
      .= f by A1,A5,FINSEQ_7:1;
     hence thesis by A6,FINSEQ_7:23;
  end;
hence thesis;
end;

theorem
 for n being Ordinal,
    T being TermOrder of n,
    b1,b2,b3 being bag of n
st b1 <= b3,T & b2 <= b3,T holds max(b1,b2,T) <= b3,T by TERMORD:12;

theorem
 for n being Ordinal,
    T being TermOrder of n,
    b1,b2,b3 being bag of n
st b3 <= b1,T & b3 <= b2,T holds b3 <= min(b1,b2,T),T by TERMORD:11;

definition
let X be set,
    b1,b2 be bag of X;
assume A1:b2 divides b1;
func b1 / b2 -> bag of X means :Def1:
  b2 + it = b1;
existence by A1,TERMORD:1;
uniqueness
 proof
 let b3,b4 be bag of X;
 assume A2: b2 + b3 = b1;
 assume A3: b2 + b4 = b1;
 A4: dom b3 = X by PBOOLE:def 3 .= dom b4 by PBOOLE:def 3;
  now let x be set;
   assume x in dom b3;
   thus b3.x = (b2.x + b3.x) -' b2.x by BINARITH:39
            .= b1.x -' b2.x by A2,POLYNOM1:def 5
            .= (b2.x + b4.x) -' b2.x by A3,POLYNOM1:def 5
            .= b4.x by BINARITH:39;
   end;
 hence thesis by A4,FUNCT_1:9;
 end;
end;

definition
::: exercise 5.45, p. 211
let X be set,
    b1,b2 be bag of X;
func lcm(b1,b2) -> bag of X means :Def2:
  for k being set holds it.k = max(b1.k,b2.k);
existence
 proof
 defpred Q[set,set] means $2 = max(b1.$1,b2.$1);
 A1: for x,y1,y2 being set st x in X & Q[x,y1] & Q[x,y2]
       holds y1 = y2;
 A2: for x being set st x in X ex y being set st Q[x,y];
 consider b being Function such that
 A3: dom b = X & for x being set st x in X holds Q[x,b.x]
     from FuncEx(A1,A2);
 reconsider b as ManySortedSet of X by A3,PBOOLE:def 3;
  now let u be set;
     assume u in rng b;
     then consider x being set such that
     A4: x in dom b & u = b.x by FUNCT_1:def 5;
     A5: u = max(b1.x,b2.x) by A3,A4;
      b1.x in NAT & b2.x in NAT;
     hence u in NAT by A5,SQUARE_1:49;
     end;
 then A6: rng b c= NAT by TARSKI:def 3;
  now let u be set;
   assume A7: u in support b;
   then A8: b.u <> 0 by POLYNOM1:def 7;
   A9: support b c= dom b by POLYNOM1:41;
    now assume not(u in support(b1) \/ support(b2));
     then not(u in support(b1)) & not(u in support(b2)) by XBOOLE_0:def 2;
     then b1.u = 0 & b2.u = 0 by POLYNOM1:def 7;
     then max(b1.u,b2.u) = 0;
     hence contradiction by A3,A7,A8,A9;
     end;
   hence u in support(b1) \/ support(b2);
   end;
 then support b c= (support(b1) \/ support(b2)) by TARSKI:def 3;
 then support b is finite by FINSET_1:13;
 then reconsider b as bag of X by A6,POLYNOM1:def 8,SEQM_3:def 8;
 A10: dom b = X by PBOOLE:def 3 .= dom b1 by PBOOLE:def 3;
 A11: dom b = X by PBOOLE:def 3 .= dom b2 by PBOOLE:def 3;
 take b;
  now let k be set;
    now per cases;
   case k in dom b;
     hence b.k = max(b1.k,b2.k) by A3;
   case A12: not(k in dom b);
     then b1.k = 0 & b2.k = 0 by A10,A11,FUNCT_1:def 4;
     hence b.k = max(b1.k,b2.k) by A12,FUNCT_1:def 4;
     end;
   hence b.k = max(b1.k,b2.k);
   end;
 hence thesis;
 end;
uniqueness
 proof
 let b3,b4 be bag of X;
 assume A13: for k being set holds b3.k = max(b1.k,b2.k);
 assume A14: for k being set holds b4.k = max(b1.k,b2.k);
 A15: dom b3 = X by PBOOLE:def 3 .= dom b4 by PBOOLE:def 3;
  now let u be set;
   assume u in dom b3;
   thus b3.u = max(b1.u,b2.u) by A13 .= b4.u by A14;
   end;
 hence thesis by A15,FUNCT_1:9;
 end;
commutativity;
idempotence;
synonym b1 lcm b2;
end;

definition
let X be set,
    b1,b2 be bag of X;
pred b1,b2 are_disjoint means :Def3:
  for i being set holds b1.i = 0 or b2.i = 0;
antonym b1,b2 are_non_disjoint;
end;

theorem Th7:
::: exercise 5.45, p. 211
for X being set,
    b1,b2 being bag of X
holds b1 divides lcm(b1,b2) & b2 divides lcm(b1,b2)
proof
let X be set,
    b1,b2 be bag of X;
set bb = lcm(b1,b2);
 now let k be set;
   b1.k <= max(b1.k,b2.k) by SQUARE_1:46;
  hence b1.k <= bb.k by Def2;
  end;
hence b1 divides lcm(b1,b2) by POLYNOM1:def 13;
 now let k be set;
   b2.k <= max(b1.k,b2.k) by SQUARE_1:46;
  hence b2.k <= bb.k by Def2;
  end;
hence b2 divides lcm(b1,b2) by POLYNOM1:def 13;
end;

theorem Th8:
::: exercise 5.45, p. 211
for X being set,
    b1,b2,b3 be bag of X
holds (b1 divides b3 & b2 divides b3) implies lcm(b1,b2) divides b3
proof
let X being set,
    b1,b2,b3 be bag of X;
assume A1: b1 divides b3 & b2 divides b3;
 now let k be set;
  assume k in X;
   now per cases by SQUARE_1:49;
    case max(b1.k,b2.k) = b1.k;
      hence max(b1.k,b2.k) <= b3.k by A1,POLYNOM1:def 13;
    case max(b1.k,b2.k) = b2.k;
      hence max(b1.k,b2.k) <= b3.k by A1,POLYNOM1:def 13;
      end;
  hence lcm(b1,b2).k <= b3.k by Def2;
  end;
hence thesis by POLYNOM1:50;
end;

theorem
 for X being set,
    T being TermOrder of X,
    b1,b2 being bag of X
holds b1,b2 are_disjoint iff lcm(b1,b2) = b1 + b2
proof
let X be set,
    T be TermOrder of X,
    b1,b2 be bag of X;
A1: now assume A2: b1,b2 are_disjoint;
    now let k be set;
     A3: 0 <= b1.k & 0 <= b2.k by NAT_1:18;
      now per cases by A2,Def3;
     case A4: b1.k = 0;
       hence (b1+b2).k = 0 + b2.k by POLYNOM1:def 5
                     .= max(b1.k,b2.k) by A3,A4,SQUARE_1:def 2;
     case A5: b2.k = 0;
       hence (b1+b2).k = b1.k + 0 by POLYNOM1:def 5
                     .= max(b1.k,b2.k) by A3,A5,SQUARE_1:def 2;
       end;
     hence (b1+b2).k = max(b1.k,b2.k);
     end;
   hence lcm(b1,b2) = b1 + b2 by Def2;
   end;
 now assume A6: lcm(b1,b2) = b1 + b2;
   now let k be set;
    A7: lcm(b1,b2).k = max(b1.k,b2.k) by Def2;
     now per cases by A6,A7,SQUARE_1:49;
    case (b1 + b2).k = b1.k;
      then b1.k + b2.k = b1.k + 0 by POLYNOM1:def 5;
      hence b2.k = 0 by XCMPLX_1:2;
    case (b1 + b2).k = b2.k;
      then b1.k + b2.k = 0 + b2.k by POLYNOM1:def 5;
      hence b1.k = 0 by XCMPLX_1:2;
      end;
    hence b1.k = 0 or b2.k = 0;
    end;
  hence b1,b2 are_disjoint by Def3;
  end;
hence thesis by A1;
end;

theorem Th10:
for X being set,
    b being bag of X
holds b/b = EmptyBag X
proof
let X be set,
    b be bag of X;
 b + EmptyBag X = b by POLYNOM1:57;
hence thesis by Def1;
end;

theorem Th11:
for X being set,
    b1,b2 be bag of X
holds b2 divides b1 iff lcm(b1,b2) = b1
proof
let X being set,
    b1,b2 be bag of X;
 now assume A1: b2 divides b1;
   now let k be set;
     b2.k <= b1.k by A1,POLYNOM1:def 13;
    hence b1.k = max(b1.k,b2.k) by SQUARE_1:def 2;
    end;
  hence lcm(b1,b2) = b1 by Def2;
  end;
hence thesis by Th7;
end;

theorem
::: exercise 5.69 (i) ==> (ii), p. 223
 for X being set,
    b1,b2,b3 being bag of X
holds b1 divides lcm(b2,b3) implies lcm(b2,b1) divides lcm(b2,b3)
proof
let X being set,
    b1,b2,b3 be bag of X;
assume A1: b1 divides lcm(b2,b3);
 for k being set st k in X holds lcm(b2,b1).k <= lcm(b2,b3).k
  proof
  let k be set;
  assume k in X;
   b1.k <= lcm(b2,b3).k by A1,POLYNOM1:def 13;
  then A2: b1.k <= max(b2.k,b3.k) by Def2;
   b2.k <= max(b2.k,b3.k) by SQUARE_1:46;
  then max(b2.k,b1.k) <= max(b2.k,b3.k) by A2,SQUARE_1:50;
  then max(b2.k,b1.k) <= lcm(b2,b3).k by Def2;
  hence lcm(b2,b1).k <= lcm(b2,b3).k by Def2;
  end;
hence thesis by POLYNOM1:50;
end;

theorem
::: exercise 5.69 (ii) ==> (iii), p. 223
 for X being set,
    b1,b2,b3 being bag of X
holds lcm(b2,b1) divides lcm(b2,b3) implies lcm(b1,b3) divides lcm(b2,b3)
proof
let X be set,
    b1,b2,b3 be bag of X;
assume A1: lcm(b2,b1) divides lcm(b2,b3);
 for k being set st k in X holds lcm(b1,b3).k <= lcm(b2,b3).k
  proof
  let k be set;
  assume k in X;
   lcm(b2,b1).k <= lcm(b2,b3).k by A1,POLYNOM1:def 13;
  then max(b2.k,b1.k) <= lcm(b2,b3).k by Def2;
  then A2: max(b2.k,b1.k) <= max(b2.k,b3.k) by Def2;
   b1.k <= max(b2.k,b1.k) by SQUARE_1:46;
  then A3: b1.k <= max(b2.k,b3.k) by A2,AXIOMS:22;
   b3.k <= max(b2.k,b3.k) by SQUARE_1:46;
  then max(b1.k,b3.k) <= max(b2.k,b3.k) by A3,SQUARE_1:50;
  then max(b1.k,b3.k) <= lcm(b2,b3).k by Def2;
  hence lcm(b1,b3).k <= lcm(b2,b3).k by Def2;
  end;
hence thesis by POLYNOM1:50;
end;

theorem
::: exercise 5.69 (iii) ==> (i), p. 223
 for n being set,
    b1,b2,b3 being bag of n
holds lcm(b1,b3) divides lcm(b2,b3) implies b1 divides lcm(b2,b3)
proof
let X be set,
    b1,b2,b3 be bag of X;
assume A1: lcm(b1,b3) divides lcm(b2,b3);
 for k being set st k in X holds b1.k <= lcm(b2,b3).k
  proof
  let k be set;
  assume k in X;
   lcm(b1,b3).k <= lcm(b2,b3).k by A1,POLYNOM1:def 13;
  then max(b1.k,b3.k) <= lcm(b2,b3).k by Def2;
  then A2: max(b1.k,b3.k) <= max(b2.k,b3.k) by Def2;
   b1.k <= max(b1.k,b3.k) by SQUARE_1:46;
  then b1.k <= max(b2.k,b3.k) by A2,AXIOMS:22;
  hence b1.k <= lcm(b2,b3).k by Def2;
  end;
hence thesis by POLYNOM1:50;
end;

theorem
 for n being Nat,
    T being connected admissible TermOrder of n,
    P being non empty Subset of Bags n
ex b being bag of n
st b in P &
   for b' being bag of n st b' in P holds b <= b',T
proof
let n be Nat,
    T be connected admissible TermOrder of n,
    P be non empty Subset of Bags n;
set R = RelStr(#Bags n, T#), m = MinElement(P,R);
A1: m in P & m is_minimal_wrt P,the InternalRel of R by BAGORDER:def 19;
 m is Element of Bags n;
then reconsider b = m as bag of n;
A2: T is_connected_in field T by RELAT_2:def 14;
 now let b' be bag of n;
  assume A3: b' in P;
   b <= b,T & b' <= b',T by TERMORD:6;
  then [b,b] in T & [b',b'] in T by TERMORD:def 2;
  then A4: b in field T & b' in field T by RELAT_1:30;
   now per cases;
  case b' = b;
     hence b <= b',T by TERMORD:6;
  case A5: b' <> b;
    then not([b',b] in T) by A1,A3,WAYBEL_4:def 26;
    then [b,b'] in T by A2,A4,A5,RELAT_2:def 6;
    hence b <= b',T by TERMORD:def 2;
    end;
  hence b <= b',T;
  end;
hence thesis by A1;
end;

definition
let L be add-associative right_zeroed right_complementable
         (non trivial LoopStr),
    a be non-zero Element of L;
cluster -a -> non-zero;
coherence
 proof
 A1: a <> 0.L by RLVECT_1:def 13;
  now assume -a = 0.L;
   then --a = 0.L by RLVECT_1:25;
   hence contradiction by A1,RLVECT_1:30;
   end;
 hence thesis by RLVECT_1:def 13;
 end;
end;

definition
let X be set,
    L be left_zeroed right_zeroed add-cancelable
         distributive (non empty doubleLoopStr),
    m be Monomial of X,L,
    a be Element of L;
cluster a * m -> monomial-like;
coherence
 proof
 set p = a * m;
  now per cases by POLYNOM7:6;
 case A1: Support m = {};
    now assume A2: Support p <> {};
     consider b being Element of Support p;
      b in Support p by A2;
     then reconsider b as Element of Bags X;
      p.b = a * m.b by POLYNOM7:def 10
        .= a * 0.L by A1,POLYNOM1:def 9
        .= 0.L by BINOM:2;
     hence contradiction by A2,POLYNOM1:def 9;
     end;
   hence thesis by POLYNOM7:6;
 case ex b being bag of X st Support m = {b};
   then consider b being bag of X such that
   A3: Support m = {b};
   reconsider b as Element of Bags X by POLYNOM1:def 14;
    now per cases;
   case A4: a = 0.L;
      now assume A5: Support p <> {};
       consider b being Element of Support p;
        b in Support p by A5;
       then reconsider b as Element of Bags X;
        p.b = a * m.b by POLYNOM7:def 10
          .= 0.L by A4,BINOM:1;
       hence contradiction by A5,POLYNOM1:def 9;
       end;
     hence Support p = {};
   case a <> 0.L;
     A6: now let b' be Element of Bags X;
         assume b' <> b;
         then not(b' in Support m) by A3,TARSKI:def 1;
         then A7: m.b' = 0.L by POLYNOM1:def 9;
          p.b' = a * m.b' by POLYNOM7:def 10;
         hence p.b' = 0.L by A7,BINOM:2;
         end;
      now per cases;
     case A8: a * m.b = 0.L;
        now assume A9: Support p <> {};
         consider b' being Element of Support p;
          b' in Support p by A9;
         then reconsider b' as Element of Bags X;
         A10: p.b' <> 0.L by A9,POLYNOM1:def 9;
         then b' = b by A6;
         hence contradiction by A8,A10,POLYNOM7:def 10;
         end;
       hence Support p = {};
     case A11: a * m.b <> 0.L;
        A12: now let u be set;
            assume u in {b};
            then A13: u = b by TARSKI:def 1;
             p.b <> 0.L by A11,POLYNOM7:def 10;
            hence u in Support p by A13,POLYNOM1:def 9;
            end;
         now let u be set;
          assume A14: u in Support p;
          then reconsider u' = u as Element of Bags X;
           p.u' <> 0.L by A14,POLYNOM1:def 9;
          then u' = b by A6;
          hence u in {b} by TARSKI:def 1;
          end;
        hence Support p = {b} by A12,TARSKI:2;
        end;
     hence thesis by POLYNOM7:6;
     end;
   hence thesis by POLYNOM7:6;
   end;
 hence thesis;
 end;
end;

definition
let n be Ordinal,
    L be left_zeroed right_zeroed add-cancelable
         distributive domRing-like (non trivial doubleLoopStr),
    p be non-zero Polynomial of n,L,
    a be non-zero Element of L;
cluster a * p -> non-zero;
coherence
 proof
 set ap = a * p;
  p <> 0_(n,L) by POLYNOM7:def 2;
 then A1: Support p <> {} by POLYNOM7:1;
 consider b being Element of Support p;
  b in Support p by A1;
 then reconsider b as Element of Bags n;
 A2: p.b <> 0.L by A1,POLYNOM1:def 9;
  a <> 0.L by RLVECT_1:def 13;
 then a * p.b <> 0.L by A2,VECTSP_2:def 5;
 then ap.b <> 0.L by POLYNOM7:def 10;
 then b in Support ap by POLYNOM1:def 9;
 then ap <> 0_(n,L) by POLYNOM7:1;
 hence thesis by POLYNOM7:def 2;
 end;
end;

theorem Th16:
for n being Ordinal,
    T being TermOrder of n,
    L being right_zeroed right-distributive (non empty doubleLoopStr),
    p,q being Series of n,L,
    b being bag of n
holds b *' (p + q) = b *' p + b *' q
proof
let n be Ordinal,
    T be TermOrder of n,
    L be right_zeroed right-distributive (non empty doubleLoopStr),
    p1,p2 be Series of n,L,
    b be bag of n;
set q1 = b *' (p1 + p2), q2 = b *' p1 + b *' p2;
A1: dom q1 = Bags n by FUNCT_2:def 1 .= dom q2 by FUNCT_2:def 1;
 now let x be set;
  assume x in dom q1;
  then reconsider u = x as bag of n by POLYNOM1:def 14;
   now per cases;
    case A2: b divides u;
      hence q1.u = (p1+p2).(u -' b) by POLYRED:def 1
                .= p1.(u -' b) + p2.(u -' b) by POLYNOM1:def 21
                .= (b*'p1).u + p2.(u -' b) by A2,POLYRED:def 1
                .= (b*'p1).u + (b*'p2).u by A2,POLYRED:def 1
                .= q2.u by POLYNOM1:def 21;
    case A3: not(b divides u);
      hence q1.u = 0.L by POLYRED:def 1
                .= 0.L + 0.L by RLVECT_1:def 7
                .= (b*'p1).u + 0.L by A3,POLYRED:def 1
                .= (b*'p1).u + (b*'p2).u by A3,POLYRED:def 1
                .= q2.u by POLYNOM1:def 21;
    end;
  hence q1.x = q2.x;
  end;
hence thesis by A1,FUNCT_1:9;
end;

theorem Th17:
for n being Ordinal,
    T being TermOrder of n,
    L being add-associative right_zeroed right_complementable
            (non empty LoopStr),
    p being Series of n,L,
    b being bag of n
holds b *' (-p) = -(b *' p)
proof
let n be Ordinal,
    T be TermOrder of n,
    L be add-associative right_zeroed right_complementable
         (non empty LoopStr),
    p be Series of n,L,
    b be bag of n;
set q1 = b *' (-p), q2 = -(b *' p);
A1: dom q1 = Bags n by FUNCT_2:def 1 .= dom q2 by FUNCT_2:def 1;
 now let x be set;
  assume x in dom q1;
  then reconsider u = x as bag of n by POLYNOM1:def 14;
   now per cases;
    case A2: b divides u;
      then A3: (b*'p).u = p.(u-'b) by POLYRED:def 1;
      thus q1.u = (-p).(u-'b) by A2,POLYRED:def 1
               .= -(p.(u-'b)) by POLYNOM1:def 22
               .= (-(b*'p)).u by A3,POLYNOM1:def 22;
    case A4: not(b divides u);
      then A5: (b*'p).u = 0.L by POLYRED:def 1;
      thus q1.u = 0.L by A4,POLYRED:def 1
               .= -0.L by RLVECT_1:25
               .= q2.u by A5,POLYNOM1:def 22;
    end;
  hence q1.x = q2.x;
  end;
hence thesis by A1,FUNCT_1:9;
end;

theorem Th18:
for n being Ordinal,
    T being TermOrder of n,
    L being left_zeroed add-right-cancelable
            right-distributive (non empty doubleLoopStr),
    p being Series of n,L,
    b being bag of n,
    a being Element of L
holds b *' (a * p) = a * (b *' p)
proof
let n be Ordinal,
    T be TermOrder of n,
    L be left_zeroed add-right-cancelable
         right-distributive (non empty doubleLoopStr),
    p be Series of n,L,
    b be bag of n,
    a be Element of L;
set q1 = b *' (a * p), q2 = a * (b *' p);
A1: dom q1 = Bags n by FUNCT_2:def 1 .= dom q2 by FUNCT_2:def 1;
 now let x be set;
  assume x in dom q1;
  then reconsider u = x as bag of n by POLYNOM1:def 14;
   now per cases;
  case A2: b divides u;
    hence q1.u = (a*p).(u-'b) by POLYRED:def 1
              .= a * p.(u-'b) by POLYNOM7:def 10
              .= a * (b*'p).u by A2,POLYRED:def 1
              .= q2.u by POLYNOM7:def 10;
  case A3: not(b divides u);
    hence q1.u = 0.L by POLYRED:def 1
              .= a * 0.L by BINOM:2
              .= a * (b*'p).u by A3,POLYRED:def 1
              .= q2.u by POLYNOM7:def 10;
    end;
  hence q1.x = q2.x;
  end;
hence thesis by A1,FUNCT_1:9;
end;

theorem Th19:
for n being Ordinal,
    T being TermOrder of n,
    L being right-distributive (non empty doubleLoopStr),
    p,q being Series of n,L,
    a being Element of L
holds a * (p + q) = a * p + a * q
proof
let n be Ordinal,
    T be TermOrder of n,
    L be right-distributive (non empty doubleLoopStr),
    p1,p2 be Series of n,L,
    b be Element of L;
set q1 = b * (p1 + p2), q2 = b * p1 + b * p2;
A1: dom q1 = Bags n by FUNCT_2:def 1 .= dom q2 by FUNCT_2:def 1;
 now let x be set;
  assume x in dom q1;
  then reconsider u = x as bag of n by POLYNOM1:def 14;
   q1.u = b * (p1+p2).u by POLYNOM7:def 10
      .= b * (p1.u + p2.u) by POLYNOM1:def 21
      .= b * p1.u + b * p2.u by VECTSP_1:def 11
      .= (b*p1).u + b * p2.u by POLYNOM7:def 10
      .= (b*p1).u + (b*p2).u by POLYNOM7:def 10
      .= (b*p1 + b*p2).u by POLYNOM1:def 21;
  hence q1.x = q2.x;
  end;
hence thesis by A1,FUNCT_1:9;
end;

theorem Th20:
for X being set,
    L being add-associative right_zeroed right_complementable
            (non empty doubleLoopStr),
    a being Element of L
holds -(a _(X,L)) = (-a) _(X,L)
proof
let n be set,
    L be add-associative right_zeroed right_complementable
         (non empty doubleLoopStr),
    a be Element of L;
A1: dom(- (a _(n,L))) = Bags n by FUNCT_2:def 1
                    .= dom((-a) _(n,L)) by FUNCT_2:def 1;
 now let u be set;
  assume u in dom((-a) _(n,L));
  then reconsider u' = u as Element of Bags n;
   now per cases;
  case A2: u' = EmptyBag n;
    hence -((a _(n,L)).u') = - a by POLYNOM7:18
                          .= ((-a) _(n,L)).u' by A2,POLYNOM7:18;
  case A3: u' <> EmptyBag n;
     -0.L = 0.L by RLVECT_1:25;
    hence -((a _(n,L)).u') = 0.L by A3,POLYNOM7:18
                          .= ((-a) _(n,L)).u' by A3,POLYNOM7:18;
    end;
  hence ((-a) _(n,L)).u = (- (a _(n,L))).u by POLYNOM1:def 22;
  end;
hence thesis by A1,FUNCT_1:9;
end;

Lm1:
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,
    g being set,
    P being Subset of Polynom-Ring(n,L)
holds PolyRedRel(P,T) reduces f,g implies g is Polynomial of n,L
proof
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,
    g be set,
    P be Subset of Polynom-Ring(n,L);
set R = PolyRedRel(P,T);
assume R reduces f,g;
then consider p being RedSequence of R such that
A1: p.1 = f & p.len p = g by REWRITE1:def 3;
 len p > 0 by REWRITE1:def 2;
then A2: 1 <= len(p) by RLVECT_1:99;
then reconsider l = len p - 1 as Nat by INT_1:18;
A3: l + 1 = (len p + -1) + 1 by XCMPLX_0:def 8
         .= len p + (-1 + 1) by XCMPLX_1:1
         .= len p + 0;
then 1 <= l + 1 & l + 1 <= len p by NAT_1:37;
then l + 1 in Seg(len p) by FINSEQ_1:3;
then A4: l + 1 in dom p by FINSEQ_1:def 3;
set h = p.l;
per cases;
suppose len p = 1;
  hence thesis by A1;
suppose len p <> 1;
  then 1 < len p by A2,REAL_1:def 5;
  then 1 + -1 < len p + -1 by REAL_1:67;
  then 1 - 1 < len p - 1 by XCMPLX_0:def 8;
  then 0 + 1 < l + 1 by REAL_1:67;
  then 1 <= l & l <= l + 1 by NAT_1:38;
  then l in Seg(len p) by A3,FINSEQ_1:3;
  then l in dom p by FINSEQ_1:def 3;
  then [h,g] in R by A1,A3,A4,REWRITE1:def 2;
  then consider h',g' being set such that
  A5: [h,g] = [h',g'] &
      h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
      g' in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
   g = [h',g']`2 by A5,MCART_1:def 2 .= g' by MCART_1:def 2;
  hence g is Polynomial of n,L by A5,POLYNOM1:def 27;
end;

begin :: S-Polynomials

theorem Th21:
::: theorem 5.44, p. 210
for n being Nat,
    T being connected admissible TermOrder of n,
    L being add-associative right_complementable right_zeroed
            commutative associative well-unital distributive
            Abelian Field-like non degenerated (non empty doubleLoopStr),
    P being Subset of Polynom-Ring(n,L) st not(0_(n,L) in P)
holds (for p1,p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P
       for m1,m2 being Monomial of n,L st HM(m1 *'p1,T) = HM(m2 *'p2,T)
       holds PolyRedRel(P,T) reduces m1 *' p1 - m2 *' p2, 0_(n,L))
      implies P is_Groebner_basis_wrt T
proof
let n be Nat,
    T be admissible connected TermOrder of n,
    L be add-associative right_complementable right_zeroed
         commutative associative well-unital distributive
         Abelian Field-like non degenerated (non empty doubleLoopStr),
    P be Subset of Polynom-Ring(n,L);
assume not(0_(n,L) in P);
assume A1: for p1,p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P
            for m1,m2 being Monomial of n,L st HM(m1 *'p1,T) = HM(m2 *'p2,T)
            holds PolyRedRel(P,T) reduces m1 *' p1 - m2 *' p2, 0_(n,L);
set R = PolyRedRel(P,T);
 now let a,b,c being set;
  assume A2: [a,b] in R & [a,c] in R;
  then consider f,f1 being set such that
  A3: f in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
      f1 in the carrier of Polynom-Ring(n,L) &
      [a,b] = [f,f1] by ZFMISC_1:def 2;
  reconsider f1 as Polynomial of n,L by A3,POLYNOM1:def 27;
  A4: f in (the carrier of Polynom-Ring(n,L)) &
       not(f in {0_(n,L)}) by A3,XBOOLE_0:def 4;
  then reconsider f as Polynomial of n,L by POLYNOM1:def 27;
   f <> 0_(n,L) by A4,TARSKI:def 1;
  then reconsider f as non-zero Polynomial of n,L by POLYNOM7:def 2;
  consider f',f2 being set such that
  A5: f' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
      f2 in the carrier of Polynom-Ring(n,L) &
      [a,c] = [f',f2] by A2,ZFMISC_1:def 2;
  reconsider f2 as Polynomial of n,L by A5,POLYNOM1:def 27;
  A6: f' = [a,c]`1 by A5,MCART_1:def 1
        .= a by MCART_1:def 1
        .= [f,f1]`1 by A3,MCART_1:def 1
        .= f by MCART_1:def 1;
  A7: f1 = [a,b]`2 by A3,MCART_1:def 2 .= b by MCART_1:def 2;
  A8: f2 = [a,c]`2 by A5,MCART_1:def 2 .= c by MCART_1:def 2;
  A9: f' = [a,c]`1 by A5,MCART_1:def 1 .= a by MCART_1:def 1;
  A10: f reduces_to f1,P,T & f reduces_to f2,P,T
      by A2,A3,A5,A6,POLYRED:def 13;
  then consider g1 being Polynomial of n,L such that
  A11: g1 in P & f reduces_to f1,g1,T by POLYRED:def 7;
  consider b1 being bag of n such that
  A12: f reduces_to f1,g1,b1,T by A11,POLYRED:def 6;
  A13: g1 <> 0_(n,L) by A12,POLYRED:def 5;
  then reconsider g1 as non-zero Polynomial of n,L by POLYNOM7:def 2;
  consider g2 being Polynomial of n,L such that
  A14: g2 in P & f reduces_to f2,g2,T by A10,POLYRED:def 7;
  consider b2 being bag of n such that
  A15: f reduces_to f2,g2,b2,T by A14,POLYRED:def 6;
  A16: g2 <> 0_(n,L) by A15,POLYRED:def 5;
  then reconsider g2 as non-zero Polynomial of n,L by POLYNOM7:def 2;
  consider m1 being Monomial of n,L such that
  A17: f1 = f - m1 *' g1 & not(HT(m1*'g1,T) in Support f1) &
      HT(m1*'g1,T) <= HT(f,T),T by A11,GROEB_1:2;
  consider m2 being Monomial of n,L such that
  A18: f2 = f - m2 *' g2 & not(HT(m2*'g2,T) in Support f2) &
      HT(m2*'g2,T) <= HT(f,T),T by A14,GROEB_1:2;
  set mg1 = m1 *' g1, mg2 = m2 *' g2;
   now per cases;
  case m1 = 0_(n,L);
  then f1 = f - 0_(n,L) by A17,POLYRED:5 .= f by POLYRED:4;
  then R reduces b,c & R reduces c,c by A2,A6,A7,A9,REWRITE1:13,16;
  hence b,c are_convergent_wrt R by REWRITE1:def 7;
  case m2 = 0_(n,L);
  then f2 = f - 0_(n,L) by A18,POLYRED:5 .= f by POLYRED:4;
  then R reduces c,b & R reduces b,b by A2,A6,A8,A9,REWRITE1:13,16;
  hence b,c are_convergent_wrt R by REWRITE1:def 7;
  case m1 <> 0_(n,L) & m2 <> 0_(n,L);
  then reconsider m1,m2 as non-zero Monomial of n,L by POLYNOM7:def 2;
   HT(m1,T) + HT(g1,T) in Support mg1 &
  HT(m2,T) + HT(g2,T) in Support mg2 by TERMORD:29;
  then A19: mg1 <> 0_(n,L) & mg2 <> 0_(n,L) by POLYNOM7:1;
  A20: HC(g1,T) <> 0.L & HC(g2,T) <> 0.L by A13,A16,TERMORD:17;
  A21: f2 - f1
          = (f + -(m2 *' g2)) - (f - m1 *' g1) by A17,A18,POLYNOM1:def 23
         .= (f + -(m2 *' g2)) - (f + -(m1 *' g1)) by POLYNOM1:def 23
         .= (f + -(m2 *' g2)) + -(f + -(m1 *' g1)) by POLYNOM1:def 23
         .= (f + -(m2 *' g2)) + (-f + --(m1 *' g1)) by POLYRED:1
         .= f + (-(m2 *' g2) + (-f + (m1 *' g1))) by POLYNOM1:80
         .= f + (-f + (-(m2 *' g2) + (m1 *' g1))) by POLYNOM1:80
         .= (f + -f) + (-(m2 *' g2) + (m1 *' g1)) by POLYNOM1:80
         .= 0_(n,L) + (-(m2 *' g2) + (m1 *' g1)) by POLYRED:3
         .= (m1 *' g1) + -(m2 *' g2) by POLYRED:2
         .= mg1 - mg2 by POLYNOM1:def 23;
   PolyRedRel(P,T) reduces f2-f1,0_(n,L)
    proof
     now per cases;
    case mg1 - mg2 = 0_(n,L);
      hence thesis by A21,REWRITE1:13;
    case A22: mg1 - mg2 <> 0_(n,L);
       now per cases;
      case g1 = g2;
        then f2 - f1 = m1 *' g1 + -(m2 *' g1) by A21,POLYNOM1:def 23
                    .= g1 *' m1 + (-m2) *' g1 by POLYRED:6
                    .= (m1 + -m2) *' g1 by POLYNOM1:85;
        hence thesis by A11,POLYRED:45;
      case A23: g1 <> g2;
         now per cases;
          case A24: HT(mg1,T) <> HT(mg2,T);
             now per cases;
            case HT(mg2,T) < HT(mg1,T),T;
              then not(HT(mg1,T) <= HT(mg2,T),T) by TERMORD:5;
              then not(HT(mg1,T)) in Support(mg2) by TERMORD:def 6;
              then A25: mg2.(HT(mg1,T)) = 0.L by POLYNOM1:def 9;
              A26:  (mg1-mg2).(HT(mg1,T))
                 = (mg1+-mg2).(HT(mg1,T)) by POLYNOM1:def 23
                .= mg1.(HT(mg1,T))+(-mg2).(HT(mg1,T)) by POLYNOM1:def 21
                .= mg1.(HT(mg1,T))+-(mg2).(HT(mg1,T)) by POLYNOM1:def 22
                .= mg1.(HT(mg1,T))+0.L by A25,RLVECT_1:25
                .= mg1.(HT(mg1,T)) by RLVECT_1:def 7
                .= HC(mg1,T) by TERMORD:def 7;
              then (mg1-mg2).(HT(mg1,T)) <> 0.L by A19,TERMORD:17;
              then A27: HT(mg1,T) in Support(mg1 - mg2) by POLYNOM1:def 9;
              A28: HT(m1,T) + HT(g1,T) = HT(mg1,T) by TERMORD:31;
               (mg1 - mg2) -
              ((mg1-mg2).HT(mg1,T)/HC(g1,T)) * (HT(m1,T) *' g1)
                  = (mg1 - mg2) -
                    ((HC(m1,T)*HC(g1,T))/HC(g1,T)) * (HT(m1,T) *' g1)
                    by A26,TERMORD:32
                 .= (mg1 - mg2) -
                    ((HC(m1,T)*HC(g1,T))*(HC(g1,T)")) * (HT(m1,T) *' g1)
                    by VECTSP_1:def 23
                 .= (mg1 - mg2) -
                    (HC(m1,T)*(HC(g1,T)*(HC(g1,T)"))) * (HT(m1,T) *' g1)
                    by VECTSP_1:def 16
                 .= (mg1 - mg2) -
                    (HC(m1,T)*1_ L) * (HT(m1,T) *' g1) by A20,VECTSP_1:def 22
                 .= (mg1 - mg2) -
                    HC(m1,T) * (HT(m1,T) *' g1) by VECTSP_1:def 19
                 .= (mg1 - mg2) - Monom(HC(m1,T),HT(m1,T)) *' g1 by POLYRED:22
                 .= (mg1 - mg2) - Monom(coefficient(m1),HT(m1,T)) *'g1
                    by TERMORD:23
                 .= (mg1 - mg2) - Monom(coefficient(m1),term(m1)) *'g1
                    by TERMORD:23
                 .= (mg1 - mg2) - mg1 by POLYNOM7:11
                 .= (mg1+-mg2)-mg1 by POLYNOM1:def 23
                 .= (mg1+-mg2)+-mg1 by POLYNOM1:def 23
                 .= (mg1+-mg1)+-mg2 by POLYNOM1:80
                 .= 0_(n,L)+-mg2 by POLYRED:3
                 .= -mg2 by POLYRED:2;
              then mg1-mg2 reduces_to -mg2,g1,HT(mg1,T),T
                 by A13,A22,A27,A28,POLYRED:def 5;
              then mg1-mg2 reduces_to -mg2,g1,T by POLYRED:def 6;
              then mg1-mg2 reduces_to -mg2,P,T by A11,POLYRED:def 7;
              then [mg1-mg2,-mg2] in R by POLYRED:def 13;
              then A29: R reduces mg1-mg2,-mg2 by REWRITE1:16;
               R reduces (-m2)*'g2,0_(n,L) by A14,POLYRED:45;
              then R reduces -mg2,0_(n,L) by POLYRED:6;
              hence thesis by A21,A29,REWRITE1:17;
            case not(HT(mg2,T) < HT(mg1,T),T);
              then HT(mg1,T) <= HT(mg2,T),T by TERMORD:5;
              then HT(mg1,T) < HT(mg2,T),T by A24,TERMORD:def 3;
              then not(HT(mg2,T) <= HT(mg1,T),T) by TERMORD:5;
              then not(HT(mg2,T)) in Support(mg1) by TERMORD:def 6;
              then A30: mg1.(HT(mg2,T)) = 0.L by POLYNOM1:def 9;
              A31:  (mg2-mg1).(HT(mg2,T))
                 = (mg2+-mg1).(HT(mg2,T)) by POLYNOM1:def 23
                .= mg2.(HT(mg2,T))+(-mg1).(HT(mg2,T)) by POLYNOM1:def 21
                .= mg2.(HT(mg2,T))+-(mg1).(HT(mg2,T)) by POLYNOM1:def 22
                .= mg2.(HT(mg2,T))+0.L by A30,RLVECT_1:25
                .= mg2.(HT(mg2,T)) by RLVECT_1:def 7
                .= HC(mg2,T) by TERMORD:def 7;
              then (mg2-mg1).(HT(mg2,T)) <> 0.L by A19,TERMORD:17;
              then A32: HT(mg2,T) in Support(mg2 - mg1) by POLYNOM1:def 9;
              A33: HT(m2,T) + HT(g2,T) = HT(mg2,T) by TERMORD:31;
              reconsider x = -0_(n,L)
                 as Element of Polynom-Ring(n,L)
                 by POLYNOM1:def 27;
              reconsider x as Element of Polynom-Ring(n,L);
               0.Polynom-Ring(n,L) = 0_(n,L) by POLYNOM1:def 27;
              then A34: x + (0.Polynom-Ring(n,L)) = -0_(n,L) + 0_(n,L)
                                  by POLYNOM1:def 27
                  .= 0_(n,L) by POLYRED:3
                  .= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 27;
              A35: now assume mg2 - mg1 = 0_(n,L);
                  then -(mg2 + -mg1) = - 0_(n,L) by POLYNOM1:def 23;
                  then -mg2 + -(-mg1) = -0_(n,L) by POLYRED:1;
                  then mg1 + -mg2
                          = -(0.(Polynom-Ring(n,L))) by A34,RLVECT_1:19
                         .= 0.(Polynom-Ring(n,L)) by RLVECT_1:25
                         .= 0_(n,L) by POLYNOM1:def 27;
                  hence contradiction by A22,POLYNOM1:def 23;
                  end;
               (mg2 - mg1) -
              ((mg2-mg1).HT(mg2,T)/HC(g2,T)) * (HT(m2,T) *' g2)
                  = (mg2 - mg1) -
                    ((HC(m2,T)*HC(g2,T))/HC(g2,T)) * (HT(m2,T) *' g2)
                    by A31,TERMORD:32
                 .= (mg2 - mg1) -
                    ((HC(m2,T)*HC(g2,T))*(HC(g2,T)")) * (HT(m2,T) *' g2)
                    by VECTSP_1:def 23
                 .= (mg2 - mg1) -
                    (HC(m2,T)*(HC(g2,T)*(HC(g2,T)"))) * (HT(m2,T) *' g2)
                    by VECTSP_1:def 16
                 .= (mg2 - mg1) -
                    (HC(m2,T)*1_ L) * (HT(m2,T) *' g2) by A20,VECTSP_1:def 22
                 .= (mg2 - mg1) -
                    HC(m2,T) * (HT(m2,T) *' g2) by VECTSP_1:def 19
                 .= (mg2 - mg1) - Monom(HC(m2,T),HT(m2,T)) *' g2 by POLYRED:22
                 .= (mg2 - mg1) - Monom(coefficient(m2),HT(m2,T)) *'g2
                    by TERMORD:23
                 .= (mg2 - mg1) - Monom(coefficient(m2),term(m2)) *'g2
                    by TERMORD:23
                 .= (mg2 - mg1) - mg2 by POLYNOM7:11
                 .= (mg2+-mg1)-mg2 by POLYNOM1:def 23
                 .= (mg2+-mg1)+-mg2 by POLYNOM1:def 23
                 .= (mg2+-mg2)+-mg1 by POLYNOM1:80
                 .= 0_(n,L)+-mg1 by POLYRED:3
                 .= -mg1 by POLYRED:2;
              then mg2-mg1 reduces_to -mg1,g2,HT(mg2,T),T
                 by A16,A32,A33,A35,POLYRED:def 5;
              then mg2-mg1 reduces_to -mg1,g2,T by POLYRED:def 6;
              then mg2-mg1 reduces_to -mg1,P,T by A14,POLYRED:def 7;
              then [mg2-mg1,-mg1] in R by POLYRED:def 13;
              then A36: R reduces mg2-mg1,-mg1 by REWRITE1:16;
               R reduces (-m1)*'g1,0_(n,L) by A11,POLYRED:45;
              then R reduces -mg1,0_(n,L) by POLYRED:6;
              then A37: R reduces mg2-mg1,0_(n,L) by A36,REWRITE1:17;
               -(1_(n,L)) = -(1.L _(n,L)) by POLYNOM7:20
                        .= (-1.L) _(n,L) by Th20;
              then A38: R reduces (-1_(n,L))*'(mg2-mg1),(-1_(n,L))*'0_(n,L)
                        by A37,POLYRED:47;
               (-1_(n,L))*'(mg2-mg1)
                = (-1_(n,L))*'(mg2+-mg1) by POLYNOM1:def 23
               .= (-1_(n,L))*'mg2+(-1_(n,L))*'(-mg1) by POLYNOM1:85
               .= -(1_(n,L)*'mg2)+(-1_(n,L))*'(-mg1) by POLYRED:6
               .= 1_(n,L)*'(-mg2)+(-1_(n,L))*'(-mg1) by POLYRED:6
               .= 1_(n,L)*'(-mg2)+(-(1_(n,L)*'(-mg1))) by POLYRED:6
               .= 1_(n,L)*'(-mg2)+1_(n,L)*'(--mg1) by POLYRED:6
               .= (-mg2)+1_(n,L)*'mg1 by POLYNOM1:89
               .= mg1 + -mg2 by POLYNOM1:89
               .= mg1 - mg2 by POLYNOM1:def 23;
              hence thesis by A21,A38,POLYNOM1:87;
              end;
            hence thesis;
          case A39: HT(mg1,T) = HT(mg2,T);
             (f-mg1).HT(mg1,T) = 0.L by A17,POLYNOM1:def 9;
            then (f+-mg1).HT(mg1,T) = 0.L by POLYNOM1:def 23;
            then f.HT(mg1,T) + (-mg1).HT(mg1,T) = 0.L by POLYNOM1:def 21;
            then f.HT(mg1,T) + -(mg1.HT(mg1,T)) = 0.L by POLYNOM1:def 22;
            then A40: f.HT(mg1,T) = --(mg1.HT(mg1,T)) by RLVECT_1:19;
             (f-mg2).HT(mg2,T) = 0.L by A18,POLYNOM1:def 9;
            then (f+-mg2).HT(mg2,T) = 0.L by POLYNOM1:def 23;
            then f.HT(mg2,T) + (-mg2).HT(mg2,T) = 0.L by POLYNOM1:def 21;
            then f.HT(mg2,T) + -(mg2.HT(mg2,T)) = 0.L by POLYNOM1:def 22;
            then A41: f.HT(mg2,T) = --(mg2.HT(mg2,T)) by RLVECT_1:19;
             HC(mg1,T) = mg1.HT(mg1,T) by TERMORD:def 7
                     .= f.(HT(mg1,T)) by A40,RLVECT_1:30
                     .= mg2.HT(mg2,T) by A39,A41,RLVECT_1:30
                     .= HC(mg2,T) by TERMORD:def 7;
            then HM(mg1,T) = Monom(HC(mg2,T),HT(mg2,T)) by A39,TERMORD:def 8
                          .= HM(mg2,T) by TERMORD:def 8;
            hence thesis by A1,A11,A14,A21,A23;
            end;
        hence thesis;
        end;
        hence thesis;
        end;
    hence thesis;
    end;
  then f2,f1 are_convergent_wrt R by POLYRED:50;
  hence b,c are_convergent_wrt R by A7,A8,REWRITE1:41;
  end;
  hence b,c are_convergent_wrt R;
  end;
then PolyRedRel(P,T) is locally-confluent by REWRITE1:def 24;
hence thesis by GROEB_1:def 3;
end;

definition
::: definition 5.46, p. 211
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),
    p1,p2 be Polynomial of n,L;
func S-Poly(p1,p2,T) -> Polynomial of n,L equals :Def4:
  HC(p2,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p1,T)) *' p1 -
  HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2;
coherence;
end;

Lm2:
for L being add-associative left_zeroed right_zeroed add-cancelable
            right_complementable associative distributive well-unital
            (non empty doubleLoopStr),
    P being Subset of L,
    p being Element of L st p in P
holds p in P-Ideal
proof
let L be add-associative left_zeroed right_zeroed add-cancelable
         associative distributive well-unital right_complementable
         (non empty doubleLoopStr),
    P be Subset of L,
    p be Element of L;
assume A1: p in P;
then reconsider P' = P as non empty Subset of L;
set f = <*p*>;
 now let i be set;
  assume A2: i in dom f;
   dom f = {1} by FINSEQ_1:4,55;
  then i = 1 by A2,TARSKI:def 1;
  then f/.i = f.1 by A2,FINSEQ_4:def 4
           .= p by FINSEQ_1:57
           .= 1_ L * p by VECTSP_1:def 19
           .= 1_ L * p * 1_ L by VECTSP_1:def 13;
  hence ex u,v being Element of L, a being Element of P' st f/.i = u*a*v by A1
;
  end;
then reconsider f as LinearCombination of P' by IDEAL_1:def 9;
 Sum f = p by RLVECT_1:61;
hence thesis by IDEAL_1:60;
end;

Lm3:
for n being Ordinal,
    T being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            unital distributive (non trivial doubleLoopStr),
    p,q being Polynomial of n,L,
    f,g being Element of Polynom-Ring(n,L)
holds (f = p & g = q) implies f - g = p - q
proof
let n be Ordinal,
    T be connected TermOrder of n,
    L be add-associative right_complementable right_zeroed
         unital distributive (non trivial doubleLoopStr),
    p,q be Polynomial of n,L,
    f,g be Element of Polynom-Ring(n,L);
assume A1: f = p & g = q;
reconsider x = -q as Element of Polynom-Ring(n,L)
       by POLYNOM1:def 27;
reconsider x as Element of Polynom-Ring(n,L);
 x + g = -q + q by A1,POLYNOM1:def 27
     .= 0_(n,L) by POLYRED:3
     .= 0.(Polynom-Ring(n,L)) by POLYNOM1:def 27;
then A2: -q = -g by RLVECT_1:19;
thus p - q = p + (-q) by POLYNOM1:def 23
          .= f + (-g) by A1,A2,POLYNOM1:def 27
          .= f - g by RLVECT_1:def 11;
end;

theorem Th22:
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 Abelian (non trivial doubleLoopStr),
    P being Subset of Polynom-Ring(n,L),
    p1,p2 being Polynomial of n,L st p1 in P & p2 in P
holds S-Poly(p1,p2,T) in P-Ideal
proof
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 Abelian (non trivial doubleLoopStr),
    P be Subset of Polynom-Ring(n,L),
    p1,p2 be Polynomial of n,L;
assume A1: p1 in P & p2 in P;
set q = S-Poly(p1,p2,T);
reconsider p1' = p1, p2' = p2 as Element of Polynom-Ring(n,L)
   by POLYNOM1:def 27;
reconsider p1', p2' as Element of Polynom-Ring(n,L);
set q1 = Monom(HC(p2,T),lcm(HT(p1,T),HT(p2,T))/HT(p1,T)),
    q2 = Monom(HC(p1,T),lcm(HT(p1,T),HT(p2,T))/HT(p2,T));
reconsider q1' = q1, q2' = q2 as Element of Polynom-Ring(n,L)
   by POLYNOM1:def 27;
reconsider q1', q2' as Element of Polynom-Ring(n,L);
A2: q = HC(p2,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p1,T)) *' p1 -
       HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2 by Def4
    .= q1 *' p1 - HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2
       by POLYRED:22
    .= q1 *' p1 - q2 *' p2 by POLYRED:22;
 p1' in P-Ideal & p2' in P-Ideal by A1,Lm2;
then q1' * p1' in P-Ideal & q2' * p2' in P-Ideal by IDEAL_1:def 2;
then A3: q1' * p1' - q2' * p2' in P-Ideal by IDEAL_1:16;
 q1 *' p1 = q1' * p1' & q2 *' p2 = q2' * p2' by POLYNOM1:def 27;
hence thesis by A2,A3,Lm3;
end;

theorem
::: exercise 5.47 (i), p. 211
 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),
    p1,p2 being Polynomial of n,L
holds p1 = p2 implies S-Poly(p1,p2,T) = 0_(n,L)
proof
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),
    p1,p2 be Polynomial of n,L;
assume p1 = p2;
then S-Poly(p1,p2,T) =
  HC(p1,T) * (lcm(HT(p1,T),HT(p1,T))/HT(p1,T)) *' p1 -
  HC(p1,T) * (lcm(HT(p1,T),HT(p1,T))/HT(p1,T)) *' p1 by Def4;
hence thesis by POLYNOM1:83;
end;

theorem Th24:
::: exercise 5.47 (i), p. 211
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),
    m1,m2 being Monomial of n,L
holds S-Poly(m1,m2,T) = 0_(n,L)
proof
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),
    m1,m2 be Monomial of n,L;
per cases;
suppose A1: m1 = 0_(n,L);
  A2: HC(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))),T)
        = coefficient(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))))
          by TERMORD:23
       .= HC(0_(n,L),T) by POLYNOM7:9
       .= 0.L by TERMORD:17;
  thus S-Poly(m1,m2,T)
    = HC(m2,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' 0_(n,L) -
      HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 by A1,Def4
   .= Monom(HC(m2,T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))) *' 0_(n,L) -
      HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 by POLYRED:22
   .= 0_(n,L) -
      HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 by POLYNOM1:87
   .= 0_(n,L) -
      Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))) *' m2
      by POLYRED:22
   .= 0_(n,L) - 0_(n,L) *' m2 by A2,TERMORD:17
   .= 0_(n,L) - 0_(n,L) by POLYRED:5
   .= 0_(n,L) by POLYNOM1:83;
suppose A3: m2 = 0_(n,L);
  A4: HC(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))),T)
        = coefficient(Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))))
          by TERMORD:23
       .= HC(0_(n,L),T) by POLYNOM7:9
       .= 0.L by TERMORD:17;
  thus S-Poly(m1,m2,T)
    = HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 -
      HC(m1,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' 0_(n,L) by A3,Def4
   .= HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 -
      Monom(HC(m1,T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))) *' 0_(n,L)
      by POLYRED:22
   .= HC(0_(n,L),T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 -
      0_(n,L) by POLYNOM1:87
   .= Monom(HC(0_(n,L),T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))) *' m1 -
      0_(n,L) by POLYRED:22
   .= 0_(n,L) *' m1 - 0_(n,L) by A4,TERMORD:17
   .= 0_(n,L) - 0_(n,L) by POLYRED:5
   .= 0_(n,L) by POLYNOM1:83;
suppose m1 <> 0_(n,L) & m2 <> 0_(n,L);
then HC(m1,T) <> 0.L & HC(m2,T) <> 0.L by TERMORD:17;
then A5: HC(m1,T) is non-zero & HC(m2,T) is non-zero by RLVECT_1:def 13;
A6: m1 = Monom(coefficient(m1),term(m1)) by POLYNOM7:11
     .= Monom(HC(m1,T),term(m1)) by TERMORD:23
     .= Monom(HC(m1,T),HT(m1,T)) by TERMORD:23;
A7: m2 = Monom(coefficient(m2),term(m2)) by POLYNOM7:11
     .= Monom(HC(m2,T),term(m2)) by TERMORD:23
     .= Monom(HC(m2,T),HT(m2,T)) by TERMORD:23;
A8: HT(m1,T) divides lcm(HT(m1,T),HT(m2,T)) by Th7;
A9: HC(m2,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1
  = Monom(HC(m2,T),(lcm(HT(m1,T),HT(m2,T))/HT(m1,T))) *' m1
    by POLYRED:22
 .= Monom(HC(m2,T)*HC(m1,T),
          (lcm(HT(m1,T),HT(m2,T))/HT(m1,T))+HT(m1,T)) by A5,A6,TERMORD:3
 .= Monom(HC(m2,T)*HC(m1,T),
          lcm(HT(m1,T),HT(m2,T))) by A8,Def1;
A10: HT(m2,T) divides lcm(HT(m1,T),HT(m2,T)) by Th7;
A11: HC(m1,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2
  = Monom(HC(m1,T),(lcm(HT(m1,T),HT(m2,T))/HT(m2,T))) *' m2
    by POLYRED:22
 .= Monom(HC(m2,T)*HC(m1,T),
          (lcm(HT(m1,T),HT(m2,T))/HT(m2,T))+HT(m2,T)) by A5,A7,TERMORD:3
 .= Monom(HC(m2,T)*HC(m1,T),
          lcm(HT(m1,T),HT(m2,T))) by A10,Def1;
thus S-Poly(m1,m2,T)
  = HC(m2,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m1,T)) *' m1 -
    HC(m1,T) * (lcm(HT(m1,T),HT(m2,T))/HT(m2,T)) *' m2 by Def4
 .= 0_(n,L) by A9,A11,POLYNOM1:83;
end;

theorem Th25:
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 S-Poly(p,0_(n,L),T) = 0_(n,L) & S-Poly(0_(n,L),p,T) = 0_(n,L)
proof
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 Polynomial of n,L;
set p2 = 0_(n,L);
thus S-Poly(p,0_(n,L),T)
  = HC(0_(n,L),T) * (lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p -
    HC(p,T) * (lcm(HT(p,T),HT(p2,T))/HT(p2,T)) *' 0_(n,L) by Def4
 .= HC(0_(n,L),T) * (lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p -
    Monom(HC(p,T),lcm(HT(p,T),HT(p2,T))/HT(p2,T)) *' 0_(n,L) by POLYRED:22
 .= HC(0_(n,L),T) * (lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p - 0_(n,L)
    by POLYNOM1:87
 .= 0.L * ((lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p) - 0_(n,L) by TERMORD:17
 .= ((0.L _(n,L)) *' ((lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p)) - 0_(n,L)
    by POLYNOM7:27
 .= (0_(n,L) *' ((lcm(HT(p,T),HT(p2,T))/HT(p,T)) *' p)) - 0_(n,L)
    by POLYNOM7:19
 .= 0_(n,L) - 0_(n,L) by POLYRED:5
 .= 0_(n,L) by POLYRED:4;
thus S-Poly(0_(n,L),p,T)
  = HC(p,T) * (lcm(HT(p2,T),HT(p,T))/HT(p2,T)) *' 0_(n,L) -
    HC(0_(n,L),T) * (lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p by Def4
 .= Monom(HC(p,T),(lcm(HT(p2,T),HT(p,T))/HT(p2,T))) *' 0_(n,L) -
    HC(0_(n,L),T) * (lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p by POLYRED:22
 .= 0_(n,L) - HC(0_(n,L),T) * (lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p
    by POLYNOM1:87
 .= 0_(n,L) - 0.L * ((lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p) by TERMORD:17
 .= 0_(n,L) - ((0.L _(n,L)) *' ((lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p))
    by POLYNOM7:27
 .= 0_(n,L) - (0_(n,L) *' ((lcm(HT(p2,T),HT(p,T))/HT(p,T)) *' p))
    by POLYNOM7:19
 .= 0_(n,L) - 0_(n,L) by POLYRED:5
 .= 0_(n,L) by POLYRED:4;
end;

theorem
::: exercise 5.47 (ii), p. 211
 for n being Ordinal,
    T being admissible connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            commutative associative well-unital distributive
            Field-like (non trivial doubleLoopStr),
    p1,p2 being Polynomial of n,L
holds S-Poly(p1,p2,T) = 0_(n,L) or
      HT(S-Poly(p1,p2,T),T) < lcm(HT(p1,T),HT(p2,T)),T
proof
let n be Ordinal,
    T be admissible connected TermOrder of n,
    L be add-associative right_complementable right_zeroed
         commutative associative well-unital distributive
         Field-like (non trivial doubleLoopStr),
    p1,p2 be Polynomial of n,L;
assume A1: S-Poly(p1,p2,T) <> 0_(n,L);
set sp = S-Poly(p1,p2,T),
    g1 = HC(p2,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p1,T)) *' p1,
    g2 = HC(p1,T) * (lcm(HT(p1,T),HT(p2,T))/HT(p2,T)) *' p2;
per cases;
suppose p1 = 0_(n,L) or p2 = 0_(n,L);
hence thesis by A1,Th25;
suppose A2: p1 <> 0_(n,L) & p2 <> 0_(n,L);
then A3: HC(p1,T) <> 0.L & HC(p2,T) <> 0.L by TERMORD:17;
then A4: HC(p1,T) is non-zero & HC(p2,T) is non-zero by RLVECT_1:def 13;
A5: HT(p1,T) divides lcm(HT(p1,T),HT(p2,T)) by Th7;
A6: HT(p2,T) divides lcm(HT(p1,T),HT(p2,T)) by Th7;
A7: p1 is non-zero & p2 is non-zero by A2,POLYNOM7:def 2;
A8: HT(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))),T)
    = term(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))))
      by TERMORD:23
   .= lcm(HT(p1,T),HT(p2,T))/HT(p1,T) by A4,POLYNOM7:10;
 HC(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))),T)
    = coefficient(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))))
      by TERMORD:23
   .= HC(p2,T) by POLYNOM7:9;
then Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))) <> 0_(n,L)
     by A3,TERMORD:17;
then A9: Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T))) is non-zero
        by POLYNOM7:def 2;
A10: HT(g1,T)
    = HT((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) *' p1,T)
      by POLYRED:22
   .= HT((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))),T) + HT(p1,T)
      by A7,A9,TERMORD:31
   .= lcm(HT(p1,T),HT(p2,T)) by A5,A8,Def1;
A11: HT(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))),T)
    = term(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))))
      by TERMORD:23
   .= lcm(HT(p1,T),HT(p2,T))/HT(p2,T) by A4,POLYNOM7:10;
 HC(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))),T)
    = coefficient(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))))
      by TERMORD:23
   .= HC(p1,T) by POLYNOM7:9;
then Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))) <> 0_(n,L)
     by A3,TERMORD:17;
then A12: Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T))) is non-zero
        by POLYNOM7:def 2;
A13: HT(g2,T)
    = HT((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) *' p2,T)
      by POLYRED:22
   .= HT((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))),T) + HT(p2,T)
      by A7,A12,TERMORD:31
   .= lcm(HT(p1,T),HT(p2,T)) by A6,A11,Def1;
 sp = g1 - g2 by Def4;
then HT(sp,T) <= max(HT(g1,T),HT(g2,T),T), T by GROEB_1:7;
then A14: HT(sp,T) <= lcm(HT(p1,T),HT(p2,T)),T by A10,A13,TERMORD:12;
A15: HC(g1,T)
    = HC((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) *' p1,T)
      by POLYRED:22
   .= HC((Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))),T) * HC(p1,T)
      by A7,A9,TERMORD:32
   .= coefficient(Monom(HC(p2,T),(lcm(HT(p1,T),HT(p2,T))/HT(p1,T)))) * HC(p1,T)
      by TERMORD:23
   .= HC(p1,T) * HC(p2,T) by POLYNOM7:9;
A16: HC(g2,T)
    = HC((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) *' p2,T)
      by POLYRED:22
   .= HC((Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))),T) * HC(p2,T)
      by A7,A12,TERMORD:32
   .= coefficient(Monom(HC(p1,T),(lcm(HT(p1,T),HT(p2,T))/HT(p2,T)))) * HC(p2,T)
      by TERMORD:23
   .= HC(p1,T) * HC(p2,T) by POLYNOM7:9;
 Support sp <> {} by A1,POLYNOM7:1;
then A17: HT(sp,T) in Support sp by TERMORD:def 6;
 sp.(lcm(HT(p1,T),HT(p2,T)))
    = (g1-g2).HT(g2,T) by A13,Def4
   .= (g1+-g2).HT(g2,T) by POLYNOM1:def 23
   .= g1.HT(g2,T) + (-g2).HT(g2,T) by POLYNOM1:def 21
   .= g1.HT(g2,T) + -(g2.HT(g2,T)) by POLYNOM1:def 22
   .= HC(g1,T) + -(g2.HT(g2,T)) by A10,A13,TERMORD:def 7
   .= HC(g1,T) + -HC(g2,T) by TERMORD:def 7
   .= 0.L by A15,A16,RLVECT_1:16;
then not(lcm(HT(p1,T),HT(p2,T)) in Support sp) by POLYNOM1:def 9;
hence HT(S-Poly(p1,p2,T),T) < lcm(HT(p1,T),HT(p2,T)),T by A14,A17,TERMORD:def 3
;
end;

theorem
::: exercise 5.47 (iii), p. 211
 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),
    p1,p2 being non-zero Polynomial of n,L
holds HT(p2,T) divides HT(p1,T) implies
      HC(p2,T) * p1 top_reduces_to S-Poly(p1,p2,T),p2,T
proof
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),
    p1,p2 be non-zero Polynomial of n,L;
assume A1: HT(p2,T) divides HT(p1,T);
A2: p1 <> 0_(n,L) & p2 <> 0_(n,L) by POLYNOM7:def 2;
then Support p1 <> {} by POLYNOM7:1;
then A3: HT(p1,T) in Support p1 by TERMORD:def 6;
set hcp2 = HC(p2,T);
A4: hcp2 <> 0.L by A2,TERMORD:17;
A5: HT(hcp2*p1,T) = HT(p1,T) by POLYRED:21;
consider b being bag of n such that
A6: HT(p1,T) = HT(p2,T) + b by A1,TERMORD:1;
set g = (hcp2*p1) - ((hcp2*p1).HT(p1,T)/HC(p2,T)) * (b *' p2);
A7: Support(p1) c= Support(hcp2*p1) by POLYRED:20;
then hcp2*p1 <> 0_(n,L) by A3,POLYNOM7:1;
then A8: hcp2*p1 reduces_to g,p2,HT(p1,T),T by A2,A3,A6,A7,POLYRED:def 5;
A9: lcm(HT(p1,T),HT(p2,T)) = HT(p1,T) by A1,Th11;
 g = (hcp2*p1) - (hcp2*(p1.HT(p1,T))/HC(p2,T)) * (b *' p2) by POLYNOM7:def 10
 .= (hcp2*p1) - ((hcp2*HC(p1,T))/HC(p2,T)) * (b *' p2) by TERMORD:def 7
 .= (hcp2*p1) - ((hcp2*HC(p1,T))*(HC(p2,T)")) * (b *' p2) by VECTSP_1:def 23
 .= (hcp2*p1) - (HC(p1,T)*(hcp2*(HC(p2,T)"))) * (b *' p2) by VECTSP_1:def 16
 .= (hcp2*p1) - (HC(p1,T)*1_ L) * (b *' p2) by A4,VECTSP_1:def 22
 .= (hcp2*p1) - HC(p1,T) * (b *' p2) by VECTSP_1:def 13
 .= HC(p2,T) * (EmptyBag n) *' p1 - HC(p1,T) * (b *' p2) by POLYRED:17
 .= HC(p2,T) * (HT(p1,T)/HT(p1,T)) *' p1 - HC(p1,T) * (b *' p2) by Th10
 .= HC(p2,T) * (HT(p1,T)/HT(p1,T)) *' p1 -
    HC(p1,T) * (HT(p1,T)/HT(p2,T)) *' p2 by A1,A6,Def1
 .= S-Poly(p1,p2,T) by A9,Def4;
hence thesis by A5,A8,POLYRED:def 10;
end;

theorem
::: theorem 5.48 (i) ==> (ii), p. 211
 for n being Nat,
    T being connected admissible TermOrder of n,
    L being add-associative right_complementable right_zeroed
            commutative associative well-unital distributive Abelian
            Field-like non degenerated (non empty doubleLoopStr),
    G being Subset of Polynom-Ring(n,L)
holds G is_Groebner_basis_wrt T
implies (for g1,g2,h being Polynomial of n,L
             st g1 in G & g2 in G &
                h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T)
         holds h = 0_(n,L))
proof
let n be Nat,
    T be connected admissible TermOrder of n,
    L be add-associative right_complementable right_zeroed
         commutative associative well-unital distributive Abelian
         Field-like non degenerated (non empty doubleLoopStr),
    G be Subset of Polynom-Ring(n,L);
assume A1: G is_Groebner_basis_wrt T;
set R = PolyRedRel(G,T);
per cases;
suppose G = {};
hence thesis;
suppose G <> {};
then reconsider G as non empty Subset of Polynom-Ring(n,L);
 R is locally-confluent by A1,GROEB_1:def 3;
then R is confluent by GROEB_1:12;
then A2: R is with_UN_property by GROEB_1:13;
then A3: R is with_Church-Rosser_property by GROEB_1:14;
 now let g1,g2,h being Polynomial of n,L;
  assume A4: g1 in G & g2 in G &
            h is_a_normal_form_of S-Poly(g1,g2,T),R;
  then S-Poly(g1,g2,T) in G-Ideal by Th22;
  then A5: R reduces S-Poly(g1,g2,T),0_(n,L) by A3,GROEB_1:15;
  A6: now assume not(0_(n,L) is_a_normal_form_wrt R);
     then consider b being set such that
     A7: [0_(n,L),b] in R by REWRITE1:def 5;
     consider f1,f2 being set such that
     A8: f1 in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
         f2 in the carrier of Polynom-Ring(n,L) &
         [0_(n,L),b] = [f1,f2] by A7,ZFMISC_1:def 2;
     A9: f1 in (the carrier of Polynom-Ring(n,L)) &
         not(f1 in {0_(n,L)}) by A8,XBOOLE_0:def 4;
      f1 = [0_(n,L),b]`1 by A8,MCART_1:def 1 .= 0_(n,L) by MCART_1:def 1;
     hence contradiction by A9,TARSKI:def 1;
     end;
  A10: h is_a_normal_form_wrt R & R reduces S-Poly(g1,g2,T),h
     by A4,REWRITE1:def 6;
  then S-Poly(g1,g2,T),0_(n,L) are_convertible_wrt R &
       h,S-Poly(g1,g2,T) are_convertible_wrt R by A5,REWRITE1:26;
  then h,0_(n,L) are_convertible_wrt R by REWRITE1:31;
  hence h = 0_(n,L) by A2,A6,A10,REWRITE1:def 19;
  end;
hence thesis;
end;

theorem
::: theorem 5.48 (ii) ==> (iii), p. 211
 for n being Nat,
    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),
    G being Subset of Polynom-Ring(n,L)
holds (for g1,g2,h being Polynomial of n,L
         st g1 in G & g2 in G &
            h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T)
       holds h = 0_(n,L))
implies (for g1,g2 being Polynomial of n,L st g1 in G & g2 in G
         holds PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L))
proof
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),
    G be Subset of Polynom-Ring(n,L);
assume A1: for g1,g2,h being Polynomial of n,L
         st g1 in G & g2 in G &
            h is_a_normal_form_of S-Poly(g1,g2,T),PolyRedRel(G,T)
       holds h = 0_(n,L);
set R = PolyRedRel(G,T);
 now let g1,g2 be Polynomial of n,L;
  assume A2: g1 in G & g2 in G;
   now per cases;
  case S-Poly(g1,g2,T) in field R;
    hence S-Poly(g1,g2,T) has_a_normal_form_wrt R by REWRITE1:def 14;
  case not(S-Poly(g1,g2,T) in field R);
    hence S-Poly(g1,g2,T) has_a_normal_form_wrt R by REWRITE1:47;
    end;
  then consider q being set such that
  A3: q is_a_normal_form_of S-Poly(g1,g2,T),R by REWRITE1:def 11;
   q is_a_normal_form_wrt R & R reduces S-Poly(g1,g2,T),q
     by A3,REWRITE1:def 6;
  then reconsider q as Polynomial of n,L by Lm1;
   q = 0_(n,L) by A1,A2,A3;
  hence R reduces S-Poly(g1,g2,T),0_(n,L) by A3,REWRITE1:def 6;
  end;
hence thesis;
end;

theorem Th30:
::: theorem 5.48 (iii) ==> (i), p. 211
for n being Nat,
    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),
    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
       holds PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L))
implies G is_Groebner_basis_wrt T
proof
let n be Nat,
    T be admissible connected TermOrder of n,
    L be add-associative right_complementable right_zeroed
         commutative associative well-unital distributive
         Abelian Field-like non degenerated (non empty doubleLoopStr),
    G be Subset of Polynom-Ring(n,L);
assume A1: not(0_(n,L) in G);
assume A2: for g1,g2 being Polynomial of n,L st g1 in G & g2 in G
           holds PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L);
 now let g1,g2 be Polynomial of n,L;
  assume A3: g1 <> g2 & g1 in G & g2 in G;
  thus for m1,m2 being Monomial of n,L st HM(m1 *'g1,T) = HM(m2 *'g2,T)
       holds PolyRedRel(G,T) reduces m1 *' g1 - m2 *' g2, 0_(n,L)
    proof
    let m1,m2 be Monomial of n,L;
    assume A4: HM(m1 *'g1,T) = HM(m2 *'g2,T);
    set t1 = HT(g1,T), t2 = HT(g2,T);
    set a1 = HC(g1,T), a2 = HC(g2,T);
    set b1 = coefficient(m1), b2 = coefficient(m2);
    set u1 = term(m1), u2 = term(m2);
    A5: a1 <> 0.L & a2 <> 0.L by A1,A3,TERMORD:17;
    then reconsider a1,a2 as non-zero Element of L by RLVECT_1:def 13;
    reconsider g1,g2 as non-zero Polynomial of n,L by A1,A3,POLYNOM7:def 2;
    A6: HC(m1*'g1,T) = coefficient(HM(m1*'g1,T)) by TERMORD:22
                    .= HC(m2*'g2,T) by A4,TERMORD:22;
     now per cases;
    case A7: b1 = 0.L or b2 = 0.L;
       now per cases by A7;
      case b1 = 0.L;
        then HC(m1,T) = 0.L by TERMORD:23;
        then m1 = 0_(n,L) by TERMORD:17;
        then A8: m1 *' g1 = 0_(n,L) by POLYRED:5;
        then HC(m2*'g2,T) = 0.L by A6,TERMORD:17;
        then m2 *' g2 = 0_(n,L) by TERMORD:17;
        then m1 *' g1 - m2 *' g2 = 0_(n,L) by A8,POLYRED:4;
        hence thesis by REWRITE1:13;
      case b2 = 0.L;
        then HC(m2,T) = 0.L by TERMORD:23;
        then m2 = 0_(n,L) by TERMORD:17;
        then A9: m2 *' g2 = 0_(n,L) by POLYRED:5;
        then HC(m1*'g1,T) = 0.L by A6,TERMORD:17;
        then m1 *' g1 = 0_(n,L) by TERMORD:17;
        then m1 *' g1 - m2 *' g2 = 0_(n,L) by A9,POLYRED:4;
        hence thesis by REWRITE1:13;
        end;
      hence thesis;
    case A10: b1 <> 0.L & b2 <> 0.L;
      then reconsider b1,b2 as non-zero Element of L by RLVECT_1:def 13;
       HC(m1,T) <> 0.L & HC(m2,T) <> 0.L by A10,TERMORD:23;
      then m1 <> 0_(n,L) & m2 <> 0_(n,L) by TERMORD:17;
      then reconsider m1,m2 as non-zero Monomial of n,L by POLYNOM7:def 2;
      A11:  Monom(b1*a1,u1+t1)
         = Monom(b1,u1) *' Monom(a1,t1) by TERMORD:3
        .= m1 *' Monom(a1,t1) by POLYNOM7:11
        .= HM(m1,T) *' Monom(a1,t1) by TERMORD:23
        .= HM(m1,T) *' HM(g1,T) by TERMORD:def 8
        .= HM(m2*'g2,T) by A4,TERMORD:33
        .= HM(m2,T) *' HM(g2,T) by TERMORD:33
        .= HM(m2,T) *' Monom(a2,t2) by TERMORD:def 8
        .= m2 *' Monom(a2,t2) by TERMORD:23
        .= Monom(b2,u2) *' Monom(a2,t2) by POLYNOM7:11
        .= Monom(b2*a2,u2+t2) by TERMORD:3;
       b1 * a1 <> 0.L & b2 * a2 <> 0.L by A5,A10,VECTSP_2:def 5;
      then A12: b1 * a1 is non-zero & b2 * a2 is non-zero by RLVECT_1:def 13;
      then A13: u1 + t1 = term(Monom(b2*a2,u2+t2)) by A11,POLYNOM7:10
                      .= u2 + t2 by A12,POLYNOM7:10;
       t1 divides lcm(t1,t2) by Th7;
      then consider s1 being bag of n such that
      A14: t1 + s1 = lcm(t1,t2) by TERMORD:1;
       t2 divides lcm(t1,t2) by Th7;
      then consider s2 being bag of n such that
      A15: t2 + s2 = lcm(t1,t2) by TERMORD:1;
       t1 divides u1 + t1 & t2 divides u1 + t1 by A13,TERMORD:1;
      then lcm(t1,t2) divides u1 + t1 by Th8;
      then consider v being bag of n such that
      A16: u1 + t1 = lcm(t1,t2) + v by TERMORD:1;
       u1 + t1 = (v + s1) + t1 by A14,A16,POLYNOM1:39;
      then A17: u1 = ((v + s1) + t1) -' t1 by POLYNOM1:52
                 .= v + s1 by POLYNOM1:52;
       u2 + t2 = (v + s2) + t2 by A13,A15,A16,POLYNOM1:39;
      then A18: u2 = ((v + s2) + t2) -' t2 by POLYNOM1:52
                 .= v + s2 by POLYNOM1:52;
       b1*a1 = coefficient(Monom(b2*a2,u2+t2)) by A11,POLYNOM7:9
           .= b2 * a2 by POLYNOM7:9;
      then (b1 * a1) / a2 = (b2 * a2) * a2" by VECTSP_1:def 23
                         .= b2 * (a2 * a2") by VECTSP_1:def 16
                         .= b2 * 1_ L by A5,VECTSP_1:def 22;
      then A19: b2 / a1 = ((b1 * a1) / a2) / a1 by VECTSP_2:def 2
                      .= ((b1 * a1) * a2") / a1 by VECTSP_1:def 23
                      .= ((b1 * a1) * a2") * a1" by VECTSP_1:def 23
                      .= ((b1 * a2") * a1) * a1" by VECTSP_1:def 16
                      .= (b1 * a2") * (a1 * a1") by VECTSP_1:def 16
                      .= (b1 * a2") * 1_ L by A5,VECTSP_1:def 22
                      .= b1 * a2" by VECTSP_2:def 2
                      .= b1 / a2 by VECTSP_1:def 23;
       HT(g1,T) divides lcm(HT(g1,T),HT(g2,T)) by Th7;
      then A20: s1 = lcm(HT(g1,T),HT(g2,T))/HT(g1,T) by A14,Def1;
       HT(g2,T) divides lcm(HT(g1,T),HT(g2,T)) by Th7;
      then A21: s2 = lcm(HT(g1,T),HT(g2,T))/HT(g2,T) by A15,Def1;
      A22: (b1/a2)*a2 = (b1*a2")*a2 by VECTSP_1:def 23
                    .= b1*(a2"*a2) by VECTSP_1:def 16
                    .= b1*1_ L by A5,VECTSP_1:def 22;
      A23: (b2/a1)*a1 = (b2*a1")*a1 by VECTSP_1:def 23
                    .= b2*(a1"*a1) by VECTSP_1:def 16
                    .= b2*1_ L by A5,VECTSP_1:def 22
                    .= b2 by VECTSP_2:def 2;
      A24: m1 *' g1 - m2 *' g2
        = Monom(b1,u1) *' g1 - m2 *' g2 by POLYNOM7:11
       .= Monom(b1,u1) *' g1 - Monom(b2,u2) *' g2 by POLYNOM7:11
       .= b1 * ((v+s1) *' g1) - Monom(b2,v+s2) *' g2 by A17,A18,POLYRED:22
       .= b1 * (v *' (s1 *' g1)) - Monom(b2,v+s2) *' g2 by POLYRED:18
       .= b1 * (v *' (s1 *' g1)) - b2 * ((v+s2) *' g2) by POLYRED:22
       .= b1 * (v *' (s1 *' g1)) - b2 * (v *' (s2 *' g2)) by POLYRED:18
       .= b1 * (v *' (s1 *' g1)) + -(b2 * (v *' (s2 *' g2))) by POLYNOM1:def 23
       .= b1 * (v *' (s1 *' g1)) + b2 * (-(v *' (s2 *' g2))) by POLYRED:9
       .= ((b1/a2) * a2) * (v*'(s1*'g1)) + ((b2/a1) * a1) * (-(v*'(s2*'g2)))
          by A22,A23,VECTSP_2:def 2
       .= ((b1/a2) * a2) * (v*'(s1*'g1)) + ((b2/a1) * a1) * (v*'(-(s2*'g2)))
          by Th17
       .= ((b1/a2) * a2) * (v*'(s1*'g1)) + (b1/a2) * (a1 * (v*'-(s2*'g2)))
          by A19,POLYRED:11
       .= (b1/a2) * (a2 * (v*'(s1*'g1))) + (b1/a2) * (a1 * (v*'-(s2*'g2)))
          by POLYRED:11
       .= (b1/a2) * (a2 * (v*'(s1*'g1)) + a1 * (v*'-(s2*'g2))) by Th19
       .= (b1/a2) * (a2 * (v*'(s1*'g1)) + v *' (a1*(-(s2*'g2)))) by Th18
       .= (b1/a2) * (a2 * (v*'(s1*'g1)) + v *' (-(a1*(s2*'g2)))) by POLYRED:9
       .= (b1/a2) * (v *' (a2*(s1*'g1)) + v *' (-(a1*(s2*'g2)))) by Th18
       .= (b1/a2) * (v *' (a2*(s1*'g1) + (-(a1*(s2*'g2))))) by Th16
       .= (b1/a2) * (v *' (a2*(s1*'g1) - a1*(s2*'g2))) by POLYNOM1:def 23
       .= (b1/a2) * v *' S-Poly(g1,g2,T) by A20,A21,Def4
       .= Monom(b1/a2,v) *' S-Poly(g1,g2,T) by POLYRED:22;
       PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L) by A2,A3;
      hence thesis by A24,POLYRED:48;
      end;
    hence thesis;
    end;
  end;
hence thesis by A1,Th21;
end;

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 S-Poly(P,T) -> Subset of Polynom-Ring(n,L) equals :Def5:
  { S-Poly(p1,p2,T) where p1,p2 is Polynomial of n,L :
                                            p1 in P & p2 in P };
coherence
 proof
 set M = {S-Poly(p1,p2,T) where p1,p2 is Polynomial of n,L :
                                            p1 in P & p2 in P};
  now let u be set;
   assume u in M;
   then consider p1,p2 being Polynomial of n,L such that
   A1: u = S-Poly(p1,p2,T) & p1 in P & p2 in P;
   thus u in the carrier of Polynom-Ring(n,L) by A1,POLYNOM1:def 27;
   end;
 then M c= the carrier of Polynom-Ring(n,L) by TARSKI:def 3;
 hence thesis;
 end;
end;

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 finite Subset of Polynom-Ring(n,L);
cluster S-Poly(P,T) -> finite;
coherence
 proof
 defpred P[set,set] means
    ex p1,p2 being Polynomial of n,L
    st p1 = $1`1 & $1`2 = p2 &
       p1 in P & p2 in P & $2 = S-Poly(p1,p2,T);
 A1: for x,y1,y2 being set st x in [:P,P:] & P[x,y1] & P[x,y2]
     holds y1 = y2;
 A2: for x being set st x in [:P,P:] ex y being set st P[x,y]
       proof
       let x be set;
       assume x in [:P,P:];
       then consider p1,p2 being set such that
       A3: p1 in P & p2 in P & [p1,p2] = x by ZFMISC_1:def 2;
       reconsider p1,p2 as Polynomial of n,L by A3,POLYNOM1:def 27;
       take S-Poly(p1,p2,T);
       take p1,p2;
       thus x`1 = p1 by A3,MCART_1:def 1;
       thus x`2 = p2 by A3,MCART_1:def 2;
       thus thesis by A3;
       end;
 consider f being Function such that
 A4: dom f = [:P,P:] & for x being set st x in [:P,P:] holds P[x,f.x]
     from FuncEx(A1,A2);
 A5: now let v be set;
     assume v in rng f;
     then consider u being set such that
     A6: u in dom f & v = f.u by FUNCT_1:def 5;
     consider p1,p2 being Polynomial of n,L such that
     A7: p1 = u`1 & u`2 = p2 &
          p1 in P & p2 in P & f.u = S-Poly(p1,p2,T) by A4,A6;
      f.u in {S-Poly(p,q,T) where p,q is Polynomial of n,L :
                                            p in P & q in P} by A7;
     hence v in S-Poly(P,T) by A6,Def5;
     end;
  now let v be set;
   assume v in S-Poly(P,T);
   then v in {S-Poly(p1,p2,T) where p1,p2 is Polynomial of n,L :
                                          p1 in P & p2 in P} by Def5;
   then consider p1,p2 being Polynomial of n,L such that
   A8: v = S-Poly(p1,p2,T) & p1 in P & p2 in P;
   A9: [p1,p2] in dom f by A4,A8,ZFMISC_1:def 2;
   then consider p1',p2' being Polynomial of n,L such that
   A10: [p1,p2]`1 = p1' & [p1,p2]`2 = p2' & p1' in P & p2' in P &
        f.[p1,p2] = S-Poly(p1',p2',T) by A4;
    p1 = p1' & p2 = p2' by A10,MCART_1:def 1,def 2;
   hence v in rng f by A8,A9,A10,FUNCT_1:def 5;
   end;
 then rng f = S-Poly(P,T) by A5,TARSKI:2;
 hence thesis by A4,FINSET_1:26;
 end;
end;

theorem
::: corollary 5.49, p. 212
 for n being Nat,
    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),
    G being Subset of Polynom-Ring(n,L)
     st not(0_(n,L) in G) &
        for g being Polynomial of n,L st g in G holds g is Monomial of n,L
holds G is_Groebner_basis_wrt T
proof
let n being Nat,
    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),
    G being Subset of Polynom-Ring(n,L);
assume A1: not(0_(n,L) in G) & for g being Polynomial of n,L
                               st g in G holds g is Monomial of n,L;
 now let g1,g2 be Polynomial of n,L;
  assume g1 in G & g2 in G;
  then g1 is Monomial of n,L & g2 is Monomial of n,L by A1;
  then S-Poly(g1,g2,T) = 0_(n,L) by Th24;
  hence PolyRedRel(G,T) reduces S-Poly(g1,g2,T),0_(n,L) by REWRITE1:13;
  end;
hence thesis by A1,Th30;
end;

begin :: Standard Representations

theorem
 for L being non empty multLoopStr,
    P being non empty Subset of L,
    A being LeftLinearCombination of P,
    i being Nat
holds A|i is LeftLinearCombination of P
proof
let L be non empty multLoopStr,
    P be non empty Subset of L,
    A be LeftLinearCombination of P,
    j be Nat;
set C = A|(Seg j);
reconsider C as FinSequence of the carrier of L by FINSEQ_1:23;
 now let i be set;
  assume A1: i in dom C;
  then A2: dom C c= dom A & C.i = A.i by FUNCT_1:70,76;
  then A3: C/.i = A.i by A1,FINSEQ_4:def 4 .= A/.i by A1,A2,FINSEQ_4:def 4;
  consider u being Element of L, a being Element of P such that
  A4: A/.i = u * a by A1,A2,IDEAL_1:def 10;
  thus ex u being Element of L, a being Element of P
       st C/.i = u * a by A3,A4;
  end;
then C is LeftLinearCombination of P by IDEAL_1:def 10;
hence thesis by TOPREAL1:def 1;
end;

theorem
 for L being non empty multLoopStr,
    P being non empty Subset of L,
    A being LeftLinearCombination of P,
    i being Nat
holds A/^i is LeftLinearCombination of P
proof
let L be non empty multLoopStr,
    P be non empty Subset of L,
    A be LeftLinearCombination of P,
    j be Nat;
set C = A/^j;
reconsider C as FinSequence of the carrier of L;
 now per cases;
case A1: j <= len A;
  then reconsider m = len A - j as Nat by INT_1:18;
   now let i be set;
    assume A2: i in dom C;
    then reconsider k = i as Nat;
    A3: C/.k = A/.(j+k) by A2,FINSEQ_5:30;
     dom C = Seg(len C) by FINSEQ_1:def 3
         .= Seg(m) by A1,RFINSEQ:def 2;
    then A4: 1 <= k & k <= len A - j by A2,FINSEQ_1:3;
    then k + j <= (len A - j) + j by AXIOMS:24;
    then k + j <= (len A + -j) + j by XCMPLX_0:def 8;
    then k + j <= len A + (-j + j) by XCMPLX_1:1;
    then k + j <= len A + (j - j) by XCMPLX_0:def 8;
    then A5: k + j <= len A + 0 by XCMPLX_1:14;
     k <= k + j by NAT_1:29;
    then 1 <= k + j by A4,AXIOMS:22;
    then j + k in Seg(len A) by A5,FINSEQ_1:3;
    then j + k in dom A by FINSEQ_1:def 3;
    then consider u being Element of L, a being Element of P such that
    A6: A/.(j+k) = u * a by IDEAL_1:def 10;
    thus ex u being Element of L, a being Element of P
          st C/.i = u * a by A3,A6;
    end;
  hence thesis by IDEAL_1:def 10;
case not(j <= len A);
  then C = <*>(the carrier of L) by RFINSEQ:def 2;
  then for i being set st i in dom C
    ex u being Element of L, a being Element of P
          st C/.i = u * a by FINSEQ_1:26;
  hence thesis by IDEAL_1:def 10;
  end;
hence thesis;
end;

theorem
 for L being non empty multLoopStr,
    P,Q being non empty Subset of L,
    A being LeftLinearCombination of P
holds P c= Q implies A is LeftLinearCombination of Q
proof
let L be non empty multLoopStr,
    P,Q be non empty Subset of L,
    A be LeftLinearCombination of P;
assume A1: P c= Q;
 now let i be set;
  assume i in dom A;
  then consider u being Element of L,
                a being Element of P such that
  A2: A/.i = u*a by IDEAL_1:def 10;
   a in P;
  hence ex u being Element of L,
           a being Element of Q st A/.i = u*a by A1,A2;
  end;
hence thesis by IDEAL_1:def 10;
end;

definition
let n be Ordinal,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    P be non empty Subset of Polynom-Ring(n,L),
    A,B be LeftLinearCombination of P;
redefine func A^B -> LeftLinearCombination of P;
coherence
 proof
  A^B is LeftLinearCombination of P \/ P;
 hence thesis;
 end;
end;

definition
let n be Ordinal,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A be LeftLinearCombination of P;
pred A is_MonomialRepresentation_of f means :Def6:
  Sum A = f &
  for i being Nat st i in dom A
  ex m being Monomial of n,L,
     p being Polynomial of n,L st p in P & A/.i = m *' p;
end;

theorem
 for n being Ordinal,
    L being right_zeroed add-associative right_complementable
            unital distributive non trivial (non empty doubleLoopStr),
    f being Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L),
    A being LeftLinearCombination of P st A is_MonomialRepresentation_of f
holds Support f c= union { Support(m*'p) where m is Monomial of n,L,
                                               p is Polynomial of n,L :
                               ex i being Nat st i in dom A & A/.i = m*'p }
proof
let n be Ordinal,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A be LeftLinearCombination of P;
assume A1: A is_MonomialRepresentation_of f;
defpred P[Nat] means
  for f being Polynomial of n,L,
      A being LeftLinearCombination of P
  st A is_MonomialRepresentation_of f & len A = $1
  holds Support f c= union {Support(m*'p) where m is Monomial of n,L,
                                                p is Polynomial of n,L :
                                   ex i being Nat st i in dom A & A/.i = m*'p};
A2: P[0]
    proof let f be Polynomial of n,L,
            A be LeftLinearCombination of P;
    assume A3: A is_MonomialRepresentation_of f & len A = 0;
    then A = <*>(the carrier of Polynom-Ring(n,L)) by FINSEQ_1:32;
    then Sum A = 0.(Polynom-Ring(n,L)) by RLVECT_1:60;
    then f = 0.(Polynom-Ring(n,L)) by A3,Def6;
    then f = 0_(n,L) by POLYNOM1:def 27;
    then Support f = {} by POLYNOM7:1;
    hence Support f c= union {Support(m*'p) where m is Monomial of n,L,
                                                  p is Polynomial of n,L :
              ex i being Nat st i in dom A & A/.i = m*'p} by XBOOLE_1:2;
    end;
A4: now let k be Nat;
    assume A5: P[k];
     for f being Polynomial of n,L,
        A being LeftLinearCombination of P
        st A is_MonomialRepresentation_of f & len A = k+1
    holds Support f c= union {Support(m*'p) where m is Monomial of n,L,
                                                p is Polynomial of n,L :
                                   ex i being Nat st i in dom A & A/.i = m*'p}
      proof
      let f be Polynomial of n,L,
          A be LeftLinearCombination of P;
      assume A6: A is_MonomialRepresentation_of f & len A = k+1;
      then A7: Sum A = f &
                for i being Nat st i in dom A
                ex m being Monomial of n,L,
                   p being Polynomial of n,L st p in P & A/.i = m*'p by Def6;
       A <> <*>(the carrier of Polynom-Ring(n,L)) by A6,FINSEQ_1:32;
      then reconsider A as non empty LeftLinearCombination of P;
      consider A' being LeftLinearCombination of P,
               e being Element of Polynom-Ring(n,L) such that
      A8: A = A'^<* e *> & <*e*> is LeftLinearCombination of P by IDEAL_1:33;
      A9: len A = len A' + len<*e*> by A8,FINSEQ_1:35
               .= len A' + 1 by FINSEQ_1:56;
      then A10: len A' = k by A6,XCMPLX_1:2;
      reconsider g = Sum A' as Polynomial of n,L by POLYNOM1:def 27;
      A11: dom A = Seg(k+1) by A6,FINSEQ_1:def 3;
      A12: dom A' = Seg k by A10,FINSEQ_1:def 3;
       k <= k + 1 by NAT_1:29;
      then A13: dom A' c= dom A by A11,A12,FINSEQ_1:7;
       now let i being Nat;
        assume A14: i in dom A';
        then A/.i = A.i by A13,FINSEQ_4:def 4
                 .= A'.i by A8,A14,FINSEQ_1:def 7 .= A'/.i by A14,FINSEQ_4:def
4;
        hence ex m being Monomial of n,L,
                 p being Polynomial of n,L st p in P & A'/.i = m*'p
              by A6,A13,A14,Def6;
        end;
      then A' is_MonomialRepresentation_of g by Def6;
      then A15: Support g c= union {Support(m*'p) where m is Monomial of n,L,
                                                   p is Polynomial of n,L :
                       ex i being Nat st i in dom A' & A'/.i = m*'p} by A5,A10;
      reconsider ep = Sum(<*e*>) as Polynomial of n,L by POLYNOM1:def 27;
       f = Sum A' + Sum(<*e*>) by A7,A8,RLVECT_1:58
       .= g + ep by POLYNOM1:def 27;
      then A16: Support f c= Support g \/ Support ep by POLYNOM1:79;
       now let x be set;
        assume A17: x in Support f;
        then reconsider u = x as Element of Bags n;
         now per cases by A16,A17,XBOOLE_0:def 2;
        case u in Support g;
          then consider Y being set such that
          A18: u in Y & Y in {Support(m*'p) where m is Monomial of n,L,
                                               p is Polynomial of n,L :
              ex i being Nat st i in dom A' & A'/.i = m*'p} by A15,TARSKI:def 4
;
          consider m' being Monomial of n,L,
                   p' being Polynomial of n,L such that
          A19: Y = Support(m'*'p') &
              ex i being Nat st i in dom A' & A'/.i = m'*'p' by A18;
          consider i being Nat such that
          A20: i in dom A' & A'/.i = m'*'p' by A19;
           A/.i = A.i by A13,A20,FINSEQ_4:def 4
              .= A'.i by A8,A20,FINSEQ_1:def 7
              .= A'/.i by A20,FINSEQ_4:def 4;
          then Y in {Support(m*'p) where m is Monomial of n,L,
                                           p is Polynomial of n,L :
              ex i being Nat st i in dom A & A/.i = m*'p} by A13,A19,A20;
          hence u in union {Support(m*'p) where m is Monomial of n,L,
                                           p is Polynomial of n,L :
              ex i being Nat st i in dom A & A/.i = m*'p} by A18,TARSKI:def 4;
        case A21: u in Support ep;
          A22: A.(len A) = e by A8,A9,FINSEQ_1:59;
          A23: dom A = Seg(len A) by FINSEQ_1:def 3;
           1 <= len A by A6,NAT_1:29;
          then A24: len A in Seg(len A) by FINSEQ_1:3;
          then A25: len A in dom A by FINSEQ_1:def 3;
          A26: ex m' being Monomial of n,L, p' being Polynomial of n,L
               st p' in P & A/.(len A) = m' *' p' by A6,A23,A24,Def6;
          A27: A/.(len A) = A.(len A) by A25,FINSEQ_4:def 4;
           e = Sum(<*e*>) by RLVECT_1:61;
          then Support ep in {Support(m*'p) where m is Monomial of n,L,
                                           p is Polynomial of n,L :
                 ex i being Nat st i in dom A & A/.i = m*'p} by A22,A25,A26,A27
;
          hence u in union {Support(m*'p) where m is Monomial of n,L,
                                           p is Polynomial of n,L :
              ex i being Nat st i in dom A & A/.i = m*'p}
            by A21,TARSKI:def 4;
          end;
        hence x in union {Support(m*'p) where m is Monomial of n,L,
                                              p is Polynomial of n,L :
                                   ex i being Nat st i in dom A & A/.i = m*'p};
        end;
      hence thesis by TARSKI:def 3;
      end;
    hence P[k+1];
    end;
A28: for k being Nat holds P[k] from Ind(A2,A4);
consider n being Nat such that A29: len A = n;
thus thesis by A1,A28,A29;
end;

theorem
 for n being Ordinal,
    L being right_zeroed add-associative right_complementable
            unital distributive non trivial (non empty doubleLoopStr),
    f,g being Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L),
    A,B being LeftLinearCombination of P
     st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g
holds (A^B) is_MonomialRepresentation_of f+g
proof
let n be Ordinal,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f,g be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A,B be LeftLinearCombination of P;
assume A1: A is_MonomialRepresentation_of f &
          B is_MonomialRepresentation_of g;
reconsider f' = f, g' = g as Element of Polynom-Ring(n,L)
  by POLYNOM1:def 27;
reconsider f',g' as Element of Polynom-Ring(n,L);
A2: Sum(A^B) = Sum A + Sum B by RLVECT_1:58
           .= f' + Sum B by A1,Def6
           .= f' + g' by A1,Def6
           .= f + g by POLYNOM1:def 27;
 now let i be Nat;
  assume A3: i in dom(A^B);
   now per cases by A3,FINSEQ_1:38;
  case A4: i in dom A;
     dom A c= dom(A^B) by FINSEQ_1:39;
    then (A^B)/.i = (A^B).i by A4,FINSEQ_4:def 4
                 .= A.i by A4,FINSEQ_1:def 7
                 .= A/.i by A4,FINSEQ_4:def 4;
    hence ex m being Monomial of n,L,
             p being Polynomial of n,L st p in P & (A^B)/.i = m *' p
          by A1,A4,Def6;
  case ex k being Nat st k in dom B & i = len A + k;
    then consider k being Nat such that
    A5: k in dom B & i = len A + k;
     i in dom(A^B) by A5,FINSEQ_1:41;
    then (A^B)/.i = (A^B).i by FINSEQ_4:def 4
                 .= B.k by A5,FINSEQ_1:def 7
                 .= B/.k by A5,FINSEQ_4:def 4;
    hence ex m being Monomial of n,L,
             p being Polynomial of n,L st p in P & (A^B)/.i = m *' p
          by A1,A5,Def6;
    end;
  hence ex m being Monomial of n,L,
           p being Polynomial of n,L st p in P & (A^B)/.i = m *' p;
  end;
hence thesis by A2,Def6;
end;

Lm4:
for n being Ordinal,
    T being connected TermOrder of n,
    L being right_zeroed add-associative right_complementable
            unital distributive non trivial (non empty doubleLoopStr),
    f being Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L),
    A being LeftLinearCombination of P
      st A is_MonomialRepresentation_of f
for b being bag of n
holds (for i being Nat st i in dom A
       for m being Monomial of n,L, p being Polynomial of n,L
       st A.i = m *' p & p in P holds (m*'p).b = 0.L)
implies f.b = 0.L
proof
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A be LeftLinearCombination of P;
assume A1: A is_MonomialRepresentation_of f;
let b be bag of n;
assume A2: for i being Nat st i in dom A
          for m being Monomial of n,L, p being Polynomial of n,L
          st A.i = m *' p & p in P holds (m*'p).b = 0.L;
A3: Sum A = f by A1,Def6;
defpred P[Nat] means
  for f being Polynomial of n,L,
      A being LeftLinearCombination of P
  st A is_MonomialRepresentation_of f & f = Sum(A) & len A = $1
  holds (for i being Nat st i in dom A
         for m being Monomial of n,L, p being Polynomial of n,L
         st A.i = m*'p & p in P holds (m*'p).b = 0.L) implies f.b = 0.L;
A4: P[0]
    proof
    let f be Polynomial of n,L,
        A be LeftLinearCombination of P;
    assume A5: A is_MonomialRepresentation_of f &
           f = Sum(A) & len A = 0;
    assume for i being Nat st i in dom A
           for m being Monomial of n,L, p being Polynomial of n,L
           st A.i = m*'p & p in P holds (m*'p).b = 0.L;
     f = Sum(<*>(the carrier of Polynom-Ring(n,L))) by A5,FINSEQ_1:32
     .= 0.(Polynom-Ring(n,L)) by RLVECT_1:60
     .= 0_(n,L) by POLYNOM1:def 27;
    hence thesis by POLYNOM1:81;
    end;
A6: now let k be Nat;
    assume A7: P[k];
     for f being Polynomial of n,L,
        A being LeftLinearCombination of P
    st A is_MonomialRepresentation_of f & f = Sum(A) & len A = k+1
    holds (for i being Nat st i in dom A
           for m being Monomial of n,L, p being Polynomial of n,L
           st A.i = m*'p & p in P holds (m*'p).b = 0.L) implies f.b = 0.L
     proof
     let f be Polynomial of n,L,
         A be LeftLinearCombination of P;
     assume A8: A is_MonomialRepresentation_of f &
                f = Sum(A) & len A = k+1;
     assume A9: for i being Nat st i in dom A
                for m being Monomial of n,L, p being Polynomial of n,L
                st A.i = m*'p & p in P holds (m*'p).b = 0.L;
     set B = A|(Seg k);
     reconsider B as FinSequence of Polynom-Ring(n,L) by FINSEQ_1:23;
     reconsider B as LeftLinearCombination of P by IDEAL_1:42;
     set g = Sum B;
     reconsider g as Polynomial of n,L by POLYNOM1:def 27;
     A10: dom A = Seg(k+1) by A8,FINSEQ_1:def 3;
     A11: k <= len A by A8,NAT_1:29;
     then A12: len B = k by FINSEQ_1:21;
     A13: k <= k + 1 by NAT_1:29;
      dom B = Seg(k) by A11,FINSEQ_1:21;
     then A14: dom B c= dom A by A10,A13,FINSEQ_1:7;
      now let i be Nat;
       assume A15: i in dom B;
       then consider m being Monomial of n,L,
                p being Polynomial of n,L such that
       A16: p in P & A/.i = m*'p by A8,A14,Def6;
        B/.i = B.i by A15,FINSEQ_4:def 4 .= A.i by A15,FUNCT_1:68
           .= A/.i by A14,A15,FINSEQ_4:def 4;
       hence ex m being Monomial of n,L,
                p being Polynomial of n,L
             st p in P & B/.i = m *' p by A16;
       end;
     then A17: B is_MonomialRepresentation_of g by Def6;
     reconsider h = A/.(k+1) as Polynomial of n,L by POLYNOM1:def 27;
     A18: k + 1 in dom A by A10,FINSEQ_1:6;
     then B^<*A/.(k+1)*> = B^<*A.(k+1)*> by FINSEQ_4:def 4
                        .= A by A8,FINSEQ_3:61;
     then f = Sum(B) + Sum(<*A/.(k+1)*>) by A8,RLVECT_1:58
           .= Sum B + A/.(k+1) by RLVECT_1:61
           .= g + h by POLYNOM1:def 27;
     then A19: f.b = g.b + h.b by POLYNOM1:def 21;
      now let i be Nat;
       assume A20: i in dom B;
        now let m be Monomial of n,L, p be Polynomial of n,L;
         assume A21: B.i = m*'p & p in P;
         then A.i = m*'p by A20,FUNCT_1:68;
         hence (m*'p).b = 0.L by A9,A14,A20,A21;
         end;
       hence for m being Monomial of n,L, p being Polynomial of n,L
             st B.i = m*'p & p in P holds (m*'p).b = 0.L;
       end;
     then A22: g.b = 0.L by A7,A12,A17;
     consider m being Monomial of n,L,
              p being Polynomial of n,L such that
     A23: p in P & A/.(k+1) = m *' p by A8,A18,Def6;
      A/.(k+1) = A.(k+1) by A18,FINSEQ_4:def 4;
     then 0.L = h.b by A9,A18,A23;
     hence thesis by A19,A22,RLVECT_1:def 7;
     end;
    hence P[k+1];
    end;
A24: for k being Nat holds P[k] from Ind(A4,A6);
consider n being Nat such that A25: n = len A;
thus thesis by A1,A2,A3,A24,A25;
end;

definition
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A be LeftLinearCombination of P,
    b be bag of n;
pred A is_Standard_Representation_of f,P,b,T means :Def7:
  Sum A = f &
  for i being Nat st i in dom A
  ex m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L
  st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T;
end;

definition
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A be LeftLinearCombination of P;
pred A is_Standard_Representation_of f,P,T means :Def8:
  A is_Standard_Representation_of f,P,HT(f,T),T;
end;

definition
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    b be bag of n;
pred f has_a_Standard_Representation_of P,b,T means
   ex A being LeftLinearCombination of P
  st A is_Standard_Representation_of f,P,b,T;
end;

definition
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L);
pred f has_a_Standard_Representation_of P,T means :Def10:
  ex A being LeftLinearCombination of P
  st A is_Standard_Representation_of f,P,T;
end;

theorem Th37:
for n being Ordinal,
    T being connected TermOrder of n,
    L being right_zeroed add-associative right_complementable
            unital distributive non trivial (non empty doubleLoopStr),
    f being Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L),
    A being LeftLinearCombination of P,
    b being bag of n
holds A is_Standard_Representation_of f,P,b,T
implies A is_MonomialRepresentation_of f
proof
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A be LeftLinearCombination of P,
    b be bag of n;
assume A1: A is_Standard_Representation_of f,P,b,T;
then A2: Sum A = f &
     for i being Nat st i in dom A
     ex m being non-zero Monomial of n,L,
        p being non-zero Polynomial of n,L
     st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T by Def7;
 now let i be Nat;
  assume i in dom A;
  then consider m' being non-zero Monomial of n,L,
                p' being non-zero Polynomial of n,L such that
  A3: p' in P & A/.i = m'*'p' & HT(m'*'p',T) <= b,T by A1,Def7;
  thus ex m being Monomial of n,L,
       p being Polynomial of n,L st p in P & A/.i = m*'p by A3;
  end;
hence thesis by A2,Def6;
end;

Lm5:
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,g being Polynomial of n,L,
    f',g' being Element of Polynom-Ring(n,L) st f = f' & g = g'
for P being non empty Subset of Polynom-Ring(n,L)
holds PolyRedRel(P,T) reduces f,g implies
  ex A being LeftLinearCombination of P
  st f' = g' + Sum A &
     for i being Nat st i in dom A
     ex m being non-zero Monomial of n,L,
        p being non-zero Polynomial of n,L
     st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T
proof
let n be Ordinal,
    T be admissible connected TermOrder of n,
    L be add-associative right_complementable right_zeroed
         commutative associative well-unital distributive
         Abelian Field-like non degenerated (non empty doubleLoopStr),
    f,g be Polynomial of n,L,
    f',g' be Element of Polynom-Ring(n,L);
assume A1: f = f' & g = g';
let P be non empty Subset of Polynom-Ring(n,L);
assume A2: PolyRedRel(P,T) reduces f,g;
defpred P[Nat] means
  for f,g being Polynomial of n,L,
      f',g' being Element of Polynom-Ring(n,L) st f = f' & g = g'
  for P being non empty Subset of Polynom-Ring(n,L),
      R being RedSequence of PolyRedRel(P,T)
  st R.1 = f & R.len R = g & len R = $1
  ex A being LeftLinearCombination of P
  st f' = g' + Sum A &
     for i being Nat st i in dom A
     ex m being non-zero Monomial of n,L,
        p being non-zero Polynomial of n,L
        st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T;
A3: P[1]
     proof
     let f,g be Polynomial of n,L,
         f',g' be Element of Polynom-Ring(n,L);
     assume A4: f = f' & g = g';
     let P be non empty Subset of Polynom-Ring(n,L),
         R be RedSequence of PolyRedRel(P,T);
     assume A5: R.1 = f & R.len R = g & len R = 1;
     set A = <*>(the carrier of Polynom-Ring(n,L));
     A6: dom A = {};
      for i being set st i in dom A
       ex u being Element of Polynom-Ring(n,L),
          a being Element of P st A/.i = u*a;
     then reconsider A as LeftLinearCombination of P by IDEAL_1:def 10;
     take A;
      f' = g' + 0.(Polynom-Ring(n,L)) by A4,A5,RLVECT_1:def 7
       .= g' + Sum A by RLVECT_1:60;
     hence thesis by A6;
     end;
A7: now let k be Nat;
    assume A8: 1 <= k;
    thus P[k] implies P[k+1]
      proof
      assume A9: P[k];
       for f,g being Polynomial of n,L,
          f',g' being Element of Polynom-Ring(n,L) st f = f' & g = g'
      for P being non empty Subset of Polynom-Ring(n,L),
          R being RedSequence of PolyRedRel(P,T)
      st R.1 = f & R.len R = g & len R = k + 1
      ex A being LeftLinearCombination of P
        st f' = g' + Sum A &
        for i being Nat st i in dom A
          ex m being non-zero Monomial of n,L,
             p being non-zero Polynomial of n,L
          st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T
       proof
       let f,g be Polynomial of n,L,
           f',g' be Element of Polynom-Ring(n,L);
       assume A10: f = f' & g = g';
       let P be non empty Subset of Polynom-Ring(n,L),
           R be RedSequence of PolyRedRel(P,T);
       assume A11: R.1 = f & R.len R = g & len R = k + 1;
       then A12: dom R = Seg(k+1) by FINSEQ_1:def 3;
       A13: k <= k + 1 by NAT_1:29;
       then A14: k in dom R by A8,A12,FINSEQ_1:3;
       A15: 1 <= k + 1 by NAT_1:29;
       set Q = R|(Seg k);
       reconsider Q as FinSequence by FINSEQ_1:19;
       A16: len Q = k by A11,A13,FINSEQ_1:21;
       A17: dom Q = Seg k by A11,A13,FINSEQ_1:21;
        k <> 0 by A8;
       then A18: len Q > 0 by A16,NAT_1:19;
        now let i be Nat;
         assume A19: i in dom Q & i+1 in dom Q;
         then A20: 1 <= i & i <= k & 1 <= i+1 & i+1 <= k by A17,FINSEQ_1:3;
         then A21: i <= k+1 & i+1 <= k+1 by A13,AXIOMS:22;
         then A22: i in dom R by A12,A20,FINSEQ_1:3;
          i+1 in dom R by A12,A20,A21,FINSEQ_1:3;
         then A23: [R.i, R.(i+1)] in PolyRedRel(P,T) by A22,REWRITE1:def 2;
          R.i = Q.i by A19,FUNCT_1:68;
         hence [Q.i, Q.(i+1)] in PolyRedRel(P,T) by A19,A23,FUNCT_1:68;
         end;
       then reconsider Q as RedSequence of PolyRedRel(P,T)
         by A18,REWRITE1:def 2;
        k + 1 in dom R by A12,A15,FINSEQ_1:3;
       then A24: [R.k,R.(k+1)] in PolyRedRel(P,T) by A14,REWRITE1:def 2;
       then consider h',g2 being set such that
       A25: [R.k,R.(k+1)] = [h',g2] &
           h' in (the carrier of Polynom-Ring(n,L)) \ {0_(n,L)} &
           g2 in (the carrier of Polynom-Ring(n,L)) by RELSET_1:6;
       A26: R.k = [h',g2]`1 by A25,MCART_1:def 1 .= h' by MCART_1:def 1;
       A27: h' in (the carrier of Polynom-Ring(n,L)) by A25,XBOOLE_0:def 4;
        not(h' in {0_(n,L)}) by A25,XBOOLE_0:def 4;
       then h' <> 0_(n,L) by TARSKI:def 1;
       then reconsider h' as non-zero Polynomial of n,L
            by A27,POLYNOM1:def 27,POLYNOM7:def 2;
       reconsider g2 as Polynomial of n,L by A25,POLYNOM1:def 27;
        k <> 0 by A8;
       then A28: k in dom Q by A17,FINSEQ_1:5;
       then A29: Q.k = h' by A26,FUNCT_1:68;
       then Q.k is Element of Polynom-Ring(n,L)
            by POLYNOM1:def 27;
       then reconsider u' = Q.k as Element of Polynom-Ring(n,L)
           ;
       reconsider u = u' as Polynomial of n,L by POLYNOM1:def 27;
       A30: 1 in dom Q by A8,A17,FINSEQ_1:3;
       then A31: Q.1 = f by A11,FUNCT_1:68;
        Q.len Q = u by A11,A13,FINSEQ_1:21;
       then consider A' being LeftLinearCombination of P such that
       A32: f' = u' + Sum A' &
           for i being Nat st i in dom A'
           ex m being non-zero Monomial of n,L,
              p being non-zero Polynomial of n,L
           st p in P & A'.i = m*'p & HT(m*'p,T)<=HT(f,T),T by A9,A10,A16,A31;
        now per cases;
       case u' = g';
       hence thesis by A32;
       case A33: u' <> g';
        h' reduces_to g2,P,T by A24,A25,POLYRED:def 13;
       then consider p' being Polynomial of n,L such that
       A34: p' in P & h' reduces_to g2,p',T by POLYRED:def 7;
       consider m' being Monomial of n,L such that
       A35: g2 = h' - m' *' p' &
           not(HT(m'*'p',T) in Support g2) & HT(m'*'p',T) <= HT(h',T),T
           by A34,GROEB_1:2;
        h' is Element of Polynom-Ring(n,L) by POLYNOM1:def 27;
       then reconsider hh = h' as Element of Polynom-Ring(n,L)
           ;
       A36: R.(k+1) = [h',g2]`2 by A25,MCART_1:def 2 .= g2 by MCART_1:def 2;
       then reconsider gg = g2 as Element of Polynom-Ring(n,L) by A10,A11;
        m' is Element of Polynom-Ring(n,L) by POLYNOM1:def 27;
       then reconsider mm = m' as Element of Polynom-Ring(n,L)
           ;
       reconsider pp = p' as Element of P by A34;
        m'*'p' is Element of Polynom-Ring(n,L)
            by POLYNOM1:def 27;
       then reconsider mp = m'*'p' as Element of Polynom-Ring(n,L)
           ;
       A37: mp = mm * pp by POLYNOM1:def 27;
        now assume p' = 0_(n,L);
         then g2 = h' - 0_(n,L) by A35,POLYRED:5
                .= Q.k by A29,POLYRED:4;
         hence contradiction by A10,A11,A33,A36;
         end;
       then reconsider p' as non-zero Polynomial of n,L by POLYNOM7:def 2;
        now assume m' = 0_(n,L);
         then g2 = h' - 0_(n,L) by A35,POLYRED:5
                .= Q.k by A29,POLYRED:4;
         hence contradiction by A10,A11,A33,A36;
         end;
       then reconsider m' as non-zero Monomial of n,L by POLYNOM7:def 2;
       A38: gg = hh - mp by A35,Lm3;
       A39: PolyRedRel(P,T) reduces f,h' by A8,A28,A29,A30,A31,REWRITE1:18;
        h' is_reducible_wrt p',T by A34,POLYRED:def 8;
       then h' <> 0_(n,L) by POLYRED:37;
       then HT(h',T) <= HT(f,T),T by A39,POLYRED:44;
       then A40: HT(m'*'p',T) <= HT(f,T),T by A35,TERMORD:8;
       set B = (A')^(<*mp*>);
        len B = len A' + len<*m'*'p'*> by FINSEQ_1:35
            .= len A' + 1 by FINSEQ_1:57;
       then A41: dom B = Seg(len A' + 1) by FINSEQ_1:def 3;
        now let i be set;
         assume A42: i in dom B;
         then reconsider j = i as Nat;
         A43: 1 <= j & j <= len A' + 1 by A41,A42,FINSEQ_1:3;
          now per cases;
         case j = len A' + 1;
           then mp = B.j by FINSEQ_1:59 .= B/.j by A42,FINSEQ_4:def 4;
           hence ex u being Element of Polynom-Ring(n,L),
                    a being Element of P st B/.i = u*a by A37;
         case j <> len A' + 1;
           then j < len A' + 1 by A43,REAL_1:def 5;
           then j <= len A' by NAT_1:38;
           then j in Seg(len A') by A43,FINSEQ_1:3;
           then A44: j in dom A' by FINSEQ_1:def 3;
           then consider m being non-zero Monomial of n,L,
                         p being non-zero Polynomial of n,L such that
           A45: p in P & A'.j = m*'p & HT(m*'p,T) <= HT(f,T),T by A32;
           A46: B.j = B/.j by A42,FINSEQ_4:def 4;
            m is Element of Polynom-Ring(n,L)
              by POLYNOM1:def 27;
           then reconsider u' = m as Element of Polynom-Ring(n,L)
             ;
           reconsider a' = p as Element of P by A45;
            u' * a' = m *' p by POLYNOM1:def 27
                  .= B/.j by A44,A45,A46,FINSEQ_1:def 7;
           hence ex u being Element of Polynom-Ring(n,L),
                    a being Element of P st B/.i = u*a;
           end;
         hence ex u being Element of Polynom-Ring(n,L),
                  a being Element of P st B/.i = u*a;
         end;
       then reconsider B as LeftLinearCombination of P by IDEAL_1:def 10;
       take B;
       A47: gg + Sum B = gg + (Sum(A') + Sum(<*mp*>)) by RLVECT_1:58
             .= gg + (Sum(A') + mp) by RLVECT_1:61
             .= (hh + -mp) + (Sum(A') + mp) by A38,RLVECT_1:def 11
             .= hh + (-mp + (Sum(A') + mp)) by RLVECT_1:def 6
             .= hh + (Sum(A') + (-mp + mp)) by RLVECT_1:def 6
             .= hh + (Sum(A') + 0.(Polynom-Ring(n,L))) by RLVECT_1:16
             .= hh + Sum(A') by RLVECT_1:10
             .= f' by A26,A28,A32,FUNCT_1:68;
        now let i be Nat;
         assume i in dom B;
         then A48: 1 <= i & i <= len A' + 1 by A41,FINSEQ_1:3;
          now per cases;
         case i = len A' + 1;
           then mp = B.i by FINSEQ_1:59;
           hence ex m being non-zero Monomial of n,L,
                    p being non-zero Polynomial of n,L
                 st p in P & B.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A34,A40;
         case i <> len A' + 1;
           then i < len A' + 1 by A48,REAL_1:def 5;
           then i <= len A' by NAT_1:38;
           then i in Seg(len A') by A48,FINSEQ_1:3;
           then A49: i in dom A' by FINSEQ_1:def 3;
           then consider m being non-zero Monomial of n,L,
                         p being non-zero Polynomial of n,L such that
           A50: p in P & A'.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A32;
            B.i = m *' p by A49,A50,FINSEQ_1:def 7;
           hence ex m being non-zero Monomial of n,L,
                    p being non-zero Polynomial of n,L
                 st p in P & B.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A50;
           end;
         hence ex m being non-zero Monomial of n,L,
                  p being non-zero Polynomial of n,L
                  st p in P & B.i = m*'p & HT(m*'p,T) <= HT(f,T),T;
         end;
       hence thesis by A10,A11,A36,A47;
       end;
      hence thesis;
      end;
      hence thesis;
      end;
    end;
A51: for k being Nat st 1 <= k holds P[k] from Ind2(A3,A7);
consider R being RedSequence of PolyRedRel(P,T) such that
A52: R.1 = f & R.len R = g by A2,REWRITE1:def 3;
 len R > 0 by REWRITE1:def 2;
then 1 <= len R by RLVECT_1:99;
hence thesis by A1,A51,A52;
end;

theorem
 for n being Ordinal,
    T being connected TermOrder of n,
    L being right_zeroed add-associative right_complementable
            unital distributive non trivial (non empty doubleLoopStr),
    f,g being Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L),
    A,B being LeftLinearCombination of P,
    b being bag of n
st A is_Standard_Representation_of f,P,b,T &
   B is_Standard_Representation_of g,P,b,T
holds A^B is_Standard_Representation_of f+g,P,b,T
proof
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f,g be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A,B be LeftLinearCombination of P,
    b be bag of n;
assume A1: A is_Standard_Representation_of f,P,b,T &
           B is_Standard_Representation_of g,P,b,T;
then f = Sum A & g = Sum B by Def7;
then A2: f + g = Sum A + Sum B by POLYNOM1:def 27
             .= Sum(A^B) by RLVECT_1:58;
 now let i be Nat;
  assume A3: i in dom(A^B);
   now per cases by A3,FINSEQ_1:38;
  case A4: i in dom A;
    then consider m being non-zero Monomial of n,L,
                  p being non-zero Polynomial of n,L such that
    A5: p in P & A/.i = m *' p & HT(m*'p,T) <= b,T by A1,Def7;
     (A^B)/.i = (A^B).i by A3,FINSEQ_4:def 4
            .= A.i by A4,FINSEQ_1:def 7
            .= A/.i by A4,FINSEQ_4:def 4;
    hence ex m being non-zero Monomial of n,L,
             p being non-zero Polynomial of n,L
          st p in P & (A^B)/.i = m *' p & HT(m*'p,T) <= b,T by A5;
  case ex k being Nat st k in dom B & i = len A + k;
    then consider k being Nat such that
    A6: k in dom B & i = len A + k;
    consider m being non-zero Monomial of n,L,
             p being non-zero Polynomial of n,L such that
    A7: p in P & B/.k = m *' p & HT(m*'p,T) <= b,T by A1,A6,Def7;
     (A^B)/.i = (A^B).i by A3,FINSEQ_4:def 4
            .= B.k by A6,FINSEQ_1:def 7
            .= B/.k by A6,FINSEQ_4:def 4;
    hence ex m being non-zero Monomial of n,L,
             p being non-zero Polynomial of n,L
          st p in P & (A^B)/.i = m *' p & HT(m*'p,T) <= b,T by A7;
    end;
  hence ex m being non-zero Monomial of n,L,
           p being non-zero Polynomial of n,L
        st p in P & (A^B)/.i = m *' p & HT(m*'p,T) <= b,T;
  end;
hence thesis by A2,Def7;
end;

theorem
 for n being Ordinal,
    T being connected TermOrder of n,
    L being right_zeroed add-associative right_complementable
            unital distributive non trivial (non empty doubleLoopStr),
    f,g being Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L),
    A,B being LeftLinearCombination of P,
    b being bag of n,
    i being Nat
st A is_Standard_Representation_of f,P,b,T &
   B = A|i & g = Sum(A/^i)
holds B is_Standard_Representation_of f-g,P,b,T
proof
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f,g be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A,B be LeftLinearCombination of P,
    b be bag of n,
    i be Nat;
assume A1: A is_Standard_Representation_of f,P,b,T &
           B = A|i & g = Sum(A/^i);
then A2:  Sum A = f &
  for i being Nat st i in dom A
  ex m being non-zero Monomial of n,L,
     p being non-zero Polynomial of n,L
  st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T by Def7;
 A = B ^ (A/^i) by A1,RFINSEQ:21;
then Sum A = Sum B + Sum(A/^i) by RLVECT_1:58;
then Sum A + -(Sum(A/^i))
  = Sum B + (Sum(A/^i) + -Sum(A/^i)) by RLVECT_1:def 6
 .= Sum B + 0.(Polynom-Ring(n,L)) by RLVECT_1:16
 .= Sum B by RLVECT_1:def 7;
then A3: Sum B = Sum A - (Sum(A/^i)) by RLVECT_1:def 11
             .= f - g by A1,A2,Lm3;
 dom(A|(Seg i)) c= dom A by FUNCT_1:76;
then A4: dom B c= dom A by A1,TOPREAL1:def 1;
 now let j being Nat;
  assume A5: j in dom B;
  then A6: j in dom(A|(Seg i)) by A1,TOPREAL1:def 1;
  A7: A/.j = A.j by A4,A5,FINSEQ_4:def 4
         .= (A|(Seg i)).j by A6,FUNCT_1:70
         .= B.j by A1,TOPREAL1:def 1
         .= B/.j by A5,FINSEQ_4:def 4;
  consider m being non-zero Monomial of n,L,
           p being non-zero Polynomial of n,L such that
  A8: p in P & A/.j = m *' p & HT(m*'p,T) <= b,T
     by A1,A4,A5,Def7;
  thus ex m being non-zero Monomial of n,L,
          p being non-zero Polynomial of n,L
  st p in P & B/.j = m *' p & HT(m*'p,T) <= b,T by A7,A8;
  end;
hence thesis by A3,Def7;
end;

theorem
 for n being Ordinal,
    T being connected TermOrder of n,
    L being Abelian right_zeroed add-associative right_complementable
            unital distributive non trivial (non empty doubleLoopStr),
    f,g being Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L),
    A,B being LeftLinearCombination of P,
    b being bag of n,
    i being Nat
st A is_Standard_Representation_of f,P,b,T &
   B = A/^i & g = Sum(A|i) & i <= len A
holds B is_Standard_Representation_of f-g,P,b,T
proof
let n be Ordinal,
    T be connected TermOrder of n,
    L be Abelian right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f,g be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A,B be LeftLinearCombination of P,
    b be bag of n,
    i be Nat;
assume A1: A is_Standard_Representation_of f,P,b,T &
           B = A/^i & g = Sum(A|i) & i <= len A;
then A2:  Sum A = f &
  for i being Nat st i in dom A
  ex m being non-zero Monomial of n,L,
     p being non-zero Polynomial of n,L
  st p in P & A/.i = m *' p & HT(m*'p,T) <= b,T by Def7;
 A = (A|i) ^ B by A1,RFINSEQ:21;
then Sum A = Sum(A|i) + Sum B by RLVECT_1:58;
then Sum A + -(Sum(A|i))
  = (Sum(A|i) + -Sum(A|i)) + Sum B by RLVECT_1:def 6
 .= 0.(Polynom-Ring(n,L)) + Sum B by RLVECT_1:16
 .= Sum B by ALGSTR_1:def 5;
then A3: Sum B = Sum A - (Sum(A|i)) by RLVECT_1:def 11
             .= f - g by A1,A2,Lm3;
 now let j being Nat;
  assume A4: j in dom B;
  then A5: j + i in dom A by A1,FINSEQ_5:29;
  A6: B/.j = B.j by A4,FINSEQ_4:def 4
         .= A.(j+i) by A1,A4,RFINSEQ:def 2
         .= A/.(j+i) by A5,FINSEQ_4:def 4;
  consider m being non-zero Monomial of n,L,
           p being non-zero Polynomial of n,L such that
  A7: p in P & A/.(j+i) = m *' p & HT(m*'p,T) <= b,T
     by A1,A5,Def7;
  thus ex m being non-zero Monomial of n,L,
          p being non-zero Polynomial of n,L
  st p in P & B/.j = m *' p & HT(m*'p,T) <= b,T by A6,A7;
  end;
hence thesis by A3,Def7;
end;

theorem Th41:
for n being Ordinal,
    T being connected TermOrder of n,
    L being right_zeroed add-associative right_complementable
            unital distributive non trivial (non empty doubleLoopStr),
    f being non-zero Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L),
    A being LeftLinearCombination of P
st A is_MonomialRepresentation_of f
ex i being Nat,
   m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L
st i in dom A & p in P & A.i = m *' p & HT(f,T) <= HT(m*'p,T),T
proof
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be non-zero Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A be LeftLinearCombination of P;
assume A1: A is_MonomialRepresentation_of f;
 f <> 0_(n,L) by POLYNOM7:def 2;
then HC(f,T) <> 0.L by TERMORD:17;
then f.(HT(f,T)) <> 0.L by TERMORD:def 7;
then consider i being Nat such that
A2: i in dom A &
    ex m being Monomial of n,L, p being Polynomial of n,L
    st A.i = m *' p & p in P & (m*'p).HT(f,T) <> 0.L by A1,Lm4;
consider m being Monomial of n,L, p being Polynomial of n,L such that
A3: A.i = m *' p & (m*'p).HT(f,T) <> 0.L & p in P by A2;
A4: m*'p <> 0_(n,L) by A3,POLYNOM1:81;
then m <> 0_(n,L) by POLYRED:5;
then reconsider m as non-zero Monomial of n,L by POLYNOM7:def 2;
 p <> 0_(n,L) by A4,POLYNOM1:87;
then reconsider p as non-zero Polynomial of n,L by POLYNOM7:def 2;
 HT(f,T) in Support(m*'p) by A3,POLYNOM1:def 9;
then HT(f,T) <= HT(m*'p,T),T by TERMORD:def 6;
hence thesis by A2,A3;
end;

theorem Th42:
for n being Ordinal,
    T being connected TermOrder of n,
    L being right_zeroed add-associative right_complementable
            unital distributive non trivial (non empty doubleLoopStr),
    f being non-zero Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L),
    A being LeftLinearCombination of P
      st A is_Standard_Representation_of f,P,T
ex i being Nat,
   m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L
st p in P & i in dom A & A/.i = m *' p & HT(f,T) = HT(m*'p,T)
proof
let n be Ordinal,
    T be connected TermOrder of n,
    L be right_zeroed add-associative right_complementable
         unital distributive non trivial (non empty doubleLoopStr),
    f be non-zero Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L),
    A be LeftLinearCombination of P;
assume A is_Standard_Representation_of f,P,T;
then A1: A is_Standard_Representation_of f,P,HT(f,T),T by Def8;
then A is_MonomialRepresentation_of f by Th37;
then consider i being Nat, m being non-zero Monomial of n,L,
         p being non-zero Polynomial of n,L such that
A2: i in dom A & p in P & A.i = m *' p &
   HT(f,T) <= HT(m*'p,T),T by Th41;
consider m' being non-zero Monomial of n,L,
         p' being non-zero Polynomial of n,L such that
A3: p' in P & A/.i = m' *' p' & HT(m'*'p',T) <= HT(f,T),T by A1,A2,Def7;
take i,m',p';
 m *' p = m' *' p' by A2,A3,FINSEQ_4:def 4;
hence thesis by A2,A3,TERMORD:7;
end;

theorem Th43:
::: lemma 5.60, p. 218
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 being Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L)
holds PolyRedRel(P,T) reduces f,0_(n,L) implies
      f has_a_Standard_Representation_of P,T
proof
let n be Ordinal,
    T be admissible connected TermOrder of n,
    L be add-associative right_complementable right_zeroed
         commutative associative well-unital distributive
         Abelian Field-like non degenerated (non empty doubleLoopStr),
    f be Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L);
assume A1: PolyRedRel(P,T) reduces f,0_(n,L);
 f is Element of Polynom-Ring(n,L) by POLYNOM1:def 27;
then reconsider f' = f as Element of Polynom-Ring(n,L);
 0_(n,L) = 0.(Polynom-Ring(n,L)) by POLYNOM1:def 27;
then consider A being LeftLinearCombination of P such that
A2: f' = 0.(Polynom-Ring(n,L)) + Sum A &
   for i being Nat st i in dom A
   ex m being non-zero Monomial of n,L,
      p being non-zero Polynomial of n,L
   st p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A1,Lm5;
A3: f = Sum A by A2,RLVECT_1:def 7;
 now let i be Nat;
  assume A4: i in dom A;
  then A5: A.i = A/.i by FINSEQ_4:def 4;
  consider m being non-zero Monomial of n,L,
           p being non-zero Polynomial of n,L such that
  A6: p in P & A.i = m*'p & HT(m*'p,T) <= HT(f,T),T by A2,A4;
  thus ex m being non-zero Monomial of n,L,
          p being non-zero Polynomial of n,L
       st p in P & A/.i = m *' p & HT(m*'p,T) <= HT(f,T),T by A5,A6;
  end;
then A is_Standard_Representation_of f,P,HT(f,T),T by A3,Def7;
then A is_Standard_Representation_of f,P,T by Def8;
hence thesis by Def10;
end;

theorem Th44:
::: lemma 5.61, p. 218
for n being Ordinal,
    T being admissible connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            commutative associative well-unital distributive
            Field-like (non trivial doubleLoopStr),
    f being non-zero Polynomial of n,L,
    P being non empty Subset of Polynom-Ring(n,L)
holds f has_a_Standard_Representation_of P,T implies
      f is_top_reducible_wrt P,T
proof
let n be Ordinal,
    T be admissible connected TermOrder of n,
    L be add-associative right_complementable right_zeroed
         commutative associative well-unital distributive
         Field-like (non trivial doubleLoopStr),
    f be non-zero Polynomial of n,L,
    P be non empty Subset of Polynom-Ring(n,L);
assume f has_a_Standard_Representation_of P,T;
then consider A being LeftLinearCombination of P
such that A1: A is_Standard_Representation_of f,P,T by Def10;
consider i being Nat,
         m being non-zero Monomial of n,L,
         p being non-zero Polynomial of n,L such that
A2: p in P & i in dom A & A/.i = m*'p & HT(f,T) = HT(m*'p,T) by A1,Th42;
A3: i in dom A & p <> 0_(n,L) & p in P &
    A/.i = m *' p by A2,POLYNOM7:def 2;
A4: f <> 0_(n,L) by POLYNOM7:def 2;
then Support f <> {} by POLYNOM7:1;
then A5: HT(f,T) in Support f by TERMORD:def 6;
set s = HT(m,T);
set g = f - (f.HT(f,T)/HC(p,T)) * (s *' p);
 HT(f,T) = s + HT(p,T) by A2,TERMORD:31;
then f reduces_to g,p,HT(f,T),T by A3,A4,A5,POLYRED:def 5;
then f top_reduces_to g,p,T by POLYRED:def 10;
then f is_top_reducible_wrt p,T by POLYRED:def 11;
hence thesis by A2,POLYRED:def 12;
end;

theorem
::: theorem 5.62, p. 219
 for n being Nat,
    T being connected admissible TermOrder of n,
    L being add-associative right_complementable right_zeroed
            commutative associative well-unital distributive Abelian
            Field-like non degenerated (non empty doubleLoopStr),
    G being non empty Subset of Polynom-Ring(n,L)
holds G is_Groebner_basis_wrt T
      iff for f being non-zero Polynomial of n,L st f in G-Ideal
          holds f has_a_Standard_Representation_of G,T
proof
let n be Nat,
    T be connected admissible TermOrder of n,
    L be add-associative right_complementable right_zeroed
         commutative associative well-unital distributive Abelian
         Field-like non degenerated (non empty doubleLoopStr),
    P be non empty Subset of Polynom-Ring(n,L);
A1: now assume P is_Groebner_basis_wrt T;
   then PolyRedRel(P,T) is locally-confluent by GROEB_1:def 3;
   then PolyRedRel(P,T) is confluent by GROEB_1:12;
   then PolyRedRel(P,T) is with_UN_property by GROEB_1:13;
   then A2: PolyRedRel(P,T) is with_Church-Rosser_property by GROEB_1:14;
    now let f be non-zero Polynomial of n,L;
     assume f in P-Ideal;
     then PolyRedRel(P,T) reduces f,0_(n,L) by A2,GROEB_1:15;
     hence f has_a_Standard_Representation_of P,T by Th43;
     end;
   hence for f being non-zero Polynomial of n,L st f in P-Ideal
         holds f has_a_Standard_Representation_of P,T;
   end;
 now assume A3: for f being non-zero Polynomial of n,L st f in P-Ideal
               holds f has_a_Standard_Representation_of P,T;
    now let f be non-zero Polynomial of n,L;
     assume f in P-Ideal;
     then f has_a_Standard_Representation_of P,T by A3;
     hence f is_top_reducible_wrt P,T by Th44;
     end;
   then for b being bag of n st b in HT(P-Ideal,T)
        ex b' being bag of n st b' in HT(P,T) & b' divides b by GROEB_1:18;
   then HT(P-Ideal,T) c= multiples(HT(P,T)) by GROEB_1:19;
   then PolyRedRel(P,T) is locally-confluent by GROEB_1:20;
   hence P is_Groebner_basis_wrt T by GROEB_1:def 3;
   end;
hence thesis by A1;
end;

Back to top