groeb_1.miz



    begin

    definition

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L;

      :: original: {

      redefine

      func {p} -> Subset of ( Polynom-Ring (n,L)) ;

      coherence

      proof

        now

          let u be object;

          assume u in {p};

          then u = p by TARSKI:def 1;

          hence u in the carrier of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: GROEB_1:1

    

     Th1: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L holds f reduces_to (g,p,T) implies ex m be Monomial of n, L st g = (f - (m *' p))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L;

      assume f reduces_to (g,p,T);

      then

      consider b be bag of n such that

       A1: f reduces_to (g,p,b,T) by POLYRED:def 6;

      consider s be bag of n such that (s + ( HT (p,T))) = b and

       A2: g = (f - (((f . b) / ( HC (p,T))) * (s *' p))) by A1, POLYRED:def 5;

      (((f . b) / ( HC (p,T))) * (s *' p)) = (( Monom (((f . b) / ( HC (p,T))),s)) *' p) by POLYRED: 22;

      hence thesis by A2;

    end;

    theorem :: GROEB_1:2

    for n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g be Polynomial of n, L holds f reduces_to (g,p,T) implies ex m be Monomial of n, L st g = (f - (m *' p)) & not (( HT ((m *' p),T)) in ( Support g)) & ( 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 almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g be Polynomial of n, L;

      assume f reduces_to (g,p,T);

      then

      consider b be bag of n such that

       A1: f reduces_to (g,p,b,T) by POLYRED:def 6;

      b in ( Support f) by A1, POLYRED:def 5;

      then

       A2: (f . b) <> ( 0. L) by POLYNOM1:def 4;

      p <> ( 0_ (n,L)) by A1, POLYRED:def 5;

      then

      reconsider p as non-zero Polynomial of n, L by POLYNOM7:def 1;

      consider s be bag of n such that

       A3: (s + ( HT (p,T))) = b and

       A4: g = (f - (((f . b) / ( HC (p,T))) * (s *' p))) by A1, POLYRED:def 5;

      set m = ( Monom (((f . b) / ( HC (p,T))),s));

      

       A5: (( HC (p,T)) " ) <> ( 0. L) by VECTSP_1: 25;

      

       A6: ((f . b) / ( HC (p,T))) <> ( 0. L) by A2, A5, VECTSP_2:def 1;

      then

       A7: ((f . b) / ( HC (p,T))) is non zero;

      ( coefficient m) <> ( 0. L) by A6, POLYNOM7: 9;

      then ( HC (m,T)) <> ( 0. L) by TERMORD: 23;

      then m <> ( 0_ (n,L)) by TERMORD: 17;

      then

      reconsider m as non-zero Monomial of n, L by POLYNOM7:def 1;

      

       A8: ( HT ((m *' p),T)) = (( HT (m,T)) + ( HT (p,T))) by TERMORD: 31

      .= (( term m) + ( HT (p,T))) by TERMORD: 23

      .= (s + ( HT (p,T))) by A7, POLYNOM7: 10;

      then ( HT ((m *' p),T)) in ( Support f) by A1, A3, POLYRED:def 5;

      then (((f . b) / ( HC (p,T))) * (s *' p)) = (( Monom (((f . b) / ( HC (p,T))),s)) *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T) by POLYRED: 22, TERMORD:def 6;

      hence thesis by A1, A3, A4, A8, POLYRED: 39;

    end;

    

     Lm1: for L be add-associative left_zeroed right_zeroed add-cancelable right_complementable associative distributive well-unital non empty doubleLoopStr, P be Subset of L, p be 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;

      set f = <*p*>;

      assume

       A1: p in P;

      then

      reconsider P9 = P as non empty Subset of L;

      now

        let i be set;

        assume

         A2: i in ( dom f);

        ( dom f) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then i = 1 by A2, TARSKI:def 1;

        

        then (f /. i) = (f . 1) by A2, PARTFUN1:def 6

        .= p by FINSEQ_1: 40

        .= (( 1. L) * p)

        .= ((( 1. L) * p) * ( 1. L));

        hence ex u,v be Element of L, a be Element of P9 st (f /. i) = ((u * a) * v) by A1;

      end;

      then

      reconsider f as LinearCombination of P9 by IDEAL_1:def 8;

      ( Sum f) = p by RLVECT_1: 44;

      hence thesis by IDEAL_1: 60;

    end;

    

     Lm2: for n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, p,q be Polynomial of n, L, f,g be Element of ( Polynom-Ring (n,L)) holds (f = p & g = q) implies (f - g) = (p - q)

    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 almost_left_invertible non degenerated non empty doubleLoopStr, p,q be Polynomial of n, L, f,g be Element of ( Polynom-Ring (n,L));

      assume that

       A1: f = p and

       A2: g = q;

      reconsider x = ( - q) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      reconsider x as Element of ( Polynom-Ring (n,L));

      (x + g) = (( - q) + q) by A2, POLYNOM1:def 11

      .= ( 0_ (n,L)) by POLYRED: 3

      .= ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      then

       A3: ( - q) = ( - g) by RLVECT_1: 6;

      

      thus (p - q) = (p + ( - q)) by POLYNOM1:def 7

      .= (f + ( - g)) by A1, A3, POLYNOM1:def 11

      .= (f - g);

    end;

    

     Lm3: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L holds f is_irreducible_wrt (( 0_ (n,L)),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 almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L;

      assume f is_reducible_wrt (( 0_ (n,L)),T);

      then

      consider g be Polynomial of n, L such that

       A1: f reduces_to (g,( 0_ (n,L)),T) by POLYRED:def 8;

      ex b be bag of n st f reduces_to (g,( 0_ (n,L)),b,T) by A1, POLYRED:def 6;

      hence thesis by POLYRED:def 5;

    end;

    theorem :: GROEB_1:3

    

     Th3: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,g be Polynomial of n, L, P,Q be Subset of ( Polynom-Ring (n,L)) st P c= Q holds f reduces_to (g,P,T) implies f reduces_to (g,Q,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 almost_left_invertible non trivial doubleLoopStr, f,g be Polynomial of n, L, P,Q be Subset of ( Polynom-Ring (n,L));

      assume

       A1: P c= Q;

      assume f reduces_to (g,P,T);

      then ex p be Polynomial of n, L st p in P & f reduces_to (g,p,T) by POLYRED:def 7;

      hence thesis by A1, POLYRED:def 7;

    end;

    theorem :: GROEB_1:4

    

     Th4: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P,Q be Subset of ( Polynom-Ring (n,L)) holds P c= Q implies ( PolyRedRel (P,T)) c= ( PolyRedRel (Q,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 almost_left_invertible non trivial doubleLoopStr, P,Q be Subset of ( Polynom-Ring (n,L));

      assume

       A1: P c= Q;

      now

        let u be object;

        assume

         A2: u in ( PolyRedRel (P,T));

        then

        consider p,q be object such that

         A3: p in ( NonZero ( Polynom-Ring (n,L))) and

         A4: q in the carrier of ( Polynom-Ring (n,L)) and

         A5: u = [p, q] by ZFMISC_1:def 2;

        reconsider q as Polynomial of n, L by A4, POLYNOM1:def 11;

        ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

        then not p in {( 0_ (n,L))} by A3, XBOOLE_0:def 5;

        then p <> ( 0_ (n,L)) by TARSKI:def 1;

        then

        reconsider p as non-zero Polynomial of n, L by A3, POLYNOM1:def 11, POLYNOM7:def 1;

        p reduces_to (q,P,T) by A2, A5, POLYRED:def 13;

        then p reduces_to (q,Q,T) by A1, Th3;

        hence u in ( PolyRedRel (Q,T)) by A5, POLYRED:def 13;

      end;

      hence thesis;

    end;

    theorem :: GROEB_1:5

    

     Th5: for n be Ordinal, L be right_zeroed add-associative right_complementable non empty doubleLoopStr, p be Polynomial of n, L holds ( Support ( - p)) = ( Support p)

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable non empty doubleLoopStr, p be Polynomial of n, L;

       A1:

      now

        let u be object;

        assume

         A2: u in ( Support p);

        then

        reconsider u9 = u as Element of ( Bags n);

        

         A3: (p . u9) <> ( 0. L) by A2, POLYNOM1:def 4;

        now

          assume (( - p) . u9) = ( 0. L);

          then (( - p) . u9) = ( - ( - ( 0. L))) by RLVECT_1: 17;

          

          then ( - (p . u9)) = ( - ( - ( 0. L))) by POLYNOM1: 17

          .= ( 0. L) by RLVECT_1: 17;

          then (p . u9) = ( - ( 0. L)) by RLVECT_1: 17;

          hence contradiction by A3, RLVECT_1: 12;

        end;

        hence u in ( Support ( - p)) by POLYNOM1:def 4;

      end;

      now

        let u be object;

        assume

         A4: u in ( Support ( - p));

        then

        reconsider u9 = u as Element of ( Bags n);

        

         A5: (( - p) . u9) <> ( 0. L) by A4, POLYNOM1:def 4;

        now

          

           A6: (( - p) . u9) = ( - (p . u9)) by POLYNOM1: 17;

          assume (p . u9) = ( 0. L);

          hence contradiction by A5, A6, RLVECT_1: 12;

        end;

        hence u in ( Support p) by POLYNOM1:def 4;

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: GROEB_1:6

    

     Th6: for n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, p be Polynomial of n, L holds ( HT (( - p),T)) = ( HT (p,T))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, p be Polynomial of n, L;

      per cases ;

        suppose

         A1: p = ( 0_ (n,L));

        reconsider x = ( - p) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        reconsider x as Element of ( Polynom-Ring (n,L));

        

         A2: ( - ( 0_ (n,L))) = (( - ( 0_ (n,L))) + ( 0_ (n,L))) by POLYNOM1: 23

        .= ( 0_ (n,L)) by POLYRED: 3;

        ( 0. ( Polynom-Ring (n,L))) = ( 0_ (n,L)) by POLYNOM1:def 11;

        

        then (x + ( 0. ( Polynom-Ring (n,L)))) = (( - p) + ( 0_ (n,L))) by POLYNOM1:def 11

        .= ( 0_ (n,L)) by A1, A2, POLYNOM1: 23

        .= ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

        

        then ( - p) = ( - ( 0. ( Polynom-Ring (n,L)))) by RLVECT_1: 6

        .= ( 0. ( Polynom-Ring (n,L))) by RLVECT_1: 12

        .= p by A1, POLYNOM1:def 11;

        hence thesis;

      end;

        suppose p <> ( 0_ (n,L));

        then

         A3: ( Support p) <> {} by POLYNOM7: 1;

        then ( Support ( - p)) <> {} by Th5;

        then ( HT (( - p),T)) in ( Support ( - p)) by TERMORD:def 6;

        then ( HT (( - p),T)) in ( Support p) by Th5;

        then

         A4: ( HT (( - p),T)) <= (( HT (p,T)),T) by TERMORD:def 6;

        ( HT (p,T)) in ( Support p) by A3, TERMORD:def 6;

        then ( HT (p,T)) in ( Support ( - p)) by Th5;

        then ( HT (p,T)) <= (( HT (( - p),T)),T) by TERMORD:def 6;

        hence thesis by A4, TERMORD: 7;

      end;

    end;

    theorem :: GROEB_1:7

    

     Th7: for n be Ordinal, T be admissible connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L holds ( HT ((p - q),T)) <= (( max (( HT (p,T)),( HT (q,T)),T)),T)

    proof

      let n be Ordinal, T be admissible connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, p,q be Polynomial of n, L;

      ( HT ((p + ( - q)),T)) <= (( max (( HT (p,T)),( HT (( - q),T)),T)),T) by TERMORD: 34;

      then ( HT ((p - q),T)) <= (( max (( HT (p,T)),( HT (( - q),T)),T)),T) by POLYNOM1:def 7;

      hence thesis by Th6;

    end;

    theorem :: GROEB_1:8

    

     Th8: for n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p,q be Polynomial of n, L holds ( Support q) c= ( Support p) implies q <= (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 almost_left_invertible non trivial doubleLoopStr, p,q be Polynomial of n, L;

      assume

       A1: ( Support q) c= ( Support p);

      defpred P[ Nat] means for f,g be Polynomial of n, L st ( Support f) c= ( Support g) & ( card ( Support f)) = $1 holds f <= (g,T);

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];

        now

          set R = RelStr (# ( Bags n), T #);

          let f,g be Polynomial of n, L;

          assume that

           A4: ( Support f) c= ( Support g) and

           A5: ( card ( Support f)) = (k + 1);

          set rf = ( Red (f,T)), rg = ( Red (g,T));

          

           A6: ( Support f) <> {} by A5;

          then

           A7: ( HT (f,T)) in ( Support f) by TERMORD:def 6;

          f <> ( 0_ (n,L)) by A6, POLYNOM7: 1;

          then

           A8: f is non-zero by POLYNOM7:def 1;

          g <> ( 0_ (n,L)) by A4, A7, POLYNOM7: 1;

          then

           A9: g is non-zero by POLYNOM7:def 1;

          now

            per cases ;

              case

               A10: ( HT (f,T)) = ( HT (g,T));

              

               A11: ( Support rf) = (( Support f) \ {( HT (f,T))}) by TERMORD: 36;

              

               A12: ( Support rg) = (( Support g) \ {( HT (g,T))}) by TERMORD: 36;

              now

                let u be object;

                assume u in ( Support rf);

                then u in ( Support f) & not u in {( HT (f,T))} by A11, XBOOLE_0:def 5;

                hence u in ( Support rg) by A4, A10, A12, XBOOLE_0:def 5;

              end;

              then

               A13: ( Support rf) c= ( Support rg);

              for u be object holds u in {( HT (f,T))} implies u in ( Support f) by A7, TARSKI:def 1;

              then

               A14: {( HT (f,T))} c= ( Support f);

              

               A15: ( Support (f,T)) <> {} & ( Support (g,T)) <> {} by A4, A7, POLYRED:def 4;

              

               A16: ( Support (rf,T)) = ( Support rf) by POLYRED:def 4;

              ( HT (f,T)) in {( HT (f,T))} by TARSKI:def 1;

              then

               A17: not ( HT (f,T)) in ( Support ( Red (f,T))) by A11, XBOOLE_0:def 5;

              

               A18: ( PosetMax ( Support (f,T))) = ( HT (g,T)) by A8, A10, POLYRED: 24

              .= ( PosetMax ( Support (g,T))) by A9, POLYRED: 24;

              

               A19: ( Support (rg,T)) = ( Support rg) by POLYRED:def 4;

              

               A20: ( Support (g,T)) = ( Support g) by POLYRED:def 4;

              then

               A21: (( Support (g,T)) \ {( PosetMax ( Support (g,T)))}) = ( Support (rg,T)) by A9, A12, A19, POLYRED: 24;

              (( Support rf) \/ {( HT (f,T))}) = (( Support f) \/ {( HT (f,T))}) by A11, XBOOLE_1: 39

              .= ( Support f) by A14, XBOOLE_1: 12;

              then (( card ( Support ( Red (f,T)))) + 1) = (k + 1) by A5, A17, CARD_2: 41;

              then rf <= (rg,T) by A3, A13;

              then [( Support rf), ( Support rg)] in ( FinOrd RelStr (# ( Bags n), T #)) by POLYRED:def 2;

              then

               A22: [( Support (rf,T)), ( Support (rg,T))] in ( union ( rng ( FinOrd-Approx R))) by A16, A19, BAGORDER:def 15;

              

               A23: ( Support (f,T)) = ( Support f) by POLYRED:def 4;

              then (( Support (f,T)) \ {( PosetMax ( Support (f,T)))}) = ( Support (rf,T)) by A8, A11, A16, POLYRED: 24;

              then [( Support (f,T)), ( Support (g,T))] in ( union ( rng ( FinOrd-Approx R))) by A22, A15, A18, A21, BAGORDER: 35;

              then [( Support f), ( Support g)] in ( FinOrd RelStr (# ( Bags n), T #)) by A23, A20, BAGORDER:def 15;

              hence f <= (g,T) by POLYRED:def 2;

            end;

              case

               A24: ( HT (f,T)) <> ( HT (g,T));

              now

                assume ( HT (g,T)) < (( HT (f,T)),T);

                then not ( HT (f,T)) <= (( HT (g,T)),T) by TERMORD: 5;

                hence contradiction by A4, A7, TERMORD:def 6;

              end;

              then ( HT (f,T)) <= (( HT (g,T)),T) by TERMORD: 5;

              then ( HT (f,T)) < (( HT (g,T)),T) by A24, TERMORD:def 3;

              then f < (g,T) by POLYRED: 32;

              hence f <= (g,T) by POLYRED:def 3;

            end;

          end;

          hence f <= (g,T);

        end;

        hence P[(k + 1)];

      end;

      

       A25: ex k be Element of NAT st ( card ( Support q)) = k;

      

       A26: P[ 0 ]

      proof

        let f,g be Polynomial of n, L;

        assume that ( Support f) c= ( Support g) and

         A27: ( card ( Support f)) = 0 ;

        ( Support f) = {} by A27;

        then f = ( 0_ (n,L)) by POLYNOM7: 1;

        hence thesis by POLYRED: 30;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A26, A2);

      hence thesis by A1, A25;

    end;

    theorem :: GROEB_1:9

    

     Th9: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p be non-zero Polynomial of n, L holds f is_reducible_wrt (p,T) implies ( HT (p,T)) <= (( HT (f,T)),T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p be non-zero Polynomial of n, L;

      assume f is_reducible_wrt (p,T);

      then

      consider b be bag of n such that

       A1: b in ( Support f) & ( HT (p,T)) divides b by POLYRED: 36;

      b <= (( HT (f,T)),T) & ( HT (p,T)) <= (b,T) by A1, TERMORD: 10, TERMORD:def 6;

      hence thesis by TERMORD: 8;

    end;

    begin

    theorem :: GROEB_1:10

    

     Th10: for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p be Polynomial of n, L holds ( PolyRedRel ( {p},T)) is locally-confluent

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p be Polynomial of n, L;

      set R = ( PolyRedRel ( {p},T));

      

       A1: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      per cases ;

        suppose

         A2: p = ( 0_ (n,L));

        now

          let a,b,c be object;

          assume that

           A3: [a, b] in R and [a, c] in R;

          consider p9,q be object such that

           A4: p9 in ( NonZero ( Polynom-Ring (n,L))) and

           A5: q in the carrier of ( Polynom-Ring (n,L)) and

           A6: [a, b] = [p9, q] by A3, ZFMISC_1:def 2;

          reconsider q as Polynomial of n, L by A5, POLYNOM1:def 11;

           not p9 in {( 0_ (n,L))} by A1, A4, XBOOLE_0:def 5;

          then p9 <> ( 0_ (n,L)) by TARSKI:def 1;

          then

          reconsider p9 as non-zero Polynomial of n, L by A4, POLYNOM1:def 11, POLYNOM7:def 1;

          p9 reduces_to (q, {p},T) by A3, A6, POLYRED:def 13;

          then

          consider g be Polynomial of n, L such that

           A7: g in {p} and

           A8: p9 reduces_to (q,g,T) by POLYRED:def 7;

          g = ( 0_ (n,L)) by A2, A7, TARSKI:def 1;

          then p9 is_reducible_wrt (( 0_ (n,L)),T) by A8, POLYRED:def 8;

          hence (b,c) are_convergent_wrt R by Lm3;

        end;

        hence thesis by REWRITE1:def 24;

      end;

        suppose p <> ( 0_ (n,L));

        then

        reconsider p as non-zero Polynomial of n, L by POLYNOM7:def 1;

        now

          let a,b,c be object;

          assume that

           A9: [a, b] in R and

           A10: [a, c] in R;

          consider pa,pb be object such that

           A11: pa in ( NonZero ( Polynom-Ring (n,L))) and

           A12: pb in the carrier of ( Polynom-Ring (n,L)) and

           A13: [a, b] = [pa, pb] by A9, ZFMISC_1:def 2;

           not pa in {( 0_ (n,L))} by A1, A11, XBOOLE_0:def 5;

          then pa <> ( 0_ (n,L)) by TARSKI:def 1;

          then

          reconsider pa as non-zero Polynomial of n, L by A11, POLYNOM1:def 11, POLYNOM7:def 1;

          reconsider pb as Polynomial of n, L by A12, POLYNOM1:def 11;

          

           A14: pb = b by A13, XTUPLE_0: 1;

          

           A15: pa = a by A13, XTUPLE_0: 1;

          then pa reduces_to (pb, {p},T) by A9, A14, POLYRED:def 13;

          then ex p9 be Polynomial of n, L st p9 in {p} & pa reduces_to (pb,p9,T) by POLYRED:def 7;

          then

           A16: pa reduces_to (pb,p,T) by TARSKI:def 1;

          consider pa9,pc be object such that pa9 in ( NonZero ( Polynom-Ring (n,L))) and

           A17: pc in the carrier of ( Polynom-Ring (n,L)) and

           A18: [a, c] = [pa9, pc] by A10, ZFMISC_1:def 2;

          reconsider pc as Polynomial of n, L by A17, POLYNOM1:def 11;

          

           A19: p in {p} by TARSKI:def 1;

          

           A20: pc = c by A18, XTUPLE_0: 1;

          then pa reduces_to (pc, {p},T) by A10, A15, POLYRED:def 13;

          then ex p9 be Polynomial of n, L st p9 in {p} & pa reduces_to (pc,p9,T) by POLYRED:def 7;

          then

           A21: pa reduces_to (pc,p,T) by TARSKI:def 1;

          now

            per cases ;

              case

               A22: pb = ( 0_ (n,L));

              then

              consider mb be Monomial of n, L such that

               A23: ( 0_ (n,L)) = (pa - (mb *' p)) by A16, Th1;

              (( 0_ (n,L)) + (mb *' p)) = ((pa + ( - (mb *' p))) + (mb *' p)) by A23, POLYNOM1:def 7;

              then (mb *' p) = ((pa + ( - (mb *' p))) + (mb *' p)) by POLYRED: 2;

              then (mb *' p) = (pa + (( - (mb *' p)) + (mb *' p))) by POLYNOM1: 21;

              then (mb *' p) = (pa + ( 0_ (n,L))) by POLYRED: 3;

              then (mb *' p) = pa by POLYNOM1: 23;

              then

              consider mc be Monomial of n, L such that

               A24: pc = ((mb *' p) - (mc *' p)) by A21, Th1;

              pc = ((mb *' p) + ( - (mc *' p))) by A24, POLYNOM1:def 7;

              then pc = ((mb *' p) + (( - mc) *' p)) by POLYRED: 6;

              then

               A25: pc = ((mb + ( - mc)) *' p) by POLYNOM1: 26;

              then

               A26: pc = ((mb - mc) *' p) by POLYNOM1:def 7;

              now

                per cases ;

                  case mb = mc;

                  then pc = (( 0_ (n,L)) *' p) by A26, POLYNOM1: 24;

                  then pc = ( 0_ (n,L)) by POLYRED: 5;

                  hence ex d be set st R reduces (b,d) & R reduces (c,d) by A14, A20, A22, REWRITE1: 12;

                end;

                  case mb <> mc;

                  R reduces (pb,( 0_ (n,L))) by A22, REWRITE1: 12;

                  hence ex d be set st R reduces (b,d) & R reduces (c,d) by A14, A20, A19, A25, POLYRED: 45;

                end;

              end;

              hence ex d be set st R reduces (b,d) & R reduces (c,d);

            end;

              case

               A27: pc = ( 0_ (n,L));

              then

              consider mc be Monomial of n, L such that

               A28: ( 0_ (n,L)) = (pa - (mc *' p)) by A21, Th1;

              (( 0_ (n,L)) + (mc *' p)) = ((pa + ( - (mc *' p))) + (mc *' p)) by A28, POLYNOM1:def 7;

              then (mc *' p) = ((pa + ( - (mc *' p))) + (mc *' p)) by POLYRED: 2;

              then (mc *' p) = (pa + (( - (mc *' p)) + (mc *' p))) by POLYNOM1: 21;

              then (mc *' p) = (pa + ( 0_ (n,L))) by POLYRED: 3;

              then (mc *' p) = pa by POLYNOM1: 23;

              then

              consider mb be Monomial of n, L such that

               A29: pb = ((mc *' p) - (mb *' p)) by A16, Th1;

              pb = ((mc *' p) + ( - (mb *' p))) by A29, POLYNOM1:def 7;

              then pb = ((mc *' p) + (( - mb) *' p)) by POLYRED: 6;

              then

               A30: pb = ((mc + ( - mb)) *' p) by POLYNOM1: 26;

              then

               A31: pb = ((mc - mb) *' p) by POLYNOM1:def 7;

              now

                per cases ;

                  case mb = mc;

                  then pb = (( 0_ (n,L)) *' p) by A31, POLYNOM1: 24;

                  then pb = ( 0_ (n,L)) by POLYRED: 5;

                  hence ex d be set st R reduces (b,d) & R reduces (c,d) by A14, A20, A27, REWRITE1: 12;

                end;

                  case mb <> mc;

                  R reduces (pc,( 0_ (n,L))) by A27, REWRITE1: 12;

                  hence ex d be set st R reduces (b,d) & R reduces (c,d) by A14, A20, A19, A30, POLYRED: 45;

                end;

              end;

              hence ex d be set st R reduces (b,d) & R reduces (c,d);

            end;

              case not (pb = ( 0_ (n,L)) or pc = ( 0_ (n,L)));

              then

              reconsider pb, pc as non-zero Polynomial of n, L by POLYNOM7:def 1;

              now

                per cases ;

                  case pb = pc;

                  hence ex d be set st R reduces (b,d) & R reduces (c,d) by A14, A20, REWRITE1: 12;

                end;

                  case

                   A32: pb <> pc;

                  now

                    assume (pb - pc) = ( 0_ (n,L));

                    then ((pb + ( - pc)) + pc) = (( 0_ (n,L)) + pc) by POLYNOM1:def 7;

                    then (pb + (( - pc) + pc)) = (( 0_ (n,L)) + pc) by POLYNOM1: 21;

                    then (pb + ( 0_ (n,L))) = (( 0_ (n,L)) + pc) by POLYRED: 3;

                    then (pb + ( 0_ (n,L))) = pc by POLYRED: 2;

                    hence contradiction by A32, POLYNOM1: 23;

                  end;

                  then

                  reconsider h = (pb - pc) as non-zero Polynomial of n, L by POLYNOM7:def 1;

                  consider mb be Monomial of n, L such that

                   A33: pb = (pa - (mb *' p)) by A16, Th1;

                  consider mc be Monomial of n, L such that

                   A34: pc = (pa - (mc *' p)) by A21, Th1;

                  now

                    assume (( - mb) + mc) = ( 0_ (n,L));

                    then (mc + (( - mb) + mb)) = (( 0_ (n,L)) + mb) by POLYNOM1: 21;

                    then (mc + ( 0_ (n,L))) = (( 0_ (n,L)) + mb) by POLYRED: 3;

                    then (mc + ( 0_ (n,L))) = mb by POLYRED: 2;

                    hence contradiction by A32, A33, A34, POLYNOM1: 23;

                  end;

                  then

                  reconsider hh = (( - mb) + mc) as non-zero Polynomial of n, L by POLYNOM7:def 1;

                  

                   A35: ( - ( - (mc *' p))) = (mc *' p) by POLYNOM1: 19;

                  h = ((pa - (mb *' p)) + ( - (pa - (mc *' p)))) by A33, A34, POLYNOM1:def 7

                  .= ((pa - (mb *' p)) + ( - (pa + ( - (mc *' p))))) by POLYNOM1:def 7

                  .= ((pa - (mb *' p)) + (( - pa) + ( - ( - (mc *' p))))) by POLYRED: 1

                  .= ((pa + ( - (mb *' p))) + (( - pa) + ( - ( - (mc *' p))))) by POLYNOM1:def 7

                  .= (((pa + ( - (mb *' p))) + ( - pa)) + (mc *' p)) by A35, POLYNOM1: 21

                  .= (((pa + ( - pa)) + ( - (mb *' p))) + (mc *' p)) by POLYNOM1: 21

                  .= ((( 0_ (n,L)) + ( - (mb *' p))) + (mc *' p)) by POLYRED: 3

                  .= (( - (mb *' p)) + (mc *' p)) by POLYRED: 2

                  .= ((( - mb) *' p) + (mc *' p)) by POLYRED: 6

                  .= (hh *' p) by POLYNOM1: 26;

                  then

                  consider f1,g1 be Polynomial of n, L such that

                   A36: (f1 - g1) = ( 0_ (n,L)) and

                   A37: R reduces (pb,f1) & R reduces (pc,g1) by A19, POLYRED: 45, POLYRED: 49;

                  ((f1 + ( - g1)) + g1) = (( 0_ (n,L)) + g1) by A36, POLYNOM1:def 7;

                  then (f1 + (( - g1) + g1)) = (( 0_ (n,L)) + g1) by POLYNOM1: 21;

                  then (f1 + ( 0_ (n,L))) = (( 0_ (n,L)) + g1) by POLYRED: 3;

                  then (f1 + ( 0_ (n,L))) = g1 by POLYRED: 2;

                  then f1 = g1 by POLYNOM1: 23;

                  hence ex d be set st R reduces (b,d) & R reduces (c,d) by A14, A20, A37;

                end;

              end;

              hence ex d be set st R reduces (b,d) & R reduces (c,d);

            end;

          end;

          hence (b,c) are_convergent_wrt R by REWRITE1:def 7;

        end;

        hence thesis by REWRITE1:def 24;

      end;

    end;

    theorem :: GROEB_1:11

    for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)) st ex p be Polynomial of n, L st p in P & (P -Ideal ) = ( {p} -Ideal ) holds ( PolyRedRel (P,T)) is locally-confluent

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T));

      assume ex p be Polynomial of n, L st p in P & (P -Ideal ) = ( {p} -Ideal );

      then

      consider p be Polynomial of n, L such that

       A1: p in P and

       A2: (P -Ideal ) = ( {p} -Ideal );

      now

        set Rp = ( PolyRedRel ( {p},T));

        reconsider Rp as locally-confluent strongly-normalizing Relation by Th10;

        let a,b,c be object;

        assume that

         A3: [a, b] in R and

         A4: [a, c] in R;

        (a,b) are_convertible_wrt R by A3, REWRITE1: 29;

        then

         A5: (b,a) are_convertible_wrt R by REWRITE1: 31;

        consider pa,pb be object such that pa in ( NonZero ( Polynom-Ring (n,L))) and

         A6: pb in the carrier of ( Polynom-Ring (n,L)) and

         A7: [a, b] = [pa, pb] by A3, ZFMISC_1:def 2;

        reconsider pb as Polynomial of n, L by A6, POLYNOM1:def 11;

        

         A8: pb = b by A7, XTUPLE_0: 1;

        consider pa9,pc be object such that pa9 in ( NonZero ( Polynom-Ring (n,L))) and

         A9: pc in the carrier of ( Polynom-Ring (n,L)) and

         A10: [a, c] = [pa9, pc] by A4, ZFMISC_1:def 2;

        reconsider pc as Polynomial of n, L by A9, POLYNOM1:def 11;

        

         A11: pc = c by A10, XTUPLE_0: 1;

        reconsider pb9 = pb, pc9 = pc as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        reconsider pc9, pb9 as Element of ( Polynom-Ring (n,L));

        (a,c) are_convertible_wrt R by A4, REWRITE1: 29;

        then (pb9,pc9) are_congruent_mod ( {p} -Ideal ) by A2, A8, A11, A5, POLYRED: 57, REWRITE1: 30;

        then (pb,pc) are_convertible_wrt ( PolyRedRel ( {p},T)) by POLYRED: 58;

        then (b,c) are_convergent_wrt Rp by A8, A11, REWRITE1:def 23;

        then

        consider d be object such that

         A12: Rp reduces (b,d) & Rp reduces (c,d) by REWRITE1:def 7;

        for u be object holds u in {p} implies u in P by A1, TARSKI:def 1;

        then {p} c= P;

        then R reduces (b,d) & R reduces (c,d) by A12, Th4, REWRITE1: 22;

        hence (b,c) are_convergent_wrt R by REWRITE1:def 7;

      end;

      hence thesis by REWRITE1:def 24;

    end;

    definition

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      :: GROEB_1:def1

      func HT (P,T) -> Subset of ( Bags n) equals { ( HT (p,T)) where p be Polynomial of n, L : p in P & p <> ( 0_ (n,L)) };

      coherence

      proof

        set M = { ( HT (p,T)) where p be Polynomial of n, L : p in P & p <> ( 0_ (n,L)) };

        now

          let u be object;

          assume u in M;

          then ex p be Polynomial of n, L st u = ( HT (p,T)) & p in P & p <> ( 0_ (n,L));

          hence u in ( Bags n);

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let n be Ordinal, S be Subset of ( Bags n);

      :: GROEB_1:def2

      func multiples (S) -> Subset of ( Bags n) equals { b where b be Element of ( Bags n) : ex b9 be bag of n st b9 in S & b9 divides b };

      coherence

      proof

        set M = { b where b be Element of ( Bags n) : ex b9 be bag of n st b9 in S & b9 divides b };

        now

          let u be object;

          assume u in M;

          then ex b be Element of ( Bags n) st u = b & ex b9 be bag of n st b9 in S & b9 divides b;

          hence u in ( Bags n);

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: GROEB_1:12

    for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)) holds ( PolyRedRel (P,T)) is locally-confluent implies ( PolyRedRel (P,T)) is confluent;

    theorem :: GROEB_1:13

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)) holds ( PolyRedRel (P,T)) is confluent implies ( PolyRedRel (P,T)) is with_UN_property;

    theorem :: GROEB_1:14

    for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)) holds ( PolyRedRel (P,T)) is with_UN_property implies ( PolyRedRel (P,T)) is with_Church-Rosser_property;

    

     Lm4: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L, g be object, P be 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 almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L, g be object, P be Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T));

      assume R reduces (f,g);

      then

      consider p be RedSequence of R such that

       A1: (p . 1) = f and

       A2: (p . ( len p)) = g by REWRITE1:def 3;

      reconsider l = (( len p) - 1) as Element of NAT by INT_1: 5, NAT_1: 14;

      

       A3: 1 <= ( len p) by NAT_1: 14;

      set h = (p . l);

      1 <= (l + 1) by NAT_1: 12;

      then (l + 1) in ( Seg ( len p)) by FINSEQ_1: 1;

      then

       A4: (l + 1) in ( dom p) by FINSEQ_1:def 3;

      per cases ;

        suppose ( len p) = 1;

        hence thesis by A1, A2;

      end;

        suppose ( len p) <> 1;

        then ( 0 + 1) < (l + 1) by A3, XXREAL_0: 1;

        then

         A5: 1 <= l by NAT_1: 13;

        l <= (l + 1) by NAT_1: 13;

        then l in ( Seg ( len p)) by A5, FINSEQ_1: 1;

        then l in ( dom p) by FINSEQ_1:def 3;

        then [h, g] in R by A2, A4, REWRITE1:def 2;

        then

        consider h9,g9 be object such that

         A6: [h, g] = [h9, g9] and h9 in ( NonZero ( Polynom-Ring (n,L))) and

         A7: g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

        g = g9 by A6, XTUPLE_0: 1;

        hence thesis by A7, POLYNOM1:def 11;

      end;

    end;

    

     Lm5: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,g be Polynomial of n, L, P be Subset of ( Polynom-Ring (n,L)) holds ( PolyRedRel (P,T)) reduces (f,g) & g <> f implies ex h be Polynomial of n, L st f reduces_to (h,P,T) & ( PolyRedRel (P,T)) reduces (h,g)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,g be Polynomial of n, L, P be Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T));

      assume that

       A1: ( PolyRedRel (P,T)) reduces (f,g) and

       A2: g <> f;

      consider p be RedSequence of R such that

       A3: (p . 1) = f and

       A4: (p . ( len p)) = g by A1, REWRITE1:def 3;

      set h = (p . 2);

      ( len p) > 0 ;

      then (( len p) + 1) > ( 0 + 1) by XREAL_1: 8;

      then

       A5: 1 <= ( len p) by NAT_1: 13;

      then 1 < ( len p) by A2, A3, A4, XXREAL_0: 1;

      then

       A6: (1 + 1) <= ( len p) by NAT_1: 13;

      then (1 + 1) in ( Seg ( len p)) by FINSEQ_1: 1;

      then

       A7: (1 + 1) in ( dom p) by FINSEQ_1:def 3;

      1 in ( Seg ( len p)) by A5, FINSEQ_1: 1;

      then 1 in ( dom p) by FINSEQ_1:def 3;

      then

       A8: [f, h] in R by A3, A7, REWRITE1:def 2;

      then

      consider f9,h9 be object such that

       A9: [f, h] = [f9, h9] and f9 in ( NonZero ( Polynom-Ring (n,L))) and

       A10: h9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

      

       A11: h = h9 by A9, XTUPLE_0: 1;

      ( len p) in ( Seg ( len p)) by A5, FINSEQ_1: 1;

      then

       A12: ( len p) in ( dom p) by FINSEQ_1:def 3;

      reconsider h as Polynomial of n, L by A10, A11, POLYNOM1:def 11;

      f reduces_to (h,P,T) by A8, POLYRED:def 13;

      hence thesis by A4, A6, A7, A12, REWRITE1: 17;

    end;

    theorem :: GROEB_1:15

    

     Th15: for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, P be non empty Subset of ( Polynom-Ring (n,L)) holds ( PolyRedRel (P,T)) is with_Church-Rosser_property implies (for f be Polynomial of n, L st f in (P -Ideal ) holds ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L))))

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be non empty Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T));

      assume

       A1: ( PolyRedRel (P,T)) is with_Church-Rosser_property;

      now

        reconsider e = ( 0_ (n,L)) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        let f be Polynomial of n, L;

        assume

         A2: f in (P -Ideal );

        reconsider e as Element of ( Polynom-Ring (n,L));

        reconsider f9 = f as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        reconsider f9 as Element of ( Polynom-Ring (n,L));

        (f - ( 0_ (n,L))) = (f9 - e) by Lm2;

        then (f9 - e) in (P -Ideal ) by A2, POLYRED: 4;

        then (f9,e) are_congruent_mod (P -Ideal ) by POLYRED:def 14;

        then (f9,e) are_convertible_wrt R by POLYRED: 58;

        then (f9,e) are_convergent_wrt R by A1, REWRITE1:def 23;

        then

        consider c be object such that

         A3: R reduces (f,c) and

         A4: R reduces (( 0_ (n,L)),c) by REWRITE1:def 7;

        reconsider c9 = c as Polynomial of n, L by A3, Lm4;

        now

          assume c9 <> ( 0_ (n,L));

          then

          consider h be Polynomial of n, L such that

           A5: ( 0_ (n,L)) reduces_to (h,P,T) and ( PolyRedRel (P,T)) reduces (h,c9) by A4, Lm5;

          consider pp be Polynomial of n, L such that pp in P and

           A6: ( 0_ (n,L)) reduces_to (h,pp,T) by A5, POLYRED:def 7;

          ( 0_ (n,L)) is_reducible_wrt (pp,T) by A6, POLYRED:def 8;

          hence contradiction by POLYRED: 37;

        end;

        hence R reduces (f,( 0_ (n,L))) by A3;

      end;

      hence thesis;

    end;

    theorem :: GROEB_1:16

    

     Th16: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)) holds (for f be Polynomial of n, L st f in (P -Ideal ) holds ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L)))) implies (for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f is_reducible_wrt (P,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 almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      assume

       A1: for f be Polynomial of n, L st f in (P -Ideal ) holds ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L)));

      now

        let f be non-zero Polynomial of n, L;

        assume f in (P -Ideal );

        then

         A2: ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L))) by A1;

        f <> ( 0_ (n,L)) by POLYNOM7:def 1;

        then ex g be Polynomial of n, L st f reduces_to (g,P,T) & ( PolyRedRel (P,T)) reduces (g,( 0_ (n,L))) by A2, Lm5;

        hence f is_reducible_wrt (P,T) by POLYRED:def 9;

      end;

      hence thesis;

    end;

    theorem :: GROEB_1:17

    

     Th17: for n be Element of NAT , T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)) holds (for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f is_reducible_wrt (P,T)) implies (for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f is_top_reducible_wrt (P,T))

    proof

      let n be Element of NAT , T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      assume

       A1: for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f is_reducible_wrt (P,T);

      thus for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f is_top_reducible_wrt (P,T)

      proof

        set H = { g where g be non-zero Polynomial of n, L : g in (P -Ideal ) & not (g is_top_reducible_wrt (P,T)) };

        let f be non-zero Polynomial of n, L;

        assume

         A2: f in (P -Ideal );

        assume not f is_top_reducible_wrt (P,T);

        then

         A3: f in H by A2;

        now

          let u be object;

          assume u in H;

          then ex g9 be non-zero Polynomial of n, L st u = g9 & g9 in (P -Ideal ) & not g9 is_top_reducible_wrt (P,T);

          hence u in the carrier of ( Polynom-Ring (n,L));

        end;

        then

        reconsider H as non empty Subset of ( Polynom-Ring (n,L)) by A3, TARSKI:def 3;

        consider p be Polynomial of n, L such that

         A4: p in H and

         A5: for q be Polynomial of n, L st q in H holds p <= (q,T) by POLYRED: 31;

        

         A6: ex p9 be non-zero Polynomial of n, L st p9 = p & p9 in (P -Ideal ) & not p9 is_top_reducible_wrt (P,T) by A4;

        then

        reconsider p as non-zero Polynomial of n, L;

        p is_reducible_wrt (P,T) by A1, A6;

        then

        consider q be Polynomial of n, L such that

         A7: p reduces_to (q,P,T) by POLYRED:def 9;

        consider u be Polynomial of n, L such that

         A8: u in P and

         A9: p reduces_to (q,u,T) by A7, POLYRED:def 7;

        ex b be bag of n st p reduces_to (q,u,b,T) by A9, POLYRED:def 6;

        then

         A10: u <> ( 0_ (n,L)) by POLYRED:def 5;

        then

        reconsider u as non-zero Polynomial of n, L by POLYNOM7:def 1;

        consider b be bag of n such that

         A11: p reduces_to (q,u,b,T) by A9, POLYRED:def 6;

         A12:

        now

          assume b = ( HT (p,T));

          then p top_reduces_to (q,u,T) by A11, POLYRED:def 10;

          then p is_top_reducible_wrt (u,T) by POLYRED:def 11;

          hence contradiction by A6, A8, POLYRED:def 12;

        end;

        consider m be Monomial of n, L such that

         A13: q = (p - (m *' u)) by A9, Th1;

        reconsider uu = u, pp = p, mm = m as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        reconsider uu, pp, mm as Element of ( Polynom-Ring (n,L));

        uu in (P -Ideal ) by A8, Lm1;

        then (mm * uu) in (P -Ideal ) by IDEAL_1:def 2;

        then ( - (mm * uu)) in (P -Ideal ) by IDEAL_1: 13;

        then

         A14: (pp + ( - (mm * uu))) in (P -Ideal ) by A6, IDEAL_1:def 1;

        (mm * uu) = (m *' u) by POLYNOM1:def 11;

        then (p - (m *' u)) = (pp - (mm * uu)) by Lm2;

        then

         A15: q in (P -Ideal ) by A13, A14;

        

         A16: q < (p,T) by A9, POLYRED: 43;

        

         A17: p <> ( 0_ (n,L)) by POLYNOM7:def 1;

        then ( Support p) <> {} by POLYNOM7: 1;

        then

         A18: ( HT (p,T)) in ( Support p) by TERMORD:def 6;

        b in ( Support p) by A11, POLYRED:def 5;

        then b <= (( HT (p,T)),T) by TERMORD:def 6;

        then b < (( HT (p,T)),T) by A12, TERMORD:def 3;

        then

         A19: ( HT (p,T)) in ( Support q) by A18, A11, POLYRED: 40;

        now

          per cases ;

            case

             A20: q <> ( 0_ (n,L));

            then

            reconsider q as non-zero Polynomial of n, L by POLYNOM7:def 1;

            ( Support q) <> {} by A20, POLYNOM7: 1;

            then ( HT (q,T)) in ( Support q) by TERMORD:def 6;

            then

             A21: ( HT (q,T)) <= (( HT (p,T)),T) by A9, POLYRED: 42;

            ( HT (p,T)) <= (( HT (q,T)),T) by A19, TERMORD:def 6;

            then

             A22: ( HT (q,T)) = ( HT (p,T)) by A21, TERMORD: 7;

            now

              assume not q is_top_reducible_wrt (P,T);

              then q in H by A15;

              then p <= (q,T) by A5;

              hence contradiction by A16, POLYRED: 29;

            end;

            then

            consider u9 be Polynomial of n, L such that

             A23: u9 in P and

             A24: q is_top_reducible_wrt (u9,T) by POLYRED:def 12;

            consider q9 be Polynomial of n, L such that

             A25: q top_reduces_to (q9,u9,T) by A24, POLYRED:def 11;

            

             A26: p <> ( 0_ (n,L)) by POLYNOM7:def 1;

            then ( Support p) <> {} by POLYNOM7: 1;

            then

             A27: ( HT (p,T)) in ( Support p) by TERMORD:def 6;

            

             A28: q reduces_to (q9,u9,( HT (q,T)),T) by A25, POLYRED:def 10;

            then

            consider s be bag of n such that

             A29: (s + ( HT (u9,T))) = ( HT (q,T)) and q9 = (q - (((q . ( HT (q,T))) / ( HC (u9,T))) * (s *' u9))) by POLYRED:def 5;

            set qq = (p - (((p . ( HT (p,T))) / ( HC (u9,T))) * (s *' u9)));

            u9 <> ( 0_ (n,L)) by A28, POLYRED:def 5;

            then p reduces_to (qq,u9,( HT (p,T)),T) by A22, A29, A26, A27, POLYRED:def 5;

            then p top_reduces_to (qq,u9,T) by POLYRED:def 10;

            then p is_top_reducible_wrt (u9,T) by POLYRED:def 11;

            hence contradiction by A6, A23, POLYRED:def 12;

          end;

            case q = ( 0_ (n,L));

            

            then

             A30: (m *' u) = ((p - (m *' u)) + (m *' u)) by A13, POLYRED: 2

            .= ((p + ( - (m *' u))) + (m *' u)) by POLYNOM1:def 7

            .= (p + (( - (m *' u)) + (m *' u))) by POLYNOM1: 21

            .= (p + ( 0_ (n,L))) by POLYRED: 3

            .= p by POLYNOM1: 23;

            m <> ( 0_ (n,L)) by POLYNOM7:def 1, A30, POLYRED: 5;

            then

            reconsider m as non-zero Polynomial of n, L by POLYNOM7:def 1;

            set pp = (p - (((p . ( HT (p,T))) / ( HC (u,T))) * (( HT (m,T)) *' u)));

            ( HT (p,T)) = (( HT (m,T)) + ( HT (u,T))) by A30, TERMORD: 31;

            then p reduces_to (pp,u,( HT (p,T)),T) by A10, A17, A18, POLYRED:def 5;

            then p top_reduces_to (pp,u,T) by POLYRED:def 10;

            then p is_top_reducible_wrt (u,T) by POLYRED:def 11;

            hence contradiction by A6, A8, POLYRED:def 12;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: GROEB_1:18

    

     Th18: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)) holds (for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f is_top_reducible_wrt (P,T)) implies (for b be bag of n st b in ( HT ((P -Ideal ),T)) holds ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      assume

       A1: for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f is_top_reducible_wrt (P,T);

      now

        let b be bag of n;

        assume b in ( HT ((P -Ideal ),T));

        then

        consider p be Polynomial of n, L such that

         A2: b = ( HT (p,T)) and

         A3: p in (P -Ideal ) and

         A4: p <> ( 0_ (n,L));

        reconsider p as non-zero Polynomial of n, L by A4, POLYNOM7:def 1;

        p is_top_reducible_wrt (P,T) by A1, A3;

        then

        consider u be Polynomial of n, L such that

         A5: u in P and

         A6: p is_top_reducible_wrt (u,T) by POLYRED:def 12;

        consider q be Polynomial of n, L such that

         A7: p top_reduces_to (q,u,T) by A6, POLYRED:def 11;

        

         A8: p reduces_to (q,u,( HT (p,T)),T) by A7, POLYRED:def 10;

        then u <> ( 0_ (n,L)) by POLYRED:def 5;

        then

         A9: ( HT (u,T)) in { ( HT (r,T)) where r be Polynomial of n, L : r in P & r <> ( 0_ (n,L)) } by A5;

        ex s be bag of n st (s + ( HT (u,T))) = ( HT (p,T)) & q = (p - (((p . ( HT (p,T))) / ( HC (u,T))) * (s *' u))) by A8, POLYRED:def 5;

        hence ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b by A2, A9, PRE_POLY: 50;

      end;

      hence thesis;

    end;

    theorem :: GROEB_1:19

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)) holds (for b be bag of n st b in ( HT ((P -Ideal ),T)) holds ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b) implies ( HT ((P -Ideal ),T)) c= ( multiples ( HT (P,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 almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      assume

       A1: for b be bag of n st b in ( HT ((P -Ideal ),T)) holds ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b;

      let u be object;

      assume

       A2: u in ( HT ((P -Ideal ),T));

      then

      reconsider u9 = u as Element of ( Bags n);

      ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides u9 by A1, A2;

      hence u in ( multiples ( HT (P,T)));

    end;

    theorem :: GROEB_1:20

    for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)) holds ( HT ((P -Ideal ),T)) c= ( multiples ( HT (P,T))) implies ( PolyRedRel (P,T)) is locally-confluent

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T));

      assume

       A1: ( HT ((P -Ideal ),T)) c= ( multiples ( HT (P,T)));

      

       A2: for f be Polynomial of n, L st f in (P -Ideal ) & f <> ( 0_ (n,L)) holds f is_reducible_wrt (P,T)

      proof

        let f be Polynomial of n, L;

        assume that

         A3: f in (P -Ideal ) and

         A4: f <> ( 0_ (n,L));

        ( HT (f,T)) in { ( HT (p,T)) where p be Polynomial of n, L : p in (P -Ideal ) & p <> ( 0_ (n,L)) } by A3, A4;

        then ( HT (f,T)) in ( multiples ( HT (P,T))) by A1;

        then ex b be Element of ( Bags n) st b = ( HT (f,T)) & ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b;

        then

        consider b9 be bag of n such that

         A5: b9 in ( HT (P,T)) and

         A6: b9 divides ( HT (f,T));

        consider p be Polynomial of n, L such that

         A7: b9 = ( HT (p,T)) and

         A8: p in P and

         A9: p <> ( 0_ (n,L)) by A5;

        consider s be bag of n such that

         A10: (b9 + s) = ( HT (f,T)) by A6, TERMORD: 1;

        set g = (f - (((f . ( HT (f,T))) / ( HC (p,T))) * (s *' p)));

        ( Support f) <> {} by A4, POLYNOM7: 1;

        then ( HT (f,T)) in ( Support f) by TERMORD:def 6;

        then f reduces_to (g,p,( HT (f,T)),T) by A4, A7, A9, A10, POLYRED:def 5;

        then f reduces_to (g,p,T) by POLYRED:def 6;

        then f reduces_to (g,P,T) by A8, POLYRED:def 7;

        hence thesis by POLYRED:def 9;

      end;

      

       A11: for f be Polynomial of n, L st f in (P -Ideal ) holds R reduces (f,( 0_ (n,L)))

      proof

        let f be Polynomial of n, L;

        assume

         A12: f in (P -Ideal );

        per cases ;

          suppose f = ( 0_ (n,L));

          hence thesis by REWRITE1: 12;

        end;

          suppose f <> ( 0_ (n,L));

          then f is_reducible_wrt (P,T) by A2, A12;

          then

          consider v be Polynomial of n, L such that

           A13: f reduces_to (v,P,T) by POLYRED:def 9;

           [f, v] in R by A13, POLYRED:def 13;

          then f in ( field R) by RELAT_1: 15;

          then f has_a_normal_form_wrt R by REWRITE1:def 14;

          then

          consider g be object such that

           A14: g is_a_normal_form_of (f,R) by REWRITE1:def 11;

          

           A15: R reduces (f,g) by A14, REWRITE1:def 6;

          then

          reconsider g9 = g as Polynomial of n, L by Lm4;

          reconsider ff = f, gg = g9 as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

          reconsider ff, gg as Element of ( Polynom-Ring (n,L));

          (f - g9) = (ff - gg) by Lm2;

          then (ff - gg) in (P -Ideal ) by A15, POLYRED: 59;

          then

           A16: ((ff - gg) - ff) in (P -Ideal ) by A12, IDEAL_1: 16;

          ((ff - gg) - ff) = ((ff + ( - gg)) - ff)

          .= ((ff + ( - gg)) + ( - ff))

          .= ((ff + ( - ff)) + ( - gg)) by RLVECT_1:def 3

          .= (( 0. ( Polynom-Ring (n,L))) + ( - gg)) by RLVECT_1: 5

          .= ( - gg) by ALGSTR_1:def 2;

          then ( - ( - gg)) in (P -Ideal ) by A16, IDEAL_1: 14;

          then

           A17: g in (P -Ideal ) by RLVECT_1: 17;

          assume not R reduces (f,( 0_ (n,L)));

          then g <> ( 0_ (n,L)) by A14, REWRITE1:def 6;

          then g9 is_reducible_wrt (P,T) by A2, A17;

          then

          consider u be Polynomial of n, L such that

           A18: g9 reduces_to (u,P,T) by POLYRED:def 9;

          

           A19: [g9, u] in R by A18, POLYRED:def 13;

          g is_a_normal_form_wrt R by A14, REWRITE1:def 6;

          hence contradiction by A19, REWRITE1:def 5;

        end;

      end;

      now

        let a,b,c be object;

        assume that

         A20: [a, b] in R and

         A21: [a, c] in R;

        consider a9,b9 be object such that a9 in ( NonZero ( Polynom-Ring (n,L))) and

         A22: b9 in the carrier of ( Polynom-Ring (n,L)) and

         A23: [a, b] = [a9, b9] by A20, ZFMISC_1:def 2;

        

         A24: b9 = b by A23, XTUPLE_0: 1;

        (a,b) are_convertible_wrt R by A20, REWRITE1: 29;

        then

         A25: (b,a) are_convertible_wrt R by REWRITE1: 31;

        consider aa,c9 be object such that aa in ( NonZero ( Polynom-Ring (n,L))) and

         A26: c9 in the carrier of ( Polynom-Ring (n,L)) and

         A27: [a, c] = [aa, c9] by A21, ZFMISC_1:def 2;

        

         A28: c9 = c by A27, XTUPLE_0: 1;

        reconsider b9, c9 as Polynomial of n, L by A22, A26, POLYNOM1:def 11;

        reconsider bb = b9, cc = c9 as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        reconsider bb, cc as Element of ( Polynom-Ring (n,L));

        (a,c) are_convertible_wrt R by A21, REWRITE1: 29;

        then (bb,cc) are_congruent_mod (P -Ideal ) by A24, A28, A25, POLYRED: 57, REWRITE1: 30;

        then

         A29: (bb - cc) in (P -Ideal ) by POLYRED:def 14;

        (b9 - c9) = (bb - cc) by Lm2;

        hence (b,c) are_convergent_wrt R by A11, A24, A28, A29, POLYRED: 50;

      end;

      hence thesis by REWRITE1:def 24;

    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 almost_left_invertible non trivial doubleLoopStr, G be Subset of ( Polynom-Ring (n,L));

      :: GROEB_1:def3

      pred G is_Groebner_basis_wrt T means ( PolyRedRel (G,T)) is locally-confluent;

    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 almost_left_invertible non trivial doubleLoopStr, G,I be Subset of ( Polynom-Ring (n,L));

      :: GROEB_1:def4

      pred G is_Groebner_basis_of I,T means (G -Ideal ) = I & ( PolyRedRel (G,T)) is locally-confluent;

    end

    

     Lm6: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), a,b be object st a <> b holds ( PolyRedRel (P,T)) reduces (a,b) implies a is Polynomial of n, L & b 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 almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be object;

      set R = ( PolyRedRel (P,T));

      assume

       A1: f <> g;

      assume R reduces (f,g);

      then

      consider p be RedSequence of R such that

       A2: (p . 1) = f and

       A3: (p . ( len p)) = g by REWRITE1:def 3;

      reconsider l = (( len p) - 1) as Element of NAT by INT_1: 5, NAT_1: 14;

      set q = (p . (1 + 1)), h = (p . l);

      

       A4: 1 <= ( len p) by NAT_1: 14;

      now

        per cases ;

          case ( len p) = 1;

          hence f is Polynomial of n, L by A1, A2, A3;

        end;

          case ( len p) <> 1;

          then 1 < ( len p) by A4, XXREAL_0: 1;

          then (1 + 1) <= ( len p) by NAT_1: 13;

          then (1 + 1) in ( Seg ( len p)) by FINSEQ_1: 1;

          then

           A5: (1 + 1) in ( dom p) by FINSEQ_1:def 3;

          1 in ( Seg ( len p)) by A4, FINSEQ_1: 1;

          then 1 in ( dom p) by FINSEQ_1:def 3;

          then [f, q] in R by A2, A5, REWRITE1:def 2;

          then

          consider h9,g9 be object such that

           A6: [f, q] = [h9, g9] and

           A7: h9 in ( NonZero ( Polynom-Ring (n,L))) and g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

          f = h9 by A6, XTUPLE_0: 1;

          hence f is Polynomial of n, L by A7, POLYNOM1:def 11;

        end;

      end;

      hence f is Polynomial of n, L;

      1 <= (l + 1) by NAT_1: 12;

      then (l + 1) in ( Seg ( len p)) by FINSEQ_1: 1;

      then

       A8: (l + 1) in ( dom p) by FINSEQ_1:def 3;

      now

        per cases ;

          case ( len p) = 1;

          hence thesis by A1, A2, A3;

        end;

          case ( len p) <> 1;

          then ( 0 + 1) < (l + 1) by A4, XXREAL_0: 1;

          then

           A9: 1 <= l by NAT_1: 13;

          l <= (l + 1) by NAT_1: 13;

          then l in ( Seg ( len p)) by A9, FINSEQ_1: 1;

          then l in ( dom p) by FINSEQ_1:def 3;

          then [h, g] in R by A3, A8, REWRITE1:def 2;

          then

          consider h9,g9 be object such that

           A10: [h, g] = [h9, g9] and h9 in ( NonZero ( Polynom-Ring (n,L))) and

           A11: g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

          g = g9 by A10, XTUPLE_0: 1;

          hence thesis by A11, POLYNOM1:def 11;

        end;

      end;

      hence thesis;

    end;

    theorem :: GROEB_1:21

    for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, G,P be non empty Subset of ( Polynom-Ring (n,L)) st G is_Groebner_basis_of (P,T) holds ( PolyRedRel (G,T)) is Completion of ( PolyRedRel (P,T))

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, G,P be non empty Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T));

      assume

       A1: G is_Groebner_basis_of (P,T);

      then ( PolyRedRel (G,T)) is locally-confluent;

      then

      reconsider RG = ( PolyRedRel (G,T)) as complete Relation;

      for a,b be object holds (a,b) are_convertible_wrt R iff (a,b) are_convergent_wrt RG

      proof

        let a,b be object;

        

         A2: (G -Ideal ) = P by A1;

         A3:

        now

          assume

           A4: (a,b) are_convertible_wrt R;

          now

            per cases ;

              case a = b;

              hence (a,b) are_convergent_wrt RG by REWRITE1: 38;

            end;

              case

               A5: a <> b;

              (R \/ (R ~ )) reduces (a,b) by A4, REWRITE1:def 4;

              then

              consider p be RedSequence of (R \/ (R ~ )) such that

               A6: (p . 1) = a and

               A7: (p . ( len p)) = b by REWRITE1:def 3;

              reconsider l = (( len p) - 1) as Element of NAT by INT_1: 5, NAT_1: 14;

              

               A8: 1 <= ( len p) by NAT_1: 14;

              set h = (p . l), g = (p . (1 + 1));

              1 <= (l + 1) by NAT_1: 12;

              then (l + 1) in ( Seg ( len p)) by FINSEQ_1: 1;

              then

               A9: (l + 1) in ( dom p) by FINSEQ_1:def 3;

              now

                per cases ;

                  case ( len p) = 1;

                  hence a is Polynomial of n, L & b is Polynomial of n, L by A5, A6, A7;

                end;

                  case

                   A10: ( len p) <> 1;

                  then ( 0 + 1) < (l + 1) by A8, XXREAL_0: 1;

                  then

                   A11: 1 <= l by NAT_1: 13;

                  l <= (l + 1) by NAT_1: 13;

                  then l in ( Seg ( len p)) by A11, FINSEQ_1: 1;

                  then l in ( dom p) by FINSEQ_1:def 3;

                  then

                   A12: [h, b] in (R \/ (R ~ )) by A7, A9, REWRITE1:def 2;

                   A13:

                  now

                    per cases by A12, XBOOLE_0:def 3;

                      case [h, b] in R;

                      then

                      consider h9,b9 be object such that

                       A14: [h, b] = [h9, b9] and h9 in ( NonZero ( Polynom-Ring (n,L))) and

                       A15: b9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

                      b = b9 by A14, XTUPLE_0: 1;

                      hence b is Polynomial of n, L by A15, POLYNOM1:def 11;

                    end;

                      case [h, b] in (R ~ );

                      then [b, h] in R by RELAT_1:def 7;

                      then

                      consider h9,b9 be object such that

                       A16: [b, h] = [h9, b9] and

                       A17: h9 in ( NonZero ( Polynom-Ring (n,L))) and b9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

                      b = h9 by A16, XTUPLE_0: 1;

                      hence b is Polynomial of n, L by A17, POLYNOM1:def 11;

                    end;

                  end;

                  1 < ( len p) by A8, A10, XXREAL_0: 1;

                  then (1 + 1) <= ( len p) by NAT_1: 13;

                  then (1 + 1) in ( Seg ( len p)) by FINSEQ_1: 1;

                  then

                   A18: (1 + 1) in ( dom p) by FINSEQ_1:def 3;

                  1 in ( Seg ( len p)) by A8, FINSEQ_1: 1;

                  then 1 in ( dom p) by FINSEQ_1:def 3;

                  then

                   A19: [a, g] in (R \/ (R ~ )) by A6, A18, REWRITE1:def 2;

                  now

                    per cases by A19, XBOOLE_0:def 3;

                      case [a, g] in R;

                      then

                      consider h9,b9 be object such that

                       A20: [a, g] = [h9, b9] and

                       A21: h9 in ( NonZero ( Polynom-Ring (n,L))) and b9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

                      a = h9 by A20, XTUPLE_0: 1;

                      hence a is Polynomial of n, L by A21, POLYNOM1:def 11;

                    end;

                      case [a, g] in (R ~ );

                      then [g, a] in R by RELAT_1:def 7;

                      then

                      consider h9,b9 be object such that

                       A22: [g, a] = [h9, b9] and h9 in ( NonZero ( Polynom-Ring (n,L))) and

                       A23: b9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

                      a = b9 by A22, XTUPLE_0: 1;

                      hence a is Polynomial of n, L by A23, POLYNOM1:def 11;

                    end;

                  end;

                  hence a is Polynomial of n, L & b is Polynomial of n, L by A13;

                end;

              end;

              then

              reconsider a9 = a, b9 = b as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

              reconsider a9, b9 as Element of ( Polynom-Ring (n,L));

              (G -Ideal ) = (P -Ideal ) by A2, IDEAL_1: 44;

              then (a9,b9) are_congruent_mod (G -Ideal ) by A4, POLYRED: 57;

              then (a9,b9) are_convertible_wrt RG by POLYRED: 58;

              hence (a,b) are_convergent_wrt RG by REWRITE1:def 23;

            end;

          end;

          hence (a,b) are_convergent_wrt RG;

        end;

        now

          assume

           A24: (a,b) are_convergent_wrt RG;

          now

            per cases ;

              case a = b;

              hence (a,b) are_convertible_wrt R by REWRITE1: 26;

            end;

              case

               A25: a <> b;

              consider c be object such that

               A26: RG reduces (a,c) and

               A27: RG reduces (b,c) by A24, REWRITE1:def 7;

              a is Polynomial of n, L & b is Polynomial of n, L

              proof

                now

                  per cases ;

                    case a = c;

                    hence thesis by A25, A27, Lm6;

                  end;

                    case

                     A28: a <> c;

                    now

                      per cases ;

                        case b = c;

                        hence thesis by A25, A26, Lm6;

                      end;

                        case b <> c;

                        hence b is Polynomial of n, L by A27, Lm6;

                      end;

                    end;

                    hence thesis by A26, A28, Lm6;

                  end;

                end;

                hence thesis;

              end;

              then

              reconsider a9 = a, b9 = b as Element of the carrier of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

              reconsider a9, b9 as Element of ( Polynom-Ring (n,L));

              (G -Ideal ) = (P -Ideal ) & (a9,b9) are_convertible_wrt RG by A2, A24, IDEAL_1: 44, REWRITE1: 37;

              then (a9,b9) are_congruent_mod (P -Ideal ) by POLYRED: 57;

              hence (a,b) are_convertible_wrt R by POLYRED: 58;

            end;

          end;

          hence (a,b) are_convertible_wrt R;

        end;

        hence thesis by A3;

      end;

      hence thesis by REWRITE1:def 28;

    end;

    theorem :: GROEB_1:22

    for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, p,q be Element of ( Polynom-Ring (n,L)), G be non empty Subset of ( Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds (p,q) are_congruent_mod (G -Ideal ) iff ( nf (p,( PolyRedRel (G,T)))) = ( nf (q,( PolyRedRel (G,T))))

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, p,q be Element of ( Polynom-Ring (n,L)), G be non empty Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (G,T));

      assume G is_Groebner_basis_wrt T;

      then

       A1: ( PolyRedRel (G,T)) is locally-confluent;

      now

        ( nf (q,R)) is_a_normal_form_of (q,R) by A1, REWRITE1: 54;

        then R reduces (q,( nf (q,R))) by REWRITE1:def 6;

        then

         A2: (( nf (q,R)),q) are_convertible_wrt R by REWRITE1: 25;

        ( nf (p,R)) is_a_normal_form_of (p,R) by A1, REWRITE1: 54;

        then R reduces (p,( nf (p,R))) by REWRITE1:def 6;

        then

         A3: (p,( nf (p,R))) are_convertible_wrt R by REWRITE1: 25;

        assume ( nf (p,( PolyRedRel (G,T)))) = ( nf (q,( PolyRedRel (G,T))));

        hence (p,q) are_congruent_mod (G -Ideal ) by A3, A2, POLYRED: 57, REWRITE1: 30;

      end;

      hence thesis by A1, POLYRED: 58, REWRITE1: 55;

    end;

    theorem :: GROEB_1:23

    for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)) st P is_Groebner_basis_wrt T holds f in (P -Ideal ) iff ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L))) by Th15, POLYRED: 60;

    

     Lm7: for n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, I be LeftIdeal of ( Polynom-Ring (n,L)), G be non empty Subset of ( Polynom-Ring (n,L)) st G c= I holds (for f be Polynomial of n, L st f in I holds ( PolyRedRel (G,T)) reduces (f,( 0_ (n,L)))) implies (G -Ideal ) = I

    proof

      let n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, I be LeftIdeal of ( Polynom-Ring (n,L)), G be non empty Subset of ( Polynom-Ring (n,L));

      assume

       A1: G c= I;

       A2:

      now

        let u be object;

        assume

         A3: u in (G -Ideal );

        (G -Ideal ) c= I by A1, IDEAL_1:def 14;

        hence u in I by A3;

      end;

      assume

       A4: for f be Polynomial of n, L st f in I holds ( PolyRedRel (G,T)) reduces (f,( 0_ (n,L)));

      now

        let u be object;

        assume

         A5: u in I;

        then

        reconsider u9 = u as Element of ( Polynom-Ring (n,L));

        reconsider u9 as Polynomial of n, L by POLYNOM1:def 11;

        ( PolyRedRel (G,T)) reduces (u9,( 0_ (n,L))) by A4, A5;

        hence u in (G -Ideal ) by POLYRED: 60;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: GROEB_1:24

    

     Th24: for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, I be Subset of ( Polynom-Ring (n,L)), G be non empty Subset of ( Polynom-Ring (n,L)) holds G is_Groebner_basis_of (I,T) implies (for f be Polynomial of n, L st f in I holds ( PolyRedRel (G,T)) reduces (f,( 0_ (n,L)))) by Th15;

    theorem :: GROEB_1:25

    

     Th25: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, G,I be Subset of ( Polynom-Ring (n,L)) holds (for f be Polynomial of n, L st f in I holds ( PolyRedRel (G,T)) reduces (f,( 0_ (n,L)))) implies (for f be non-zero Polynomial of n, L st f in I holds f is_reducible_wrt (G,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 almost_left_invertible non trivial doubleLoopStr, G,I be Subset of ( Polynom-Ring (n,L));

      assume

       A1: for f be Polynomial of n, L st f in I holds ( PolyRedRel (G,T)) reduces (f,( 0_ (n,L)));

      now

        let f be non-zero Polynomial of n, L;

        assume f in I;

        then

         A2: ( PolyRedRel (G,T)) reduces (f,( 0_ (n,L))) by A1;

        f <> ( 0_ (n,L)) by POLYNOM7:def 1;

        then ex g be Polynomial of n, L st f reduces_to (g,G,T) & ( PolyRedRel (G,T)) reduces (g,( 0_ (n,L))) by A2, Lm5;

        hence f is_reducible_wrt (G,T) by POLYRED:def 9;

      end;

      hence thesis;

    end;

    theorem :: GROEB_1:26

    

     Th26: for n be Element of NAT , T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal Subset of ( Polynom-Ring (n,L)), G be Subset of ( Polynom-Ring (n,L)) st G c= I holds (for f be non-zero Polynomial of n, L st f in I holds f is_reducible_wrt (G,T)) implies (for f be non-zero Polynomial of n, L st f in I holds f is_top_reducible_wrt (G,T))

    proof

      let n be Element of NAT , T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal Subset of ( Polynom-Ring (n,L)), P be Subset of ( Polynom-Ring (n,L));

      assume

       A1: P c= I;

      assume

       A2: for f be non-zero Polynomial of n, L st f in I holds f is_reducible_wrt (P,T);

      thus for f be non-zero Polynomial of n, L st f in I holds f is_top_reducible_wrt (P,T)

      proof

        set H = { g where g be non-zero Polynomial of n, L : g in I & not (g is_top_reducible_wrt (P,T)) };

        let f be non-zero Polynomial of n, L;

        assume

         A3: f in I;

        assume not f is_top_reducible_wrt (P,T);

        then

         A4: f in H by A3;

        now

          let u be object;

          assume u in H;

          then ex g9 be non-zero Polynomial of n, L st u = g9 & g9 in I & not g9 is_top_reducible_wrt (P,T);

          hence u in the carrier of ( Polynom-Ring (n,L));

        end;

        then

        reconsider H as non empty Subset of ( Polynom-Ring (n,L)) by A4, TARSKI:def 3;

        consider p be Polynomial of n, L such that

         A5: p in H and

         A6: for q be Polynomial of n, L st q in H holds p <= (q,T) by POLYRED: 31;

        

         A7: ex p9 be non-zero Polynomial of n, L st p9 = p & p9 in I & not p9 is_top_reducible_wrt (P,T) by A5;

        then

        reconsider p as non-zero Polynomial of n, L;

        p is_reducible_wrt (P,T) by A2, A7;

        then

        consider q be Polynomial of n, L such that

         A8: p reduces_to (q,P,T) by POLYRED:def 9;

        consider u be Polynomial of n, L such that

         A9: u in P and

         A10: p reduces_to (q,u,T) by A8, POLYRED:def 7;

        ex b be bag of n st p reduces_to (q,u,b,T) by A10, POLYRED:def 6;

        then

         A11: u <> ( 0_ (n,L)) by POLYRED:def 5;

        then

        reconsider u as non-zero Polynomial of n, L by POLYNOM7:def 1;

        consider b be bag of n such that

         A12: p reduces_to (q,u,b,T) by A10, POLYRED:def 6;

         A13:

        now

          assume b = ( HT (p,T));

          then p top_reduces_to (q,u,T) by A12, POLYRED:def 10;

          then p is_top_reducible_wrt (u,T) by POLYRED:def 11;

          hence contradiction by A7, A9, POLYRED:def 12;

        end;

        consider m be Monomial of n, L such that

         A14: q = (p - (m *' u)) by A10, Th1;

        reconsider uu = u, pp = p, mm = m as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        reconsider uu, pp, mm as Element of ( Polynom-Ring (n,L));

        (mm * uu) in I by A1, A9, IDEAL_1:def 2;

        then ( - (mm * uu)) in I by IDEAL_1: 13;

        then

         A15: (pp + ( - (mm * uu))) in I by A7, IDEAL_1:def 1;

        (mm * uu) = (m *' u) by POLYNOM1:def 11;

        then (p - (m *' u)) = (pp - (mm * uu)) by Lm2;

        then

         A16: q in I by A14, A15;

        

         A17: q < (p,T) by A10, POLYRED: 43;

        

         A18: p <> ( 0_ (n,L)) by POLYNOM7:def 1;

        then ( Support p) <> {} by POLYNOM7: 1;

        then

         A19: ( HT (p,T)) in ( Support p) by TERMORD:def 6;

        b in ( Support p) by A12, POLYRED:def 5;

        then b <= (( HT (p,T)),T) by TERMORD:def 6;

        then b < (( HT (p,T)),T) by A13, TERMORD:def 3;

        then

         A20: ( HT (p,T)) in ( Support q) by A19, A12, POLYRED: 40;

        now

          per cases ;

            case

             A21: q <> ( 0_ (n,L));

            then

            reconsider q as non-zero Polynomial of n, L by POLYNOM7:def 1;

            ( Support q) <> {} by A21, POLYNOM7: 1;

            then ( HT (q,T)) in ( Support q) by TERMORD:def 6;

            then

             A22: ( HT (q,T)) <= (( HT (p,T)),T) by A10, POLYRED: 42;

            ( HT (p,T)) <= (( HT (q,T)),T) by A20, TERMORD:def 6;

            then

             A23: ( HT (q,T)) = ( HT (p,T)) by A22, TERMORD: 7;

            now

              assume not q is_top_reducible_wrt (P,T);

              then q in H by A16;

              then p <= (q,T) by A6;

              hence contradiction by A17, POLYRED: 29;

            end;

            then

            consider u9 be Polynomial of n, L such that

             A24: u9 in P and

             A25: q is_top_reducible_wrt (u9,T) by POLYRED:def 12;

            consider q9 be Polynomial of n, L such that

             A26: q top_reduces_to (q9,u9,T) by A25, POLYRED:def 11;

            

             A27: p <> ( 0_ (n,L)) by POLYNOM7:def 1;

            then ( Support p) <> {} by POLYNOM7: 1;

            then

             A28: ( HT (p,T)) in ( Support p) by TERMORD:def 6;

            

             A29: q reduces_to (q9,u9,( HT (q,T)),T) by A26, POLYRED:def 10;

            then

            consider s be bag of n such that

             A30: (s + ( HT (u9,T))) = ( HT (q,T)) and q9 = (q - (((q . ( HT (q,T))) / ( HC (u9,T))) * (s *' u9))) by POLYRED:def 5;

            set qq = (p - (((p . ( HT (p,T))) / ( HC (u9,T))) * (s *' u9)));

            u9 <> ( 0_ (n,L)) by A29, POLYRED:def 5;

            then p reduces_to (qq,u9,( HT (p,T)),T) by A23, A30, A27, A28, POLYRED:def 5;

            then p top_reduces_to (qq,u9,T) by POLYRED:def 10;

            then p is_top_reducible_wrt (u9,T) by POLYRED:def 11;

            hence contradiction by A7, A24, POLYRED:def 12;

          end;

            case q = ( 0_ (n,L));

            

            then

             A31: (m *' u) = ((p - (m *' u)) + (m *' u)) by A14, POLYRED: 2

            .= ((p + ( - (m *' u))) + (m *' u)) by POLYNOM1:def 7

            .= (p + (( - (m *' u)) + (m *' u))) by POLYNOM1: 21

            .= (p + ( 0_ (n,L))) by POLYRED: 3

            .= p by POLYNOM1: 23;

            m <> ( 0_ (n,L)) by A31, POLYRED: 5, POLYNOM7:def 1;

            then

            reconsider m as non-zero Polynomial of n, L by POLYNOM7:def 1;

            set pp = (p - (((p . ( HT (p,T))) / ( HC (u,T))) * (( HT (m,T)) *' u)));

            ( HT (p,T)) = (( HT (m,T)) + ( HT (u,T))) by A31, TERMORD: 31;

            then p reduces_to (pp,u,( HT (p,T)),T) by A11, A18, A19, POLYRED:def 5;

            then p top_reduces_to (pp,u,T) by POLYRED:def 10;

            then p is_top_reducible_wrt (u,T) by POLYRED:def 11;

            hence contradiction by A7, A9, POLYRED:def 12;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: GROEB_1:27

    

     Th27: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, G,I be Subset of ( Polynom-Ring (n,L)) holds (for f be non-zero Polynomial of n, L st f in I holds f is_top_reducible_wrt (G,T)) implies (for b be bag of n st b in ( HT (I,T)) holds ex b9 be bag of n st b9 in ( HT (G,T)) & b9 divides b)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P,I be Subset of ( Polynom-Ring (n,L));

      assume

       A1: for f be non-zero Polynomial of n, L st f in I holds f is_top_reducible_wrt (P,T);

      now

        let b be bag of n;

        assume b in ( HT (I,T));

        then

        consider p be Polynomial of n, L such that

         A2: b = ( HT (p,T)) and

         A3: p in I and

         A4: p <> ( 0_ (n,L));

        reconsider p as non-zero Polynomial of n, L by A4, POLYNOM7:def 1;

        p is_top_reducible_wrt (P,T) by A1, A3;

        then

        consider u be Polynomial of n, L such that

         A5: u in P and

         A6: p is_top_reducible_wrt (u,T) by POLYRED:def 12;

        consider q be Polynomial of n, L such that

         A7: p top_reduces_to (q,u,T) by A6, POLYRED:def 11;

        

         A8: p reduces_to (q,u,( HT (p,T)),T) by A7, POLYRED:def 10;

        then u <> ( 0_ (n,L)) by POLYRED:def 5;

        then

         A9: ( HT (u,T)) in { ( HT (r,T)) where r be Polynomial of n, L : r in P & r <> ( 0_ (n,L)) } by A5;

        ex s be bag of n st (s + ( HT (u,T))) = ( HT (p,T)) & q = (p - (((p . ( HT (p,T))) / ( HC (u,T))) * (s *' u))) by A8, POLYRED:def 5;

        hence ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b by A2, A9, PRE_POLY: 50;

      end;

      hence thesis;

    end;

    theorem :: GROEB_1:28

    

     Th28: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, G,I be Subset of ( Polynom-Ring (n,L)) holds (for b be bag of n st b in ( HT (I,T)) holds ex b9 be bag of n st b9 in ( HT (G,T)) & b9 divides b) implies ( HT (I,T)) c= ( multiples ( HT (G,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 almost_left_invertible non trivial doubleLoopStr, P,I be Subset of ( Polynom-Ring (n,L));

      assume

       A1: for b be bag of n st b in ( HT (I,T)) holds ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b;

      let u be object;

      assume

       A2: u in ( HT (I,T));

      then

      reconsider u9 = u as Element of ( Bags n);

      ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides u9 by A1, A2;

      hence u in ( multiples ( HT (P,T)));

    end;

    theorem :: GROEB_1:29

    

     Th29: for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)), G be non empty Subset of ( Polynom-Ring (n,L)) st G c= I holds ( HT (I,T)) c= ( multiples ( HT (G,T))) implies G is_Groebner_basis_of (I,T)

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)), P be non empty Subset of ( Polynom-Ring (n,L));

      assume

       A1: P c= I;

      set R = ( PolyRedRel (P,T));

      assume

       A2: ( HT (I,T)) c= ( multiples ( HT (P,T)));

      

       A3: for f be Polynomial of n, L st f in I & f <> ( 0_ (n,L)) holds f is_reducible_wrt (P,T)

      proof

        let f be Polynomial of n, L;

        assume that

         A4: f in I and

         A5: f <> ( 0_ (n,L));

        ( HT (f,T)) in { ( HT (p,T)) where p be Polynomial of n, L : p in I & p <> ( 0_ (n,L)) } by A4, A5;

        then ( HT (f,T)) in ( multiples ( HT (P,T))) by A2;

        then ex b be Element of ( Bags n) st b = ( HT (f,T)) & ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b;

        then

        consider b9 be bag of n such that

         A6: b9 in ( HT (P,T)) and

         A7: b9 divides ( HT (f,T));

        consider p be Polynomial of n, L such that

         A8: b9 = ( HT (p,T)) and

         A9: p in P and

         A10: p <> ( 0_ (n,L)) by A6;

        consider s be bag of n such that

         A11: (b9 + s) = ( HT (f,T)) by A7, TERMORD: 1;

        set g = (f - (((f . ( HT (f,T))) / ( HC (p,T))) * (s *' p)));

        ( Support f) <> {} by A5, POLYNOM7: 1;

        then ( HT (f,T)) in ( Support f) by TERMORD:def 6;

        then f reduces_to (g,p,( HT (f,T)),T) by A5, A8, A10, A11, POLYRED:def 5;

        then f reduces_to (g,p,T) by POLYRED:def 6;

        then f reduces_to (g,P,T) by A9, POLYRED:def 7;

        hence thesis by POLYRED:def 9;

      end;

      

       A12: ( PolyRedRel (P,T)) c= ( PolyRedRel (I,T)) by A1, Th4;

      

       A13: for f be Polynomial of n, L st f in I holds R reduces (f,( 0_ (n,L)))

      proof

        let f be Polynomial of n, L;

        assume

         A14: f in I;

        per cases ;

          suppose f = ( 0_ (n,L));

          hence thesis by REWRITE1: 12;

        end;

          suppose f <> ( 0_ (n,L));

          then f is_reducible_wrt (P,T) by A3, A14;

          then

          consider v be Polynomial of n, L such that

           A15: f reduces_to (v,P,T) by POLYRED:def 9;

           [f, v] in R by A15, POLYRED:def 13;

          then f in ( field R) by RELAT_1: 15;

          then f has_a_normal_form_wrt R by REWRITE1:def 14;

          then

          consider g be object such that

           A16: g is_a_normal_form_of (f,R) by REWRITE1:def 11;

          

           A17: R reduces (f,g) by A16, REWRITE1:def 6;

          then

          reconsider g9 = g as Polynomial of n, L by Lm4;

          reconsider ff = f, gg = g9 as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

          reconsider ff, gg as Element of ( Polynom-Ring (n,L));

          (f - g9) = (ff - gg) by Lm2;

          then (ff - gg) in (I -Ideal ) by A12, A17, POLYRED: 59, REWRITE1: 22;

          then (ff - gg) in I by IDEAL_1: 44;

          then

           A18: ((ff - gg) - ff) in I by A14, IDEAL_1: 16;

          ((ff - gg) - ff) = ((ff + ( - gg)) - ff)

          .= ((ff + ( - gg)) + ( - ff))

          .= ((ff + ( - ff)) + ( - gg)) by RLVECT_1:def 3

          .= (( 0. ( Polynom-Ring (n,L))) + ( - gg)) by RLVECT_1: 5

          .= ( - gg) by ALGSTR_1:def 2;

          then ( - ( - gg)) in I by A18, IDEAL_1: 14;

          then

           A19: g in I by RLVECT_1: 17;

          assume not R reduces (f,( 0_ (n,L)));

          then g <> ( 0_ (n,L)) by A16, REWRITE1:def 6;

          then g9 is_reducible_wrt (P,T) by A3, A19;

          then

          consider u be Polynomial of n, L such that

           A20: g9 reduces_to (u,P,T) by POLYRED:def 9;

          

           A21: [g9, u] in R by A20, POLYRED:def 13;

          g is_a_normal_form_wrt R by A16, REWRITE1:def 6;

          hence contradiction by A21, REWRITE1:def 5;

        end;

      end;

      then

       A22: (P -Ideal ) = I by A1, Lm7;

      now

        let a,b,c be object;

        assume that

         A23: [a, b] in R and

         A24: [a, c] in R;

        consider a9,b9 be object such that a9 in ( NonZero ( Polynom-Ring (n,L))) and

         A25: b9 in the carrier of ( Polynom-Ring (n,L)) and

         A26: [a, b] = [a9, b9] by A23, ZFMISC_1:def 2;

        

         A27: b9 = b by A26, XTUPLE_0: 1;

        (a,b) are_convertible_wrt R by A23, REWRITE1: 29;

        then

         A28: (b,a) are_convertible_wrt R by REWRITE1: 31;

        consider aa,c9 be object such that aa in ( NonZero ( Polynom-Ring (n,L))) and

         A29: c9 in the carrier of ( Polynom-Ring (n,L)) and

         A30: [a, c] = [aa, c9] by A24, ZFMISC_1:def 2;

        

         A31: c9 = c by A30, XTUPLE_0: 1;

        reconsider b9, c9 as Polynomial of n, L by A25, A29, POLYNOM1:def 11;

        reconsider bb = b9, cc = c9 as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        reconsider bb, cc as Element of ( Polynom-Ring (n,L));

        (a,c) are_convertible_wrt R by A24, REWRITE1: 29;

        then (bb,cc) are_congruent_mod I by A22, A27, A31, A28, POLYRED: 57, REWRITE1: 30;

        then

         A32: (bb - cc) in I by POLYRED:def 14;

        (b9 - c9) = (bb - cc) by Lm2;

        hence (b,c) are_convergent_wrt R by A13, A27, A31, A32, POLYRED: 50;

      end;

      then ( PolyRedRel (P,T)) is locally-confluent by REWRITE1:def 24;

      hence thesis by A22;

    end;

    begin

    theorem :: GROEB_1:30

    

     Th30: for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr holds {( 0_ (n,L))} is_Groebner_basis_of ( {( 0_ (n,L))},T)

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr;

      set I = {( 0_ (n,L))}, G = {( 0_ (n,L))}, R = ( PolyRedRel (G,T));

      

       A1: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      now

        let a,b,c be object;

        assume that

         A2: [a, b] in R and [a, c] in R;

        consider p,q be object such that

         A3: p in ( NonZero ( Polynom-Ring (n,L))) and

         A4: q in the carrier of ( Polynom-Ring (n,L)) and

         A5: [a, b] = [p, q] by A2, ZFMISC_1:def 2;

        reconsider q as Polynomial of n, L by A4, POLYNOM1:def 11;

         not p in {( 0_ (n,L))} by A1, A3, XBOOLE_0:def 5;

        then p <> ( 0_ (n,L)) by TARSKI:def 1;

        then

        reconsider p as non-zero Polynomial of n, L by A3, POLYNOM1:def 11, POLYNOM7:def 1;

        p reduces_to (q,G,T) by A2, A5, POLYRED:def 13;

        then

        consider g be Polynomial of n, L such that

         A6: g in G and

         A7: p reduces_to (q,g,T) by POLYRED:def 7;

        g = ( 0_ (n,L)) by A6, TARSKI:def 1;

        then p is_reducible_wrt (( 0_ (n,L)),T) by A7, POLYRED:def 8;

        hence (b,c) are_convergent_wrt R by Lm3;

      end;

      then

       A8: ( PolyRedRel (G,T)) is locally-confluent by REWRITE1:def 24;

      ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      then (G -Ideal ) = I by IDEAL_1: 44;

      hence thesis by A8;

    end;

    theorem :: GROEB_1:31

    for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p be Polynomial of n, L holds {p} is_Groebner_basis_of (( {p} -Ideal ),T)

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p be Polynomial of n, L;

      per cases ;

        suppose

         A1: p = ( 0_ (n,L));

        ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

        then ( {p} -Ideal ) = {( 0_ (n,L))} by A1, IDEAL_1: 44;

        hence thesis by A1, Th30;

      end;

        suppose p <> ( 0_ (n,L));

        then

        reconsider p as non-zero Polynomial of n, L by POLYNOM7:def 1;

        ( PolyRedRel ( {p},T)) is locally-confluent by Th10;

        hence thesis;

      end;

    end;

    theorem :: GROEB_1:32

    for T be admissible connected TermOrder of {} , L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring ( {} ,L)), P be non empty Subset of ( Polynom-Ring ( {} ,L)) st P c= I & P <> {( 0_ ( {} ,L))} holds P is_Groebner_basis_of (I,T)

    proof

      now

        set j = the Element of { i where i be Element of NAT : i < 0 };

        assume { i where i be Element of NAT : i < 0 } <> {} ;

        then j in { i where i be Element of NAT : i < 0 };

        then ex i be Element of NAT st i = j & i < 0 ;

        hence contradiction;

      end;

      then

      reconsider n = {} as Element of NAT ;

      let T be admissible connected TermOrder of {} , L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring ( {} ,L)), P be non empty Subset of ( Polynom-Ring ( {} ,L));

      assume that

       A1: P c= I and

       A2: P <> {( 0_ ( {} ,L))};

      reconsider T as admissible connected TermOrder of n;

      reconsider P as non empty Subset of ( Polynom-Ring (n,L));

      reconsider I as add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L));

      

       A3: ex q be Element of P st q <> ( 0_ (n,L))

      proof

        assume

         A4: not (ex q be Element of P st q <> ( 0_ (n,L)));

         A5:

        now

          let u be object;

          assume u in {( 0_ (n,L))};

          then

           A6: u = ( 0_ (n,L)) by TARSKI:def 1;

          now

            assume not u in P;

            then for v be object holds not v in P by A4, A6;

            hence thesis by XBOOLE_0:def 1;

          end;

          hence u in P;

        end;

        now

          let u be object;

          assume u in P;

          then u = ( 0_ (n,L)) by A4;

          hence u in {( 0_ (n,L))} by TARSKI:def 1;

        end;

        hence thesis by A2, A5, TARSKI: 2;

      end;

      now

        consider p be Element of P such that

         A7: p <> ( 0_ (n,L)) by A3;

        reconsider p as Polynomial of n, L by POLYNOM1:def 11;

        reconsider p as non-zero Polynomial of n, L by A7, POLYNOM7:def 1;

        let f be non-zero Polynomial of n, L;

        assume f in I;

        f <> ( 0_ (n,L)) by POLYNOM7:def 1;

        then ( Support f) <> {} by POLYNOM7: 1;

        then ( HT (f,T)) in ( Support f) by TERMORD:def 6;

        then ( HT (p,T)) = ( EmptyBag n) & ( EmptyBag n) in ( Support f);

        then f is_reducible_wrt (p,T) by POLYRED: 36;

        then

        consider g be Polynomial of n, L such that

         A8: f reduces_to (g,p,T) by POLYRED:def 8;

        f reduces_to (g,P,T) by A8, POLYRED:def 7;

        hence f is_reducible_wrt (P,T) by POLYRED:def 9;

      end;

      then for f be non-zero Polynomial of n, L st f in I holds f is_top_reducible_wrt (P,T) by A1, Th26;

      then for b be bag of n st b in ( HT (I,T)) holds ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b by Th27;

      then ( HT (I,T)) c= ( multiples ( HT (P,T))) by Th28;

      hence thesis by A1, Th29;

    end;

    theorem :: GROEB_1:33

    for n be non empty Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr holds ex P be Subset of ( Polynom-Ring (n,L)) st not (P is_Groebner_basis_wrt T)

    proof

      let n be non empty Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr;

      set 1bag = (( EmptyBag n) +* ( {} ,1));

      reconsider 1bag as Element of ( Bags n) by PRE_POLY:def 12;

      set p = ((( 1. L) | (n,L)) +* (1bag,( 1. L)));

      reconsider p as Function of ( Bags n), L;

      reconsider p as Series of n, L;

      

       A1: ( 1. L) <> ( 0. L);

      set q = ((( 0. L) | (n,L)) +* (1bag,( 1. L)));

      reconsider q as Function of ( Bags n), L;

      reconsider q as Series of n, L;

       A2:

      now

        let u be bag of n;

        assume that

         A3: u <> ( EmptyBag n) and

         A4: u <> 1bag;

        (p . u) = ((( 1. L) | (n,L)) . u) by A4, FUNCT_7: 32;

        then (p . u) = (( 1_ (n,L)) . u) by POLYNOM7: 20;

        hence (p . u) = ( 0. L) by A3, POLYNOM1: 25;

      end;

       A5:

      now

        let u9 be object;

        assume

         A6: u9 in ( Support p);

        then

        reconsider u = u9 as Element of ( Bags n);

        

         A7: (p . u) <> ( 0. L) by A6, POLYNOM1:def 4;

        now

          assume not u in {( EmptyBag n), 1bag};

          then u <> ( EmptyBag n) & u <> 1bag by TARSKI:def 2;

          hence contradiction by A2, A7;

        end;

        hence u9 in {( EmptyBag n), 1bag};

      end;

       {} in n & ( dom ( EmptyBag n)) = n by ORDINAL1: 14, PARTFUN1:def 2;

      then (1bag . {} ) = 1 by FUNCT_7: 31;

      then

       A8: ( EmptyBag n) <> 1bag by PBOOLE: 5;

      

      then

       A9: (q . ( EmptyBag n)) = ((( 0. L) | (n,L)) . ( EmptyBag n)) by FUNCT_7: 32

      .= (( 0_ (n,L)) . ( EmptyBag n)) by POLYNOM7: 19

      .= ( 0. L) by POLYNOM1: 22;

       A10:

      now

        let u be bag of n;

        assume u <> 1bag;

        then (q . u) = ((( 0. L) | (n,L)) . u) by FUNCT_7: 32;

        then (q . u) = (( 0_ (n,L)) . u) by POLYNOM7: 19;

        hence (q . u) = ( 0. L) by POLYNOM1: 22;

      end;

       A11:

      now

        let u9 be object;

        assume

         A12: u9 in ( Support q);

        then

        reconsider u = u9 as Element of ( Bags n);

        

         A13: (q . u) <> ( 0. L) by A12, POLYNOM1:def 4;

        now

          assume not u in {1bag};

          then u <> 1bag by TARSKI:def 1;

          hence contradiction by A10, A13;

        end;

        hence u9 in {1bag};

      end;

      ( dom (( 0. L) | (n,L))) = ( Bags n) by FUNCT_2:def 1;

      then

       A14: (q . 1bag) = ( 1. L) by FUNCT_7: 31;

      then

       A15: q <> ( 0_ (n,L)) by POLYNOM1: 22;

      now

        let u be object;

        assume u in {1bag};

        then u = 1bag by TARSKI:def 1;

        hence u in ( Support q) by A14, POLYNOM1:def 4;

      end;

      then

       A16: ( Support q) = {1bag} by A11, TARSKI: 2;

      then

      reconsider q as Polynomial of n, L by POLYNOM1:def 5;

      reconsider q as non-zero Polynomial of n, L by A15, POLYNOM7:def 1;

      set q1 = (q - (((q . ( HT (q,T))) / ( HC (q,T))) * (( EmptyBag n) *' q)));

      ( Support q) <> {} by A15, POLYNOM7: 1;

      then

       A17: ( HT (q,T)) in ( Support q) by TERMORD:def 6;

      (( EmptyBag n) + ( HT (q,T))) = ( HT (q,T)) by PRE_POLY: 53;

      then q reduces_to (q1,q,( HT (q,T)),T) by A15, A17, POLYRED:def 5;

      then

       A18: q reduces_to (q1,q,T) by POLYRED:def 6;

      

       A19: q1 = (q - ((( HC (q,T)) / ( HC (q,T))) * (( EmptyBag n) *' q))) by TERMORD:def 7

      .= (q - ((( HC (q,T)) * (( HC (q,T)) " )) * (( EmptyBag n) *' q)))

      .= (q - (( 1. L) * (( EmptyBag n) *' q))) by VECTSP_1:def 10

      .= (q - (( 1. L) * q)) by POLYRED: 17

      .= (q - ((( 1. L) | (n,L)) *' q)) by POLYNOM7: 27

      .= (q - (( 1_ (n,L)) *' q)) by POLYNOM7: 20

      .= (q - q) by POLYNOM1: 30

      .= ( 0_ (n,L)) by POLYNOM1: 24;

      

       A20: ( dom (( 1. L) | (n,L))) = ( Bags n) by FUNCT_2:def 1;

      then

       A21: (p . 1bag) = ( 1. L) by FUNCT_7: 31;

      then

       A22: p <> ( 0_ (n,L)) by A1, POLYNOM1: 22;

      

       A23: (p . ( EmptyBag n)) = ((( 1. L) | (n,L)) . ( EmptyBag n)) by A8, FUNCT_7: 32

      .= (( 1_ (n,L)) . ( EmptyBag n)) by POLYNOM7: 20

      .= ( 1. L) by POLYNOM1: 25;

      now

        let u be object;

        assume

         A24: u in {( EmptyBag n), 1bag};

        now

          per cases by A24, TARSKI:def 2;

            case u = ( EmptyBag n);

            hence u in ( Support p) by A1, A23, POLYNOM1:def 4;

          end;

            case u = 1bag;

            hence u in ( Support p) by A1, A21, POLYNOM1:def 4;

          end;

        end;

        hence u in ( Support p);

      end;

      then

       A25: ( Support p) = {( EmptyBag n), 1bag} by A5, TARSKI: 2;

      then

      reconsider p as Polynomial of n, L by POLYNOM1:def 5;

      reconsider p as non-zero Polynomial of n, L by A22, POLYNOM7:def 1;

      

       A26: (( EmptyBag n) + ( HT (p,T))) = ( HT (p,T)) by PRE_POLY: 53;

       A27:

      now

        

         A28: ( EmptyBag n) <= (1bag,T) by TERMORD: 9;

        assume

         A29: ( HT (p,T)) = ( EmptyBag n);

        1bag in ( Support p) by A25, TARSKI:def 2;

        then 1bag <= (( EmptyBag n),T) by A29, TERMORD:def 6;

        hence contradiction by A8, A28, TERMORD: 7;

      end;

      set p1 = (q - (((q . ( HT (p,T))) / ( HC (p,T))) * (( EmptyBag n) *' p)));

      ( Support p) <> {} by A22, POLYNOM7: 1;

      then

       A30: ( HT (p,T)) in ( Support p) by TERMORD:def 6;

      then

       A31: ( HT (p,T)) = 1bag by A25, A27, TARSKI:def 2;

      then ( HT (p,T)) in ( Support q) by A16, TARSKI:def 1;

      then q reduces_to (p1,p,( HT (p,T)),T) by A22, A15, A26, POLYRED:def 5;

      then

       A32: q reduces_to (p1,p,T) by POLYRED:def 6;

       A33:

      now

        assume ( Support q) = ( Support p);

        then ( EmptyBag n) in {1bag} by A25, A16, TARSKI:def 2;

        hence contradiction by A8, TARSKI:def 1;

      end;

       A34:

      now

        assume (q - p) = ( 0_ (n,L));

        

        then p = ((q - p) + p) by POLYRED: 2

        .= ((q + ( - p)) + p) by POLYNOM1:def 7

        .= (q + (( - p) + p)) by POLYNOM1: 21

        .= (q + ( 0_ (n,L))) by POLYRED: 3;

        hence contradiction by A33, POLYNOM1: 23;

      end;

      set P = {p, q};

      now

        let u be object;

        assume u in P;

        then u = p or u = q by TARSKI:def 2;

        hence u in the carrier of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      end;

      then

      reconsider P as Subset of ( Polynom-Ring (n,L)) by TARSKI:def 3;

      reconsider P as Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T));

      take P;

      

       A35: p in P by TARSKI:def 2;

      q in P by TARSKI:def 2;

      then q reduces_to (( 0_ (n,L)),P,T) by A18, A19, POLYRED:def 7;

      then

       A36: [q, ( 0_ (n,L))] in R by POLYRED:def 13;

      p1 = (q - ((( 1. L) / (p . 1bag)) * (( EmptyBag n) *' p))) by A14, A31, TERMORD:def 7

      .= (q - ((( 1. L) / ( 1. L)) * (( EmptyBag n) *' p))) by A20, FUNCT_7: 31

      .= (q - ((( 1. L) * (( 1. L) " )) * (( EmptyBag n) *' p)))

      .= (q - (( 1. L) * (( EmptyBag n) *' p))) by VECTSP_1:def 10

      .= (q - (( 1. L) * p)) by POLYRED: 17

      .= (q - ((( 1. L) | (n,L)) *' p)) by POLYNOM7: 27

      .= (q - (( 1_ (n,L)) *' p)) by POLYNOM7: 20

      .= (q - p) by POLYNOM1: 30;

      then q reduces_to ((q - p),P,T) by A32, A35, POLYRED:def 7;

      then

       A37: [q, (q - p)] in R by POLYRED:def 13;

      now

         A38:

        now

          let u be object;

          now

            let u be object;

            assume u in {1bag};

            then u = 1bag by TARSKI:def 1;

            hence u in {( EmptyBag n), 1bag} by TARSKI:def 2;

          end;

          then {1bag} c= {( EmptyBag n), 1bag};

          then

           A39: ( {1bag} \/ {( EmptyBag n), 1bag}) = {( EmptyBag n), 1bag} by XBOOLE_1: 12;

          

           A40: ((q - p) . 1bag) = ((q + ( - p)) . 1bag) by POLYNOM1:def 7

          .= ((q . 1bag) + (( - p) . 1bag)) by POLYNOM1: 15

          .= ((q . 1bag) + ( - (p . 1bag))) by POLYNOM1: 17

          .= (( 1. L) + ( - ( 1. L))) by A20, A14, FUNCT_7: 31

          .= ( 0. L) by RLVECT_1: 5;

          ( Support (q - p)) = ( Support (q + ( - p))) by POLYNOM1:def 7;

          then ( Support (q - p)) c= (( Support q) \/ ( Support ( - p))) by POLYNOM1: 20;

          then

           A41: ( Support (q - p)) c= ( {1bag} \/ {( EmptyBag n), 1bag}) by A25, A16, Th5;

          assume

           A42: u in ( Support (q - p));

          then ((q - p) . u) <> ( 0. L) by POLYNOM1:def 4;

          then u = ( EmptyBag n) by A42, A41, A39, A40, TARSKI:def 2;

          hence u in {( EmptyBag n)} by TARSKI:def 1;

        end;

        assume R is locally-confluent;

        then (( 0_ (n,L)),(q - p)) are_convergent_wrt R by A37, A36, REWRITE1:def 24;

        then

        consider c be object such that

         A43: R reduces (( 0_ (n,L)),c) and

         A44: R reduces ((q - p),c) by REWRITE1:def 7;

        reconsider c as Polynomial of n, L by A43, Lm4;

        consider s be FinSequence such that

         A45: ( len s) > 0 and

         A46: (s . 1) = ( 0_ (n,L)) and

         A47: (s . ( len s)) = c and

         A48: for i be Nat st i in ( dom s) & (i + 1) in ( dom s) holds [(s . i), (s . (i + 1))] in R by A43, REWRITE1: 11;

        now

          

           A49: ( 0 + 1) <= ( len s) by A45, NAT_1: 13;

          

           A50: ( dom s) = ( Seg ( len s)) by FINSEQ_1:def 3;

          assume ( len s) <> 1;

          then 1 < ( len s) by A49, XXREAL_0: 1;

          then (1 + 1) <= ( len s) by NAT_1: 13;

          then

           A51: (1 + 1) in ( dom s) by A50, FINSEQ_1: 1;

          

           A52: 1 in ( dom s) by A49, A50, FINSEQ_1: 1;

          then

          consider f9,h9 be object such that

           A53: [( 0_ (n,L)), (s . 2)] = [f9, h9] and f9 in ( NonZero ( Polynom-Ring (n,L))) and

           A54: h9 in the carrier of ( Polynom-Ring (n,L)) by A46, A48, A51, RELSET_1: 2;

          (s . 2) = h9 by A53, XTUPLE_0: 1;

          then

          reconsider c9 = (s . 2) as Polynomial of n, L by A54, POLYNOM1:def 11;

           [(s . 1), (s . 2)] in R by A48, A52, A51;

          then ( 0_ (n,L)) reduces_to (c9,P,T) by A46, POLYRED:def 13;

          then

          consider g be Polynomial of n, L such that g in P and

           A55: ( 0_ (n,L)) reduces_to (c9,g,T) by POLYRED:def 7;

          ( 0_ (n,L)) is_reducible_wrt (g,T) by A55, POLYRED:def 8;

          hence contradiction by POLYRED: 37;

        end;

        then

        consider s be FinSequence such that

         A56: ( len s) > 0 and

         A57: (s . 1) = (q - p) and

         A58: (s . ( len s)) = ( 0_ (n,L)) and

         A59: for i be Nat st i in ( dom s) & (i + 1) in ( dom s) holds [(s . i), (s . (i + 1))] in R by A44, A46, A47, REWRITE1: 11;

         A60:

        now

          assume ( - ( 1. L)) = ( 0. L);

          then ( - ( - ( 1. L))) = ( 0. L) by RLVECT_1: 12;

          hence contradiction by RLVECT_1: 17;

        end;

        now

          let u be object;

          assume

           A61: u in {( EmptyBag n)};

          then

          reconsider u9 = u as Element of ( Bags n) by TARSKI:def 1;

          ((q - p) . u9) = ((q + ( - p)) . u9) by POLYNOM1:def 7

          .= ((q . u9) + (( - p) . u9)) by POLYNOM1: 15

          .= ((q . u9) + ( - (p . u9))) by POLYNOM1: 17

          .= (( 0. L) + ( - (p . u9))) by A9, A61, TARSKI:def 1

          .= (( 0. L) + ( - ( 1. L))) by A23, A61, TARSKI:def 1

          .= ( - ( 1. L)) by ALGSTR_1:def 2;

          hence u in ( Support (q - p)) by A60, POLYNOM1:def 4;

        end;

        then

         A62: ( Support (q - p)) = {( EmptyBag n)} by A38, TARSKI: 2;

         A63:

        now

          assume (q - p) is_reducible_wrt (P,T);

          then

          consider g be Polynomial of n, L such that

           A64: (q - p) reduces_to (g,P,T) by POLYRED:def 9;

          consider h be Polynomial of n, L such that

           A65: h in P and

           A66: (q - p) reduces_to (g,h,T) by A64, POLYRED:def 7;

          ex b be bag of n st (q - p) reduces_to (g,h,b,T) by A66, POLYRED:def 6;

          then h <> ( 0_ (n,L)) by POLYRED:def 5;

          then

          reconsider h as non-zero Polynomial of n, L by POLYNOM7:def 1;

          (q - p) is_reducible_wrt (h,T) by A66, POLYRED:def 8;

          then

          consider b9 be bag of n such that

           A67: b9 in ( Support (q - p)) and

           A68: ( HT (h,T)) divides b9 by POLYRED: 36;

          

           A69: ( HT (h,T)) = 1bag

          proof

            now

              per cases by A65, TARSKI:def 2;

                case h = p;

                hence thesis by A25, A30, A27, TARSKI:def 2;

              end;

                case h = q;

                hence thesis by A16, A17, TARSKI:def 1;

              end;

            end;

            hence thesis;

          end;

          b9 = ( EmptyBag n) by A62, A67, TARSKI:def 1;

          hence contradiction by A8, A68, A69, PRE_POLY: 58;

        end;

        now

          

           A70: ( 0 + 1) <= ( len s) by A56, NAT_1: 13;

          

           A71: ( dom s) = ( Seg ( len s)) by FINSEQ_1:def 3;

          assume ( len s) <> 1;

          then 1 < ( len s) by A70, XXREAL_0: 1;

          then (1 + 1) <= ( len s) by NAT_1: 13;

          then

           A72: (1 + 1) in ( dom s) by A71, FINSEQ_1: 1;

          

           A73: 1 in ( dom s) by A70, A71, FINSEQ_1: 1;

          then

          consider f9,h9 be object such that

           A74: [(q - p), (s . 2)] = [f9, h9] and f9 in ( NonZero ( Polynom-Ring (n,L))) and

           A75: h9 in the carrier of ( Polynom-Ring (n,L)) by A57, A59, A72, RELSET_1: 2;

          (s . 2) = h9 by A74, XTUPLE_0: 1;

          then

          reconsider c9 = (s . 2) as Polynomial of n, L by A75, POLYNOM1:def 11;

           [(q - p), (s . 2)] in R by A57, A59, A73, A72;

          then (q - p) reduces_to (c9,P,T) by POLYRED:def 13;

          hence contradiction by A63, POLYRED:def 9;

        end;

        hence contradiction by A34, A57, A58;

      end;

      hence thesis;

    end;

    

     Lm8: for n be Ordinal, b1,b2,b3 be bag of n holds b1 divides b2 & b2 divides b3 implies b1 divides b3

    proof

      let n be Ordinal, b1,b2,b3 be bag of n;

      assume

       A1: b1 divides b2 & b2 divides b3;

      now

        let k be object;

        (b1 . k) <= (b2 . k) & (b2 . k) <= (b3 . k) by A1, PRE_POLY:def 11;

        hence (b1 . k) <= (b3 . k) by XXREAL_0: 2;

      end;

      hence thesis by PRE_POLY:def 11;

    end;

    definition

      let n be Ordinal;

      :: GROEB_1:def5

      func DivOrder (n) -> Order of ( Bags n) means

      : Def5: for b1,b2 be bag of n holds [b1, b2] in it iff b1 divides b2;

      existence

      proof

        defpred P[ object, object] means ex b1,b2 be Element of ( Bags n) st $1 = b1 & $2 = b2 & b1 divides b2;

        consider BO be Relation of ( Bags n), ( Bags n) such that

         A1: for x,y be object holds [x, y] in BO iff x in ( Bags n) & y in ( Bags n) & P[x, y] from RELSET_1:sch 1;

        

         A2: BO is_transitive_in ( Bags n)

        proof

          let x,y,z be object such that x in ( Bags n) and y in ( Bags n) and z in ( Bags n) and

           A3: [x, y] in BO and

           A4: [y, z] in BO;

          consider b1,b2 be Element of ( Bags n) such that

           A5: x = b1 and

           A6: y = b2 & b1 divides b2 by A1, A3;

          consider b11,b22 be Element of ( Bags n) such that

           A7: y = b11 and

           A8: z = b22 and

           A9: b11 divides b22 by A1, A4;

          reconsider B1 = b1, B29 = b22 as bag of n;

          B1 divides B29 by A6, A7, A9, Lm8;

          hence thesis by A1, A5, A8;

        end;

        

         A10: BO is_reflexive_in ( Bags n) by A1;

        then

         A11: ( dom BO) = ( Bags n) & ( field BO) = ( Bags n) by ORDERS_1: 13;

        BO is_antisymmetric_in ( Bags n)

        proof

          let x,y be object;

          assume that x in ( Bags n) and y in ( Bags n) and

           A12: [x, y] in BO and

           A13: [y, x] in BO;

          consider b19,b29 be Element of ( Bags n) such that

           A14: y = b19 & x = b29 and

           A15: b19 divides b29 by A1, A13;

          consider b11,b22 be Element of ( Bags n) such that

           A16: x = b11 & y = b22 and

           A17: b11 divides b22 by A1, A12;

          reconsider b11, b22 as bag of n;

           A18:

          now

            let k be object;

            assume k in ( dom b11);

            (b11 . k) <= (b22 . k) & (b19 . k) <= (b29 . k) by A17, A15, PRE_POLY:def 11;

            hence (b11 . k) = (b22 . k) by A16, A14, XXREAL_0: 1;

          end;

          ( dom b11) = n by PARTFUN1:def 2

          .= ( dom b22) by PARTFUN1:def 2;

          hence thesis by A16, A18, FUNCT_1: 2;

        end;

        then

        reconsider BO as Order of ( Bags n) by A10, A2, A11, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

        take BO;

        let p,q be bag of n;

        hereby

          assume [p, q] in BO;

          then ex b19,b29 be Element of ( Bags n) st p = b19 & q = b29 & b19 divides b29 by A1;

          hence p divides q;

        end;

        p in ( Bags n) & q in ( Bags n) by PRE_POLY:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let B1,B2 be Order of ( Bags n) such that

         A19: for p,q be bag of n holds [p, q] in B1 iff p divides q and

         A20: for p,q be bag of n holds [p, q] in B2 iff p divides q;

        let a,b be object;

        hereby

          assume

           A21: [a, b] in B1;

          then

          consider b1,b2 be object such that

           A22: [a, b] = [b1, b2] and

           A23: b1 in ( Bags n) & b2 in ( Bags n) by RELSET_1: 2;

          reconsider b1, b2 as bag of n by A23;

          b1 divides b2 by A19, A21, A22;

          hence [a, b] in B2 by A20, A22;

        end;

        assume

         A24: [a, b] in B2;

        then

        consider b1,b2 be object such that

         A25: [a, b] = [b1, b2] and

         A26: b1 in ( Bags n) & b2 in ( Bags n) by RELSET_1: 2;

        reconsider b1, b2 as bag of n by A26;

        b1 divides b2 by A20, A24, A25;

        hence thesis by A19, A25;

      end;

    end

    registration

      let n be Element of NAT ;

      cluster RelStr (# ( Bags n), ( DivOrder n) #) -> Dickson;

      coherence

      proof

        set R = RelStr (# ( Bags n), ( DivOrder n) #);

        set S = ( product ( Carrier (n --> OrderedNAT ))), SJ = ( Carrier (n --> OrderedNAT ));

        set P = ( product (n --> OrderedNAT )), J = (n --> OrderedNAT );

        defpred Q[ object, object] means $1 in S & (ex b be bag of n st b = $2 & b = $1);

        

         A1: for x be set st x in S holds for g be Function st x = g holds ( dom g) = n & for y be set st y in ( dom g) holds (g . y) in NAT

        proof

          let x be set;

          assume x in S;

          then

          consider g be Function such that

           A2: x = g and

           A3: ( dom g) = ( dom SJ) and

           A4: for y be object st y in ( dom SJ) holds (g . y) in (SJ . y) by CARD_3:def 5;

          let g9 be Function;

          assume

           A5: x = g9;

          hence ( dom g9) = n by A2, A3, PARTFUN1:def 2;

          thus for y be set st y in ( dom g9) holds (g9 . y) in NAT

          proof

            let y be set;

            assume

             A6: y in ( dom g9);

            then

             A7: y in n by A5, A2, A3;

            then

            consider R be 1-sorted such that

             A8: R = (J . y) and

             A9: (SJ . y) = the carrier of R by PRALG_1:def 15;

            (g . y) in the carrier of R by A5, A2, A3, A4, A6, A9;

            hence thesis by A5, A2, A7, A8, DICKSON:def 15, FUNCOP_1: 7;

          end;

        end;

        

         A10: for x be object st x in S holds ex y be object st Q[x, y]

        proof

          let x be object;

          assume

           A11: x in S;

          then

          consider g be Function such that

           A12: x = g and ( dom g) = ( dom SJ) and for y be object st y in ( dom SJ) holds (g . y) in (SJ . y) by CARD_3:def 5;

          defpred QQ[ object, object] means $2 = (g . $1);

          

           A13: for x be object st x in n holds ex y be object st QQ[x, y];

          consider b be Function such that

           A14: ( dom b) = n & for x be object st x in n holds QQ[x, (b . x)] from CLASSES1:sch 1( A13);

          reconsider b as ManySortedSet of n by A14, PARTFUN1:def 2, RELAT_1:def 18;

          

           A15: ( dom g) = n by A1, A11, A12;

          now

            let u be object;

            assume u in ( rng b);

            then

            consider x be object such that

             A16: x in ( dom b) & u = (b . x) by FUNCT_1:def 3;

            u = (g . x) & x in ( dom g) by A15, A14, A16;

            hence u in NAT by A1, A11, A12;

          end;

          then ( rng b) c= NAT ;

          then

          reconsider b as bag of n by VALUED_0:def 6;

          take b;

          thus x in S by A11;

          take b;

          thus b = b;

          b = g by A15, A14, FUNCT_1: 2;

          hence thesis by A12;

        end;

        consider i be Function such that

         A17: ( dom i) = S & for x be object st x in S holds Q[x, (i . x)] from CLASSES1:sch 1( A10);

        

         A18: for x be Element of R holds ex u be Element of P st u in ( dom i) & (i . u) = x

        proof

          let x be Element of R;

          reconsider g = x as bag of n;

           A19:

          now

            let x be object;

            assume x in ( dom ( Carrier J));

            then

             A20: x in n;

            then

            consider L be 1-sorted such that

             A21: L = (J . x) and

             A22: (( Carrier J) . x) = the carrier of L by PRALG_1:def 15;

            the carrier of L = NAT by A20, A21, DICKSON:def 15, FUNCOP_1: 7;

            hence (g . x) in (( Carrier J) . x) by A22, ORDINAL1:def 12;

          end;

          

           A23: ( dom g) = n by PARTFUN1:def 2

          .= ( dom ( Carrier J)) by PARTFUN1:def 2;

          then

           A24: g in ( product ( Carrier J)) by A19, CARD_3:def 5;

          then

          reconsider g as Element of P by YELLOW_1:def 4;

          take g;

          thus g in ( dom i) by A17, A23, A19, CARD_3:def 5;

           Q[g, (i . g)] by A17, A24;

          hence thesis;

        end;

         A25:

        now

          let v be set;

          assume v in ( rng i);

          then

          consider u be object such that

           A26: u in ( dom i) and

           A27: v = (i . u) by FUNCT_1:def 3;

          ex b be bag of n st b = (i . u) & b = u by A17, A26;

          hence v in ( Bags n) by A27, PRE_POLY:def 12;

        end;

        now

          let N be Subset of R;

          set N9 = (i " N);

          

           A28: N9 c= S by A17, RELAT_1: 132;

          then

          reconsider N9 as Subset of P by YELLOW_1:def 4;

          consider B9 be set such that

           A29: B9 is_Dickson-basis_of (N9,P) and

           A30: B9 is finite by DICKSON:def 10;

          set B = (i .: B9);

          

           A31: B9 c= N9 by A29, DICKSON:def 9;

          

           A32: for a,b be Element of P, ta,tb be Element of ( Bags n) st a = ta & b = tb & a in S holds a <= b implies ta divides tb

          proof

            let a,b be Element of P, ta,tb be Element of ( Bags n);

            assume that

             A33: a = ta & b = tb and

             A34: a in S;

            assume a <= b;

            then

            consider f,g be Function such that

             A35: f = a & g = b and

             A36: for i be object st i in n holds ex R be RelStr, ai,bi be Element of R st R = (J . i) & ai = (f . i) & bi = (g . i) & ai <= bi by A34, YELLOW_1:def 4;

            now

              let k be object;

              assume

               A37: k in n;

              then

              consider R be RelStr, ak,bk be Element of R such that

               A38: R = (J . k) and

               A39: ak = (f . k) & bk = (g . k) and

               A40: ak <= bk by A36;

              (J . k) = OrderedNAT by A37, FUNCOP_1: 7;

              then [ak, bk] in NATOrd by A38, A40, DICKSON:def 15, ORDERS_2:def 5;

              then

              consider a9,b9 be Element of NAT such that

               A41: [a9, b9] = [ak, bk] and

               A42: a9 <= b9 by DICKSON:def 14;

              

               A43: b9 = bk by A41, XTUPLE_0: 1;

              a9 = ak by A41, XTUPLE_0: 1;

              hence (ta . k) <= (tb . k) by A33, A35, A39, A42, A43;

            end;

            hence thesis by PRE_POLY: 46;

          end;

          

           A44: for a be Element of R st a in N holds ex b be Element of R st b in B & b <= a

          proof

            let a be Element of R;

            consider a9 be Element of P such that

             A45: a9 in ( dom i) and

             A46: (i . a9) = a by A18;

            

             A47: ex b be bag of n st b = (i . a9) & b = a9 by A17, A45;

            assume a in N;

            then a9 in N9 by A45, A46, FUNCT_1:def 7;

            then

            consider b9 be Element of P such that

             A48: b9 in B9 and

             A49: b9 <= a9 by A29, DICKSON:def 9;

            set b = (i . b9);

            

             A50: B9 c= S by A28, A31;

            then b in ( rng i) by A17, A48, FUNCT_1:def 3;

            then

            reconsider b as Element of ( Bags n) by A25;

            reconsider b as Element of R;

            take b;

            thus b in B by A17, A48, A50, FUNCT_1:def 6;

            reconsider aa = a, bb = b as Element of ( Bags n);

            ex b1 be bag of n st b1 = (i . b9) & b1 = b9 by A17, A48, A50;

            then bb divides aa by A32, A46, A47, A48, A49, A50;

            then [b, a] in ( DivOrder n) by Def5;

            hence thesis by ORDERS_2:def 5;

          end;

          now

            let u be object;

            assume u in B;

            then ex v be object st v in ( dom i) & v in B9 & u = (i . v) by FUNCT_1:def 6;

            hence u in N by A31, FUNCT_1:def 7;

          end;

          then B c= N;

          then B is_Dickson-basis_of (N,R) by A44, DICKSON:def 9;

          hence ex B be set st B is_Dickson-basis_of (N,R) & B is finite by A30;

        end;

        hence thesis by DICKSON:def 10;

      end;

    end

    theorem :: GROEB_1:34

    

     Th34: for n be Element of NAT , N be Subset of RelStr (# ( Bags n), ( DivOrder n) #) holds ex B be finite Subset of ( Bags n) st B is_Dickson-basis_of (N, RelStr (# ( Bags n), ( DivOrder n) #))

    proof

      let n be Element of NAT , N be Subset of RelStr (# ( Bags n), ( DivOrder n) #);

      consider B be set such that

       A1: B is_Dickson-basis_of (N, RelStr (# ( Bags n), ( DivOrder n) #)) and

       A2: B is finite by DICKSON:def 10;

      now

        let u be object;

        assume

         A3: u in B;

        B c= N by A1, DICKSON:def 9;

        hence u in N by A3;

      end;

      then

      reconsider B as finite Subset of N by A2, TARSKI:def 3;

      reconsider B as finite Subset of ( Bags n) by XBOOLE_1: 1;

      take B;

      thus thesis by A1;

    end;

    theorem :: GROEB_1:35

    

     Th35: for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)) holds ex G be finite Subset of ( Polynom-Ring (n,L)) st G is_Groebner_basis_of (I,T)

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L));

      

       A1: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      per cases ;

        suppose

         A2: I = {( 0_ (n,L))};

        set G = {( 0_ (n,L))}, R = ( PolyRedRel (G,T));

        take G;

        now

          let a,b,c be object;

          assume that

           A3: [a, b] in R and [a, c] in R;

          consider p,q be object such that

           A4: p in ( NonZero ( Polynom-Ring (n,L))) and

           A5: q in the carrier of ( Polynom-Ring (n,L)) and

           A6: [a, b] = [p, q] by A3, ZFMISC_1:def 2;

          reconsider q as Polynomial of n, L by A5, POLYNOM1:def 11;

           not p in {( 0_ (n,L))} by A1, A4, XBOOLE_0:def 5;

          then p <> ( 0_ (n,L)) by TARSKI:def 1;

          then

          reconsider p as non-zero Polynomial of n, L by A4, POLYNOM1:def 11, POLYNOM7:def 1;

          p reduces_to (q,G,T) by A3, A6, POLYRED:def 13;

          then

          consider g be Polynomial of n, L such that

           A7: g in G and

           A8: p reduces_to (q,g,T) by POLYRED:def 7;

          g = ( 0_ (n,L)) by A7, TARSKI:def 1;

          then p is_reducible_wrt (( 0_ (n,L)),T) by A8, POLYRED:def 8;

          hence (b,c) are_convergent_wrt R by Lm3;

        end;

        then

         A9: ( PolyRedRel (G,T)) is locally-confluent by REWRITE1:def 24;

        (G -Ideal ) = I by A2, IDEAL_1: 44;

        hence thesis by A9;

      end;

        suppose

         A10: I <> {( 0_ (n,L))};

        ex q be Element of I st q <> ( 0_ (n,L))

        proof

          assume

           A11: not (ex q be Element of I st q <> ( 0_ (n,L)));

           A12:

          now

            let u be object;

            assume u in {( 0_ (n,L))};

            then

             A13: u = ( 0_ (n,L)) by TARSKI:def 1;

            now

              assume not u in I;

              then for v be object holds not v in I by A11, A13;

              hence thesis by XBOOLE_0:def 1;

            end;

            hence u in I;

          end;

          now

            let u be object;

            assume u in I;

            then u = ( 0_ (n,L)) by A11;

            hence u in {( 0_ (n,L))} by TARSKI:def 1;

          end;

          hence thesis by A10, A12, TARSKI: 2;

        end;

        then

        consider q be Element of I such that

         A14: q <> ( 0_ (n,L));

        set R = RelStr (# ( Bags n), ( DivOrder n) #), hti = ( HT (I,T));

        reconsider hti as Subset of R;

        consider S be finite Subset of ( Bags n) such that

         A15: S is_Dickson-basis_of (hti,R) by Th34;

        set M = { { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = s & p <> ( 0_ (n,L)) } where s be Element of ( Bags n) : s in S };

        set s = the Element of S;

        reconsider q as Polynomial of n, L by POLYNOM1:def 11;

        set hq = ( HT (q,T));

        reconsider hq as Element of R;

        hq in { ( HT (p,T)) where p be Polynomial of n, L : p in I & p <> ( 0_ (n,L)) } by A14;

        then ex b be Element of R st b in S & b <= hq by A15, DICKSON:def 9;

        then s in S;

        then { r where r be Polynomial of n, L : r in I & ( HT (r,T)) = s & r <> ( 0_ (n,L)) } in { { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = s9 & p <> ( 0_ (n,L)) } where s9 be Element of ( Bags n) : s9 in S };

        then

        reconsider M as non empty set;

        

         A16: for x,y be set st x in M & y in M & x <> y holds x misses y

        proof

          let x,y be set;

          assume that

           A17: x in M and

           A18: y in M and

           A19: x <> y;

          consider t be Element of ( Bags n) such that

           A20: y = { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = t & p <> ( 0_ (n,L)) } and t in S by A18;

          consider s be Element of ( Bags n) such that

           A21: x = { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = s & p <> ( 0_ (n,L)) } and s in S by A17;

          reconsider x, y as set;

          now

            set u = the Element of (x /\ y);

            assume

             A22: (x /\ y) <> {} ;

            then u in y by XBOOLE_0:def 4;

            then

             A23: ex v be Polynomial of n, L st u = v & v in I & ( HT (v,T)) = t & v <> ( 0_ (n,L)) by A20;

            u in x by A22, XBOOLE_0:def 4;

            then ex r be Polynomial of n, L st u = r & r in I & ( HT (r,T)) = s & r <> ( 0_ (n,L)) by A21;

            hence contradiction by A19, A21, A20, A23;

          end;

          hence thesis by XBOOLE_0:def 7;

        end;

        

         A24: S c= hti by A15, DICKSON:def 9;

        for x be set st x in M holds x <> {}

        proof

          let x be set;

          assume x in M;

          then

          consider s be Element of ( Bags n) such that

           A25: x = { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = s & p <> ( 0_ (n,L)) } and

           A26: s in S;

          s in hti by A24, A26;

          then

          consider q be Polynomial of n, L such that

           A27: s = ( HT (q,T)) & q in I & q <> ( 0_ (n,L));

          q in x by A25, A27;

          hence thesis;

        end;

        then

        consider G9 be set such that

         A28: for x be set st x in M holds ex y be object st (G9 /\ x) = {y} by A16, WELLORD2: 18;

        set xx = the Element of M;

        

         A29: M is finite

        proof

          defpred P[ object, object] means $2 = { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = $1 & p <> ( 0_ (n,L)) };

          

           A30: for x be object st x in S holds ex y be object st P[x, y];

          consider f be Function such that

           A31: ( dom f) = S & for x be object st x in S holds P[x, (f . x)] from CLASSES1:sch 1( A30);

           A32:

          now

            let u be object;

            assume u in ( rng f);

            then

            consider s be object such that

             A33: s in ( dom f) and

             A34: u = (f . s) by FUNCT_1:def 3;

            u = { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = s & p <> ( 0_ (n,L)) } by A31, A33, A34;

            hence u in M by A31, A33;

          end;

          now

            let u be object;

            assume u in M;

            then

            consider s be Element of ( Bags n) such that

             A35: u = { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = s & p <> ( 0_ (n,L)) } and

             A36: s in S;

            (f . s) in ( rng f) by A31, A36, FUNCT_1: 3;

            hence u in ( rng f) by A31, A35, A36;

          end;

          then ( rng f) = M by A32, TARSKI: 2;

          hence thesis by A31, FINSET_1: 8;

        end;

        

         A37: ex y be object st (G9 /\ xx) = {y} by A28;

        set xx = the Element of M;

        reconsider G9 as non empty set by A37;

        set G = { x where x be Element of G9 : ex y be set st y in M & (G9 /\ y) = {x} };

        now

          let u be object;

          assume u in G;

          then

          consider x be Element of G9 such that

           A38: u = x and

           A39: ex y be set st y in M & (G9 /\ y) = {x};

          consider y be set such that

           A40: y in M and

           A41: (G9 /\ y) = {x} by A39;

          consider s be Element of ( Bags n) such that

           A42: y = { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = s & p <> ( 0_ (n,L)) } and s in S by A40;

          x in (G9 /\ y) by A41, TARSKI:def 1;

          then x in y by XBOOLE_0:def 4;

          then ex q be Polynomial of n, L st x = q & q in I & ( HT (q,T)) = s & q <> ( 0_ (n,L)) by A42;

          hence u in the carrier of ( Polynom-Ring (n,L)) by A38;

        end;

        then

        reconsider G as Subset of ( Polynom-Ring (n,L)) by TARSKI:def 3;

        defpred P[ object, object] means ex D1 be set st D1 = $1 & (G9 /\ D1) = {$2} & $2 in G;

        

         A43: for x be object st x in M holds ex y be object st P[x, y]

        proof

          let x be object;

          assume

           A44: x in M;

          reconsider xx = x as set by TARSKI: 1;

          consider y be object such that

           A45: (G9 /\ xx) = {y} by A28, A44;

          y in (G9 /\ xx) by A45, TARSKI:def 1;

          then

          reconsider y as Element of G9 by XBOOLE_0:def 4;

          y in G by A44, A45;

          hence thesis by A45;

        end;

        consider f be Function such that

         A46: ( dom f) = M & for x be object st x in M holds P[x, (f . x)] from CLASSES1:sch 1( A43);

         A47:

        now

          let u be object;

          assume u in G;

          then

          consider x be Element of G9 such that

           A48: u = x and

           A49: ex y be set st y in M & (G9 /\ y) = {x};

          consider y be set such that

           A50: y in M and

           A51: (G9 /\ y) = {x} by A49;

           P[y, (f . y)] by A46, A50;

          then (G9 /\ y) = {(f . y)};

          then

           A52: x in {(f . y)} by A51, TARSKI:def 1;

          (f . y) in ( rng f) by A46, A50, FUNCT_1: 3;

          hence u in ( rng f) by A48, A52, TARSKI:def 1;

        end;

        now

          let u be object;

          assume u in ( rng f);

          then

          consider s be object such that

           A53: s in ( dom f) & u = (f . s) by FUNCT_1:def 3;

           P[s, (f . s)] by A46, A53;

          hence u in G by A53;

        end;

        then

         A54: ( rng f) = G by A47, TARSKI: 2;

        consider y be object such that

         A55: (G9 /\ xx) = {y} by A28;

        y in (G9 /\ xx) by A55, TARSKI:def 1;

        then y in G9 by XBOOLE_0:def 4;

        then y in G by A55;

        then G is non empty finite by A29, A46, A54, FINSET_1: 8;

        then

        reconsider G as non empty finite Subset of ( Polynom-Ring (n,L));

        for b be bag of n st b in ( HT (I,T)) holds ex b9 be bag of n st b9 in ( HT (G,T)) & b9 divides b

        proof

          let b be bag of n;

          reconsider bb = b as Element of R by PRE_POLY:def 12;

          assume b in ( HT (I,T));

          then

          consider bb9 be Element of R such that

           A56: bb9 in S and

           A57: bb9 <= bb by A15, DICKSON:def 9;

          set N = { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = bb9 & p <> ( 0_ (n,L)) };

          

           A58: N in M by A56;

          then

          consider y be object such that

           A59: (G9 /\ N) = {y} by A28;

          reconsider b9 = bb9 as bag of n;

          take b9;

          

           A60: [bb9, bb] in ( DivOrder n) by A57, ORDERS_2:def 5;

          

           A61: y in (G9 /\ N) by A59, TARSKI:def 1;

          then

          reconsider y as Element of G9 by XBOOLE_0:def 4;

          y in N by A61, XBOOLE_0:def 4;

          then

           A62: ex r be Polynomial of n, L st y = r & r in I & ( HT (r,T)) = bb9 & r <> ( 0_ (n,L));

          y in G by A58, A59;

          hence thesis by A60, A62, Def5;

        end;

        then

         A63: ( HT (I,T)) c= ( multiples ( HT (G,T))) by Th28;

        take G;

        now

          let u be object;

          assume u in G;

          then

          consider x be Element of G9 such that

           A64: u = x and

           A65: ex y be set st y in M & (G9 /\ y) = {x};

          consider y be set such that

           A66: y in M and

           A67: (G9 /\ y) = {x} by A65;

          consider s be Element of ( Bags n) such that

           A68: y = { p where p be Polynomial of n, L : p in I & ( HT (p,T)) = s & p <> ( 0_ (n,L)) } and s in S by A66;

          x in (G9 /\ y) by A67, TARSKI:def 1;

          then x in y by XBOOLE_0:def 4;

          then ex q be Polynomial of n, L st x = q & q in I & ( HT (q,T)) = s & q <> ( 0_ (n,L)) by A68;

          hence u in I by A64;

        end;

        then G c= I;

        hence thesis by A63, Th29;

      end;

    end;

    

     Lm9: for L be add-associative left_zeroed right_zeroed right_complementable associative distributive well-unital non empty doubleLoopStr, A,B be non empty Subset of L st B = (A \ {( 0. L)}) holds for f be LinearCombination of A, u be set st u = ( Sum f) holds ex g be LinearCombination of B st u = ( Sum g)

    proof

      let L be add-associative left_zeroed right_zeroed right_complementable associative distributive well-unital non empty doubleLoopStr, A,B be non empty Subset of L;

      defpred P[ Nat] means for f be LinearCombination of A st ( len f) = $1 holds for u be set st u = ( Sum f) holds ex g be LinearCombination of B st u = ( Sum g);

      assume

       A1: B = (A \ {( 0. L)});

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];

        for f be LinearCombination of A st ( len f) = (k + 1) holds for u be set st u = ( Sum f) holds ex g be LinearCombination of B st u = ( Sum g)

        proof

          let f be LinearCombination of A;

          set g = (f | ( Seg k));

          reconsider g as FinSequence by FINSEQ_1: 15;

          

           A4: ( rng f) c= the carrier of L by FINSEQ_1:def 4;

          set h = (f /. ( len f));

          assume

           A5: ( len f) = (k + 1);

          then 1 <= ( len f) by NAT_1: 12;

          then ( len f) in ( Seg ( len f)) by FINSEQ_1: 1;

          then

           A6: ( len f) in ( dom f) by FINSEQ_1:def 3;

          then

           A7: h = (f . ( len f)) by PARTFUN1:def 6;

          

           A8: k <= (k + 1) by NAT_1: 12;

          then

           A9: ( len g) = k by A5, FINSEQ_1: 17;

          

           A10: ( dom g) = ( Seg k) by A5, A8, FINSEQ_1: 17;

          

           A11: ( dom f) = ( Seg (k + 1)) by A5, FINSEQ_1:def 3;

          then

           A12: ( dom g) c= ( dom f) by A8, A10, FINSEQ_1: 5;

          now

            let u be object;

            assume u in ( rng g);

            then

            consider x be object such that

             A13: x in ( dom g) and

             A14: u = (g . x) by FUNCT_1:def 3;

            (g . x) = (f . x) by A13, FUNCT_1: 47;

            then u in ( rng f) by A12, A13, A14, FUNCT_1:def 3;

            hence u in the carrier of L by A4;

          end;

          then ( rng g) c= the carrier of L;

          then

          reconsider g as FinSequence of the carrier of L by FINSEQ_1:def 4;

          for i be set st i in ( dom g) holds ex u,v be Element of L, a be Element of A st (g /. i) = ((u * a) * v)

          proof

            let i be set;

            assume

             A15: i in ( dom g);

            then

            reconsider i as Element of NAT ;

            i <= k by A10, A15, FINSEQ_1: 1;

            then

             A16: i <= (k + 1) by NAT_1: 12;

            1 <= i by A10, A15, FINSEQ_1: 1;

            then

             A17: i in ( dom f) by A11, A16, FINSEQ_1: 1;

            (g /. i) = (g . i) by A15, PARTFUN1:def 6

            .= (f . i) by A15, FUNCT_1: 47

            .= (f /. i) by A17, PARTFUN1:def 6;

            hence thesis by A17, IDEAL_1:def 8;

          end;

          then

          reconsider g as LinearCombination of A by IDEAL_1:def 8;

          consider g9 be LinearCombination of B such that

           A18: ( Sum g) = ( Sum g9) by A3, A9;

          let u be set;

          assume

           A19: u = ( Sum f);

          

           A20: ( len f) = (( len g) + 1) by A5, A8, FINSEQ_1: 17;

          then

           A21: ( Sum f) = (( Sum g) + h) by A10, A7, RLVECT_1: 38;

          now

            per cases ;

              case h = ( 0. L);

              hence ( Sum f) = ( Sum g) by A21, RLVECT_1:def 4;

            end;

              case

               A22: h <> ( 0. L);

              set l = (g9 ^ <*h*>);

              for i be set st i in ( dom l) holds ex u,v be Element of L, a be Element of B st (l /. i) = ((u * a) * v)

              proof

                let i be set;

                assume

                 A23: i in ( dom l);

                then

                reconsider i as Element of NAT ;

                

                 A24: ( len l) = (( len g9) + ( len <*h*>)) by FINSEQ_1: 22

                .= (( len g9) + 1) by FINSEQ_1: 39;

                now

                  per cases ;

                    case

                     A25: i = ( len l);

                    consider u,v be Element of L, a be Element of A such that

                     A26: (f /. ( len f)) = ((u * a) * v) by A6, IDEAL_1:def 8;

                     A27:

                    now

                      assume not a in B;

                      then a in {( 0. L)} by A1, XBOOLE_0:def 5;

                      then a = ( 0. L) by TARSKI:def 1;

                      

                      then ((u * a) * v) = (( 0. L) * v)

                      .= ( 0. L);

                      hence contradiction by A22, A26;

                    end;

                    (l /. i) = (l . i) by A23, PARTFUN1:def 6

                    .= h by A24, A25, FINSEQ_1: 42;

                    hence thesis by A26, A27;

                  end;

                    case

                     A28: i <> ( len l);

                    

                     A29: i in ( Seg ( len l)) by A23, FINSEQ_1:def 3;

                    then i <= ( len l) by FINSEQ_1: 1;

                    then i < ( len l) by A28, XXREAL_0: 1;

                    then

                     A30: i <= ( len g9) by A24, NAT_1: 13;

                    1 <= i by A29, FINSEQ_1: 1;

                    then i in ( Seg ( len g9)) by A30, FINSEQ_1: 1;

                    then

                     A31: i in ( dom g9) by FINSEQ_1:def 3;

                    (l /. i) = (l . i) by A23, PARTFUN1:def 6

                    .= (g9 . i) by A31, FINSEQ_1:def 7

                    .= (g9 /. i) by A31, PARTFUN1:def 6;

                    hence thesis by A31, IDEAL_1:def 8;

                  end;

                end;

                hence thesis;

              end;

              then

              reconsider l as LinearCombination of B by IDEAL_1:def 8;

              ( Sum l) = (( Sum g9) + ( Sum <*h*>)) by RLVECT_1: 41

              .= ( Sum f) by A10, A18, A7, A20, RLVECT_1: 38, RLVECT_1: 44;

              hence thesis by A19;

            end;

          end;

          hence thesis by A19, A18;

        end;

        hence P[(k + 1)];

      end;

      let f be LinearCombination of A, u be set;

      assume

       A32: u = ( Sum f);

      

       A33: ex n be Element of NAT st ( len f) = n;

      

       A34: P[ 0 ]

      proof

        set g = ( <*> the carrier of L);

        reconsider g as FinSequence of the carrier of L;

        for i be set st i in ( dom g) holds ex u,v be Element of L, a be Element of B st (g /. i) = ((u * a) * v);

        then

        reconsider g as LinearCombination of B by IDEAL_1:def 8;

        let f be LinearCombination of A;

        

         A35: g = ( <*> the carrier of L);

        assume ( len f) = 0 ;

        then

         A36: f = ( <*> the carrier of L);

        let u be set;

        assume u = ( Sum f);

        hence thesis by A36, A35;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A34, A2);

      hence thesis by A32, A33;

    end;

    theorem :: GROEB_1:36

    for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)) st I <> {( 0_ (n,L))} holds ex G be finite Subset of ( Polynom-Ring (n,L)) st G is_Groebner_basis_of (I,T) & not (( 0_ (n,L)) in G)

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L));

      assume

       A1: I <> {( 0_ (n,L))};

      

       A2: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      consider G be finite Subset of ( Polynom-Ring (n,L)) such that

       A3: G is_Groebner_basis_of (I,T) by Th35;

      set R = ( PolyRedRel (G,T));

      

       A4: (G -Ideal ) = I by A3;

      

       A5: ( PolyRedRel (G,T)) is locally-confluent by A3;

      set G9 = (G \ {( 0_ (n,L))}), R9 = ( PolyRedRel (G9,T));

      reconsider G9 as finite Subset of ( Polynom-Ring (n,L));

       A6:

      now

        per cases ;

          case

           A7: G9 = {} ;

          now

            per cases ;

              case G = {} ;

              hence (G9 -Ideal ) = I by A3;

            end;

              case

               A8: G <> {} ;

               A9:

              now

                let u be object;

                assume u in {( 0_ (n,L))};

                then

                 A10: u = ( 0_ (n,L)) by TARSKI:def 1;

                

                 A11: G c= {( 0_ (n,L))} by A7, XBOOLE_1: 37;

                now

                  assume not u in G;

                  then for v be object holds not v in G by A10, A11, TARSKI:def 1;

                  hence G = {} by XBOOLE_0:def 1;

                end;

                hence u in G by A8;

              end;

              

               A12: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

              now

                let u be object;

                assume

                 A13: u in G;

                G c= {( 0_ (n,L))} by A7, XBOOLE_1: 37;

                hence u in {( 0_ (n,L))} by A13;

              end;

              then G = {( 0_ (n,L))} by A9, TARSKI: 2;

              hence (G9 -Ideal ) = I by A1, A4, A12, IDEAL_1: 44;

            end;

          end;

          hence (G9 -Ideal ) = I;

        end;

          case G9 <> {} ;

          then

          reconsider GG = G, GG9 = G9 as non empty Subset of ( Polynom-Ring (n,L));

          

           A14: ( 0. ( Polynom-Ring (n,L))) = ( 0_ (n,L)) by POLYNOM1:def 11;

           A15:

          now

            let u be object;

            assume u in (G -Ideal );

            then ex f be LinearCombination of GG st u = ( Sum f) by IDEAL_1: 60;

            then ex g be LinearCombination of GG9 st u = ( Sum g) by A14, Lm9;

            hence u in (G9 -Ideal ) by IDEAL_1: 60;

          end;

          now

            let u be object;

            

             A16: (GG9 -Ideal ) c= (GG -Ideal ) by IDEAL_1: 57, XBOOLE_1: 36;

            assume u in (G9 -Ideal );

            hence u in (G -Ideal ) by A16;

          end;

          hence (G9 -Ideal ) = I by A4, A15, TARSKI: 2;

        end;

      end;

       A17:

      now

        assume ( 0_ (n,L)) in G9;

        then not ( 0_ (n,L)) in {( 0_ (n,L))} by XBOOLE_0:def 5;

        hence contradiction by TARSKI:def 1;

      end;

      

       A18: for u be object holds u in R implies u in R9

      proof

        let u be object;

        assume

         A19: u in R;

        then

        consider p,q be object such that

         A20: p in ( NonZero ( Polynom-Ring (n,L))) and

         A21: q in the carrier of ( Polynom-Ring (n,L)) and

         A22: u = [p, q] by ZFMISC_1:def 2;

        reconsider q as Polynomial of n, L by A21, POLYNOM1:def 11;

         not p in {( 0_ (n,L))} by A2, A20, XBOOLE_0:def 5;

        then p <> ( 0_ (n,L)) by TARSKI:def 1;

        then

        reconsider p as non-zero Polynomial of n, L by A20, POLYNOM1:def 11, POLYNOM7:def 1;

        p reduces_to (q,G,T) by A19, A22, POLYRED:def 13;

        then

        consider f be Polynomial of n, L such that

         A23: f in G and

         A24: p reduces_to (q,f,T) by POLYRED:def 7;

        ex b be bag of n st p reduces_to (q,f,b,T) by A24, POLYRED:def 6;

        then f <> ( 0_ (n,L)) by POLYRED:def 5;

        then not f in {( 0_ (n,L))} by TARSKI:def 1;

        then f in G9 by A23, XBOOLE_0:def 5;

        then p reduces_to (q,G9,T) by A24, POLYRED:def 7;

        hence thesis by A22, POLYRED:def 13;

      end;

      R9 c= R by Th4, XBOOLE_1: 36;

      then for u be object holds u in R9 implies u in R;

      then R9 is locally-confluent by A5, A18, TARSKI: 2;

      then G9 is_Groebner_basis_of (I,T) by A6;

      hence thesis by A17;

    end;

    definition

      let n be Ordinal, T be connected TermOrder of n, L be non empty multLoopStr_0, p be Polynomial of n, L;

      :: GROEB_1:def6

      pred p is_monic_wrt T means

      : Def6: ( HC (p,T)) = ( 1. L);

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      :: GROEB_1:def7

      pred P is_reduced_wrt T means for p be Polynomial of n, L st p in P holds p is_monic_wrt T & p is_irreducible_wrt ((P \ {p}),T);

    end

    notation

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      synonym P is_autoreduced_wrt T for P is_reduced_wrt T;

    end

    theorem :: GROEB_1:37

    

     Th37: for n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal Subset of ( Polynom-Ring (n,L)), m be Monomial of n, L, f,g be Polynomial of n, L st f in I & g in I & ( HM (f,T)) = m & ( HM (g,T)) = m holds not (ex p be Polynomial of n, L st p in I & p < (f,T) & ( HM (p,T)) = m) & not (ex p be Polynomial of n, L st p in I & p < (g,T) & ( HM (p,T)) = m) implies f = g

    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 almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal Subset of ( Polynom-Ring (n,L)), m be Monomial of n, L, f,g be Polynomial of n, L;

      assume that

       A1: f in I and

       A2: g in I and

       A3: ( HM (f,T)) = m and

       A4: ( HM (g,T)) = m;

      

       A5: ( HT (f,T)) = ( term ( HM (f,T))) by TERMORD: 22

      .= ( HT (g,T)) by A3, A4, TERMORD: 22;

      

       A6: ( HC (f,T)) = (f . ( HT (f,T))) by TERMORD:def 7

      .= (( HM (f,T)) . ( HT (f,T))) by TERMORD: 18

      .= (g . ( HT (g,T))) by A3, A4, A5, TERMORD: 18

      .= ( HC (g,T)) by TERMORD:def 7;

      assume that

       A7: not (ex p be Polynomial of n, L st p in I & p < (f,T) & ( HM (p,T)) = m) and

       A8: not (ex p be Polynomial of n, L st p in I & p < (g,T) & ( HM (p,T)) = m);

      reconsider I as LeftIdeal of ( Polynom-Ring (n,L)) by A1;

      per cases ;

        suppose (f - g) = ( 0_ (n,L));

        

        hence g = ((f - g) + g) by POLYRED: 2

        .= ((f + ( - g)) + g) by POLYNOM1:def 7

        .= (f + (( - g) + g)) by POLYNOM1: 21

        .= (f + ( 0_ (n,L))) by POLYRED: 3

        .= f by POLYNOM1: 23;

      end;

        suppose

         A9: (f - g) <> ( 0_ (n,L));

        now

          per cases ;

            case

             A10: f = ( 0_ (n,L));

            then ( HC (g,T)) = ( 0. L) by A6, TERMORD: 17;

            hence thesis by A10, TERMORD: 17;

          end;

            case

             A11: g = ( 0_ (n,L));

            then ( HC (f,T)) = ( 0. L) by A6, TERMORD: 17;

            hence thesis by A11, TERMORD: 17;

          end;

            case

             A12: f <> ( 0_ (n,L)) & g <> ( 0_ (n,L));

            set s = ( HT ((f - g),T));

            set d = ((f . s) - (g . s));

            set c = ((f . s) * (d " ));

            set h = (f - (c * (f - g)));

            

             A13: ( Support (f - g)) <> {} by A9, POLYNOM7: 1;

            then

             A14: ( HT ((f - g),T)) in ( Support (f - g)) by TERMORD:def 6;

             A15:

            now

              assume ( HT ((f - g),T)) = ( HT (f,T));

              

              then ((f - g) . ( HT ((f - g),T))) = ((f + ( - g)) . ( HT (f,T))) by POLYNOM1:def 7

              .= ((f . ( HT (f,T))) + (( - g) . ( HT (g,T)))) by A5, POLYNOM1: 15

              .= ((f . ( HT (f,T))) + ( - (g . ( HT (g,T))))) by POLYNOM1: 17

              .= (( HC (f,T)) + ( - (g . ( HT (g,T))))) by TERMORD:def 7

              .= (( HC (f,T)) + ( - ( HC (g,T)))) by TERMORD:def 7

              .= ( 0. L) by A6, RLVECT_1: 5;

              hence contradiction by A14, POLYNOM1:def 4;

            end;

            ( HT ((f - g),T)) <= (( max (( HT (f,T)),( HT (f,T)),T)),T) by A5, Th7;

            then ( HT ((f - g),T)) <= (( HT (f,T)),T) by TERMORD: 12;

            then ( HT ((f - g),T)) < (( HT (f,T)),T) by A15, TERMORD:def 3;

            then not ( HT (f,T)) <= (( HT ((f - g),T)),T) by TERMORD: 5;

            then not ( HT (f,T)) in ( Support (f - g)) by TERMORD:def 6;

            then

             A16: ((f - g) . ( HT (f,T))) = ( 0. L) by POLYNOM1:def 4;

            

             A17: (h . ( HT (f,T))) = ((f + ( - (c * (f - g)))) . ( HT (f,T))) by POLYNOM1:def 7

            .= ((f . ( HT (f,T))) + (( - (c * (f - g))) . ( HT (f,T)))) by POLYNOM1: 15

            .= ((f . ( HT (f,T))) + ( - ((c * (f - g)) . ( HT (f,T))))) by POLYNOM1: 17

            .= ((f . ( HT (f,T))) + ( - (c * ( 0. L)))) by A16, POLYNOM7:def 9

            .= ((f . ( HT (f,T))) + ( - ( 0. L)))

            .= ((f . ( HT (f,T))) + ( 0. L)) by RLVECT_1: 12

            .= (f . ( HT (f,T))) by RLVECT_1:def 4;

            ( Support f) <> {} by A12, POLYNOM7: 1;

            then ( HT (f,T)) in ( Support f) by TERMORD:def 6;

            then (h . ( HT (f,T))) <> ( 0. L) by A17, POLYNOM1:def 4;

            then

             A18: ( HT (f,T)) in ( Support h) by POLYNOM1:def 4;

            then

             A19: ( HT (f,T)) <= (( HT (h,T)),T) by TERMORD:def 6;

            ( Support h) = ( Support (f + ( - (c * (f - g))))) by POLYNOM1:def 7;

            then ( Support h) c= (( Support f) \/ ( Support ( - (c * (f - g))))) by POLYNOM1: 20;

            then

             A20: ( Support h) c= (( Support f) \/ ( Support (c * (f - g)))) by Th5;

            (( Support f) \/ ( Support (c * (f - g)))) c= (( Support f) \/ ( Support (f - g))) by POLYRED: 19, XBOOLE_1: 9;

            then

             A21: ( Support h) c= (( Support f) \/ ( Support (f - g))) by A20;

             not g < (f,T) by A2, A4, A7;

            then

             A22: f <= (g,T) by POLYRED: 29;

             not f < (g,T) by A1, A3, A8;

            then g <= (f,T) by POLYRED: 29;

            then

             A23: ( Support f) = ( Support g) by A22, POLYRED: 26;

            ( Support (f - g)) = ( Support (f + ( - g))) & ( Support (f + ( - g))) c= (( Support f) \/ ( Support ( - g))) by POLYNOM1: 20, POLYNOM1:def 7;

            then

             A24: ( Support (f - g)) c= (( Support f) \/ ( Support g)) by Th5;

            then

             A25: (( Support f) \/ ( Support (f - g))) c= (( Support f) \/ ( Support f)) by A23, XBOOLE_1: 9;

            then

             A26: ( Support h) c= ( Support f) by A21;

            ( HT (h,T)) in ( Support h) by A18, TERMORD:def 6;

            then ( HT (h,T)) <= (( HT (f,T)),T) by A26, TERMORD:def 6;

            then

             A27: ( HT (h,T)) = ( HT (f,T)) by A19, TERMORD: 7;

            

            then ( HC (h,T)) = (f . ( HT (f,T))) by A17, TERMORD:def 7

            .= ( HC (f,T)) by TERMORD:def 7;

            

            then

             A28: ( HM (h,T)) = ( Monom (( HC (f,T)),( HT (f,T)))) by A27, TERMORD:def 8

            .= m by A3, TERMORD:def 8;

            reconsider cp = ((c | (n,L)) *' (f - g)) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

            reconsider cc = (c | (n,L)) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

            reconsider f9 = f, g9 = g as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

            

             A29: ((f - g) . s) = ((f + ( - g)) . s) by POLYNOM1:def 7

            .= ((f . s) + (( - g) . s)) by POLYNOM1: 15

            .= ((f . s) + ( - (g . s))) by POLYNOM1: 17

            .= ((f . s) - (g . s));

            

             A30: s in ( Support (f - g)) by A13, TERMORD:def 6;

             A31:

            now

              

               A32: ((f - g) . s) <> ( 0. L) by A30, POLYNOM1:def 4;

              

               A33: ( - (c * ((f . s) - (g . s)))) = ( - ((f . s) * ((((f . s) - (g . s)) " ) * ((f . s) - (g . s))))) by GROUP_1:def 3

              .= ( - ((f . s) * ( 1. L))) by A29, A32, VECTSP_1:def 10

              .= ( - (f . s));

              assume

               A34: ( Support h) = ( Support f);

              (h . s) = ((f + ( - (c * (f - g)))) . s) by POLYNOM1:def 7

              .= ((f . s) + (( - (c * (f - g))) . s)) by POLYNOM1: 15

              .= ((f . s) + ((( - c) * (f - g)) . s)) by POLYRED: 9

              .= ((f . s) + (( - c) * ((f - g) . s))) by POLYNOM7:def 9

              .= ((f . s) + ( - (f . s))) by A29, A33, VECTSP_1: 9

              .= ( 0. L) by RLVECT_1: 5;

              hence contradiction by A23, A14, A24, A34, POLYNOM1:def 4;

            end;

            h <= (f,T) by A21, A25, Th8, XBOOLE_1: 1;

            then

             A35: h < (f,T) by A31, POLYRED:def 3;

            reconsider cp as Element of ( Polynom-Ring (n,L));

            reconsider cc as Element of ( Polynom-Ring (n,L));

            reconsider f9, g9 as Element of ( Polynom-Ring (n,L));

            (f - g) = (f9 - g9) by Lm2;

            then

             A36: cp = (cc * (f9 - g9)) by POLYNOM1:def 11;

            (f9 - g9) in I by A1, A2, IDEAL_1: 15;

            then

             A37: (cc * (f9 - g9)) in I by IDEAL_1:def 2;

            (f9 - cp) = (f - ((c | (n,L)) *' (f - g))) by Lm2

            .= (f - (c * (f - g))) by POLYNOM7: 27;

            hence contradiction by A1, A7, A28, A35, A37, A36, IDEAL_1: 15;

          end;

        end;

        hence thesis;

      end;

    end;

    

     Lm10: for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, p be Polynomial of n, L, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)) st p in I & p <> ( 0_ (n,L)) holds ex q be Polynomial of n, L st q in I & ( HM (q,T)) = ( Monom (( 1. L),( HT (p,T)))) & q <> ( 0_ (n,L))

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, p be Polynomial of n, L, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L));

      assume that

       A1: p in I and

       A2: p <> ( 0_ (n,L));

      set c = (( HC (p,T)) " );

      

       A3: ( HC (p,T)) <> ( 0. L) by A2, TERMORD: 17;

      now

        assume c = ( 0. L);

        

        then ( 0. L) = (c * ( HC (p,T)))

        .= ( 1. L) by A3, VECTSP_1:def 10;

        hence contradiction;

      end;

      then

      reconsider c as non zero Element of L by STRUCT_0:def 12;

      set q = (c * p);

      take q;

      reconsider pp = p, cc = (c | (n,L)) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      reconsider pp, cc as Element of ( Polynom-Ring (n,L));

      q = ((c | (n,L)) *' p) by POLYNOM7: 27

      .= (cc * pp) by POLYNOM1:def 11;

      hence q in I by A1, IDEAL_1:def 2;

      

       A4: ( HT (q,T)) = ( HT (p,T)) by POLYRED: 21;

      

      then ( HC (q,T)) = (q . ( HT (p,T))) by TERMORD:def 7

      .= (c * (p . ( HT (p,T)))) by POLYNOM7:def 9

      .= (( HC (p,T)) * (( HC (p,T)) " )) by TERMORD:def 7

      .= ( 1. L) by A3, VECTSP_1:def 10;

      hence ( HM (q,T)) = ( Monom (( 1. L),( HT (p,T)))) by A4, TERMORD:def 8;

      

      then ( 1. L) = ( coefficient ( HM (q,T))) by POLYNOM7: 9

      .= ( HC (q,T)) by TERMORD: 22;

      then ( HC (q,T)) <> ( 0. L);

      hence thesis by TERMORD: 17;

    end;

    theorem :: GROEB_1:38

    for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)), G be Subset of ( Polynom-Ring (n,L)), p be Polynomial of n, L, q be non-zero Polynomial of n, L st p in G & q in G & p <> q & ( HT (q,T)) divides ( HT (p,T)) holds G is_Groebner_basis_of (I,T) implies (G \ {p}) is_Groebner_basis_of (I,T)

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)), G be Subset of ( Polynom-Ring (n,L)), p be Polynomial of n, L, q be non-zero Polynomial of n, L;

      assume that

       A1: p in G and

       A2: q in G and

       A3: p <> q and

       A4: ( HT (q,T)) divides ( HT (p,T));

      reconsider GG = G as non empty Subset of ( Polynom-Ring (n,L)) by A1;

      assume

       A5: G is_Groebner_basis_of (I,T);

      set G9 = (G \ {p});

      

       A6: not q in {p} by A3, TARSKI:def 1;

      then q <> ( 0_ (n,L)) & q in G9 by A2, POLYNOM7:def 1, XBOOLE_0:def 5;

      then

       A7: ( HT (q,T)) in { ( HT (u,T)) where u be Polynomial of n, L : u in G9 & u <> ( 0_ (n,L)) };

      GG c= (GG -Ideal ) by IDEAL_1:def 14;

      then

       A8: G c= I by A5;

      for f be Polynomial of n, L st f in I holds ( PolyRedRel (G,T)) reduces (f,( 0_ (n,L))) by A1, A5, Th24;

      then for f be non-zero Polynomial of n, L st f in I holds f is_reducible_wrt (G,T) by Th25;

      then

       A9: for f be non-zero Polynomial of n, L st f in I holds f is_top_reducible_wrt (G,T) by A8, Th26;

      for b be bag of n st b in ( HT (I,T)) holds ex b9 be bag of n st b9 in ( HT (G9,T)) & b9 divides b

      proof

        let b be bag of n;

        assume b in ( HT (I,T));

        then

        consider bb be bag of n such that

         A10: bb in ( HT (G,T)) and

         A11: bb divides b by A9, Th27;

        consider r be Polynomial of n, L such that

         A12: bb = ( HT (r,T)) and

         A13: r in G and

         A14: r <> ( 0_ (n,L)) by A10;

        now

          per cases ;

            case r = p;

            hence thesis by A4, A7, A11, A12, Lm8;

          end;

            case r <> p;

            then not r in {p} by TARSKI:def 1;

            then r in G9 by A13, XBOOLE_0:def 5;

            then bb in { ( HT (u,T)) where u be Polynomial of n, L : u in G9 & u <> ( 0_ (n,L)) } by A12, A14;

            hence thesis by A11;

          end;

        end;

        hence thesis;

      end;

      then

       A15: ( HT (I,T)) c= ( multiples ( HT (G9,T))) by Th28;

      G9 c= G by XBOOLE_1: 36;

      then

       A16: G9 c= I by A8;

      G9 <> {} by A2, A6, XBOOLE_0:def 5;

      hence thesis by A16, A15, Th29;

    end;

    theorem :: GROEB_1:39

    for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)) st I <> {( 0_ (n,L))} holds ex G be finite Subset of ( Polynom-Ring (n,L)) st G is_Groebner_basis_of (I,T) & G is_reduced_wrt T

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L));

      set R = RelStr (# ( Bags n), ( DivOrder n) #);

      assume

       A1: I <> {( 0_ (n,L))};

      ex q be Element of I st q <> ( 0_ (n,L))

      proof

        assume

         A2: not (ex q be Element of I st q <> ( 0_ (n,L)));

         A3:

        now

          let u be object;

          assume u in {( 0_ (n,L))};

          then

           A4: u = ( 0_ (n,L)) by TARSKI:def 1;

          now

            assume not u in I;

            then for v be object holds not v in I by A2, A4;

            hence thesis by XBOOLE_0:def 1;

          end;

          hence u in I;

        end;

        now

          let u be object;

          assume u in I;

          then u = ( 0_ (n,L)) by A2;

          hence u in {( 0_ (n,L))} by TARSKI:def 1;

        end;

        hence thesis by A1, A3, TARSKI: 2;

      end;

      then

      consider q be Element of I such that

       A5: q <> ( 0_ (n,L));

      reconsider q as Polynomial of n, L by POLYNOM1:def 11;

      ( HT (q,T)) in { ( HT (p,T)) where p be Polynomial of n, L : p in I & p <> ( 0_ (n,L)) } by A5;

      then

      reconsider hti = ( HT (I,T)) as non empty Subset of R;

      set hq = ( HT (q,T));

      consider S be set such that

       A6: S is_Dickson-basis_of (hti,R) and

       A7: for C be set st C is_Dickson-basis_of (hti,R) holds S c= C by DICKSON: 34;

      reconsider hq as Element of R;

       A8:

      now

        

         A9: ex B be set st B is_Dickson-basis_of (hti,R) & B is finite by DICKSON:def 10;

        assume S is non finite;

        hence contradiction by A7, A9, FINSET_1: 1;

      end;

      

       A10: S c= hti by A6, DICKSON:def 9;

      now

        let u be object;

        assume u in S;

        then u in hti by A10;

        hence u in ( Bags n);

      end;

      then

      reconsider S as finite Subset of ( Bags n) by A8, TARSKI:def 3;

      set M = { { p where p be Polynomial of n, L : p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s))) } where s be Element of ( Bags n) : s in S };

      set s = the Element of S;

      hq in { ( HT (p,T)) where p be Polynomial of n, L : p in I & p <> ( 0_ (n,L)) } by A5;

      then

       A11: ex b be Element of R st b in S & b <= hq by A6, DICKSON:def 9;

      then s in S;

      then

      reconsider s as Element of ( Bags n);

      { p where p be Polynomial of n, L : p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) & not (ex r be Polynomial of n, L st r in I & r < (p,T) & r <> ( 0_ (n,L)) & ( HM (r,T)) = ( Monom (( 1. L),s))) } in M by A11;

      then

      reconsider M as non empty set;

      set G = { r where r be Polynomial of n, L : ex x be Element of M st x = {r} };

      

       A12: for x be set st x in M holds ex q be Polynomial of n, L st q in I & x = {q} & q <> ( 0_ (n,L))

      proof

        let x be set;

        assume x in M;

        then

        consider s be Element of ( Bags n) such that

         A13: x = { p where p be Polynomial of n, L : p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s))) } and

         A14: s in S;

        s in hti by A10, A14;

        then

        consider q be Polynomial of n, L such that

         A15: s = ( HT (q,T)) and

         A16: q in I & q <> ( 0_ (n,L));

        consider qq be Polynomial of n, L such that

         A17: qq in I & ( HM (qq,T)) = ( Monom (( 1. L),( HT (q,T)))) & qq <> ( 0_ (n,L)) by A16, Lm10;

        set M9 = { p where p be Polynomial of n, L : p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) };

         A18:

        now

          let u be object;

          assume u in M9;

          then ex pp be Polynomial of n, L st u = pp & pp in I & ( HM (pp,T)) = ( Monom (( 1. L),s)) & pp <> ( 0_ (n,L));

          hence u in the carrier of ( Polynom-Ring (n,L));

        end;

        qq in M9 by A15, A17;

        then

        reconsider M9 as non empty Subset of ( Polynom-Ring (n,L)) by A18, TARSKI:def 3;

        reconsider M9 as non empty Subset of ( Polynom-Ring (n,L));

        consider p be Polynomial of n, L such that

         A19: p in M9 and

         A20: for r be Polynomial of n, L st r in M9 holds p <= (r,T) by POLYRED: 31;

        consider p9 be Polynomial of n, L such that

         A21: p9 = p and

         A22: p9 in I and

         A23: ( HM (p9,T)) = ( Monom (( 1. L),s)) and

         A24: p9 <> ( 0_ (n,L)) by A19;

         A25:

        now

          assume ex q be Polynomial of n, L st q in I & q < (p9,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s));

          then

          consider q be Polynomial of n, L such that

           A26: q in I and

           A27: q < (p9,T) and

           A28: q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s));

          q in M9 by A26, A28;

          then p <= (q,T) by A20;

          hence contradiction by A21, A27, POLYRED: 29;

        end;

         A29:

        now

          

           A30: ( 1. L) <> ( 0. L);

          assume ex q be Polynomial of n, L st q in I & q < (p9,T) & ( HM (q,T)) = ( Monom (( 1. L),s));

          then

          consider q be Polynomial of n, L such that

           A31: q in I & q < (p9,T) and

           A32: ( HM (q,T)) = ( Monom (( 1. L),s));

          ( HC (q,T)) = ( coefficient ( Monom (( 1. L),s))) by A32, TERMORD: 22

          .= ( 1. L) by POLYNOM7: 9;

          then q <> ( 0_ (n,L)) by A30, TERMORD: 17;

          hence contradiction by A25, A31, A32;

        end;

         A33:

        now

          let u be object;

          assume u in x;

          then

          consider u9 be Polynomial of n, L such that

           A34: u9 = u and

           A35: u9 in I & ( HM (u9,T)) = ( Monom (( 1. L),s)) and u9 <> ( 0_ (n,L)) and

           A36: not (ex q be Polynomial of n, L st q in I & q < (u9,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s))) by A13;

          now

            

             A37: ( 1. L) <> ( 0. L);

            assume ex q be Polynomial of n, L st q in I & q < (u9,T) & ( HM (q,T)) = ( Monom (( 1. L),s));

            then

            consider q be Polynomial of n, L such that

             A38: q in I & q < (u9,T) and

             A39: ( HM (q,T)) = ( Monom (( 1. L),s));

            ( HC (q,T)) = ( coefficient ( Monom (( 1. L),s))) by A39, TERMORD: 22

            .= ( 1. L) by POLYNOM7: 9;

            then q <> ( 0_ (n,L)) by A37, TERMORD: 17;

            hence contradiction by A36, A38, A39;

          end;

          then u9 = p9 by A22, A23, A29, A35, Th37;

          hence u in {p9} by A34, TARSKI:def 1;

        end;

        take p9;

        p9 in x by A13, A22, A23, A24, A25;

        then for u be object holds u in {p9} implies u in x by TARSKI:def 1;

        hence thesis by A22, A24, A33, TARSKI: 2;

      end;

      now

        let u be object;

        assume u in G;

        then

        consider r be Polynomial of n, L such that

         A40: u = r and

         A41: ex x be Element of M st x = {r};

        consider x be Element of M such that

         A42: x = {r} by A41;

        consider r9 be Polynomial of n, L such that

         A43: r9 in I and

         A44: x = {r9} and r9 <> ( 0_ (n,L)) by A12;

        r9 in {r} by A42, A44, TARSKI:def 1;

        hence u in I by A40, A43, TARSKI:def 1;

      end;

      then

       A45: G c= I;

      

       A46: M is finite

      proof

        defpred P[ object, object] means $2 = { p where p be Polynomial of n, L : ex b be bag of n st b = $1 & p in I & ( HM (p,T)) = ( Monom (( 1. L),b)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),b))) };

        

         A47: for x be object st x in S holds ex y be object st P[x, y];

        consider f be Function such that

         A48: ( dom f) = S & for x be object st x in S holds P[x, (f . x)] from CLASSES1:sch 1( A47);

         A49:

        now

          let u be object;

          assume u in ( rng f);

          then

          consider s be object such that

           A50: s in ( dom f) and

           A51: u = (f . s) by FUNCT_1:def 3;

          reconsider s as Element of ( Bags n) by A48, A50;

          set V = { p where p be Polynomial of n, L : p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s))) };

          

           A52: ex b be bag of n st (f . s) = { p where p be Polynomial of n, L : ex b be bag of n st b = s & p in I & ( HM (p,T)) = ( Monom (( 1. L),b)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),b))) } by A48, A50;

           A53:

          now

            let v be object;

            assume v in V;

            then ex p be Polynomial of n, L st v = p & p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s)));

            hence v in (f . s) by A52;

          end;

          now

            let v be object;

            assume v in (f . s);

            then ex p be Polynomial of n, L st v = p & ex b be bag of n st b = s & p in I & ( HM (p,T)) = ( Monom (( 1. L),b)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),b))) by A52;

            hence v in V;

          end;

          then u = { p where p be Polynomial of n, L : p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s))) } by A51, A53, TARSKI: 2;

          hence u in M by A48, A50;

        end;

        now

          let u be object;

          reconsider uu = u as set by TARSKI: 1;

          assume u in M;

          then

          consider s be Element of ( Bags n) such that

           A54: u = { p where p be Polynomial of n, L : p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s))) } and

           A55: s in S;

          

           A56: ex b be bag of n st (f . s) = { p where p be Polynomial of n, L : ex b be bag of n st b = s & p in I & ( HM (p,T)) = ( Monom (( 1. L),b)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),b))) } by A48, A55;

           A57:

          now

            let v be object;

            assume v in uu;

            then ex p be Polynomial of n, L st v = p & p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s))) by A54;

            hence v in (f . s) by A56;

          end;

           A58:

          now

            let v be object;

            assume v in (f . s);

            then ex p be Polynomial of n, L st v = p & ex b be bag of n st b = s & p in I & ( HM (p,T)) = ( Monom (( 1. L),b)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),b))) by A56;

            hence v in uu by A54;

          end;

          (f . s) in ( rng f) by A48, A55, FUNCT_1: 3;

          hence u in ( rng f) by A57, A58, TARSKI: 2;

        end;

        then ( rng f) = M by A49, TARSKI: 2;

        hence thesis by A48, FINSET_1: 8;

      end;

      

       A59: G is finite

      proof

        defpred P[ object, object] means ex p be Polynomial of n, L, x be Element of M st $1 = x & $2 = p & x = {p};

        

         A60: for x be object st x in M holds ex y be object st P[x, y]

        proof

          let x be object;

          assume

           A61: x in M;

          then

          reconsider x9 = x as Element of M;

          consider q be Polynomial of n, L such that q in I and

           A62: x = {q} and q <> ( 0_ (n,L)) by A12, A61;

          take q;

          take q, x9;

          thus x = x9;

          thus q = q;

          thus thesis by A62;

        end;

        consider f be Function such that

         A63: ( dom f) = M & for x be object st x in M holds P[x, (f . x)] from CLASSES1:sch 1( A60);

         A64:

        now

          let u be object;

          assume u in G;

          then

          consider r be Polynomial of n, L such that

           A65: u = r and

           A66: ex x be Element of M st x = {r};

          consider x be Element of M such that

           A67: x = {r} by A66;

           P[x, (f . x)] by A63;

          then

          consider p9 be Polynomial of n, L, x9 be Element of M such that x9 = x and

           A68: p9 = (f . x) and

           A69: x = {p9};

          

           A70: (f . x) in ( rng f) by A63, FUNCT_1: 3;

          p9 in {r} by A67, A69, TARSKI:def 1;

          hence u in ( rng f) by A65, A70, A68, TARSKI:def 1;

        end;

        now

          let u be object;

          assume u in ( rng f);

          then

          consider s be object such that

           A71: s in ( dom f) and

           A72: u = (f . s) by FUNCT_1:def 3;

          reconsider s as Element of M by A63, A71;

          ex p9 be Polynomial of n, L, x9 be Element of M st x9 = s & p9 = (f . s) & x9 = {p9} by A63;

          hence u in G by A72;

        end;

        then ( rng f) = G by A64, TARSKI: 2;

        hence thesis by A46, A63, FINSET_1: 8;

      end;

      now

        let u be object;

        assume u in G;

        then ex r be Polynomial of n, L st u = r & ex x be Element of M st x = {r};

        hence u in the carrier of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      end;

      then

      reconsider G as Subset of ( Polynom-Ring (n,L)) by TARSKI:def 3;

      G <> {}

      proof

        set z = the Element of M;

        consider r be Polynomial of n, L such that r in I and

         A73: z = {r} and r <> ( 0_ (n,L)) by A12;

        r in G by A73;

        hence thesis;

      end;

      then

      reconsider G as non empty finite Subset of ( Polynom-Ring (n,L)) by A59;

      take G;

      for b be bag of n st b in ( HT (I,T)) holds ex b9 be bag of n st b9 in ( HT (G,T)) & b9 divides b

      proof

        let b be bag of n;

        reconsider bb = b as Element of R by PRE_POLY:def 12;

        assume b in ( HT (I,T));

        then

        consider bb9 be Element of R such that

         A74: bb9 in S and

         A75: bb9 <= bb by A6, DICKSON:def 9;

        

         A76: [bb9, bb] in ( DivOrder n) by A75, ORDERS_2:def 5;

        reconsider b9 = bb9 as bag of n;

        set N = { p where p be Polynomial of n, L : p in I & ( HM (p,T)) = ( Monom (( 1. L),b9)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),b9))) };

        N in M by A74;

        then

        reconsider N as Element of M;

        take b9;

        consider r be Polynomial of n, L such that r in I and

         A77: N = {r} and r <> ( 0_ (n,L)) by A12;

        r in N by A77, TARSKI:def 1;

        then

        consider r9 be Polynomial of n, L such that

         A78: r = r9 and r9 in I and

         A79: ( HM (r9,T)) = ( Monom (( 1. L),b9)) and

         A80: r9 <> ( 0_ (n,L)) and not (ex q be Polynomial of n, L st q in I & q < (r9,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),b9)));

        

         A81: r9 in G by A77, A78;

        b9 = ( term ( HM (r9,T))) by A79, POLYNOM7: 10

        .= ( HT (r9,T)) by TERMORD: 22;

        hence thesis by A76, A80, A81, Def5;

      end;

      then ( HT (I,T)) c= ( multiples ( HT (G,T))) by Th28;

      hence G is_Groebner_basis_of (I,T) by A45, Th29;

      now

        let q be Polynomial of n, L;

        assume

         A82: q in G;

        then

        consider rr be Polynomial of n, L such that

         A83: q = rr and

         A84: ex x be Element of M st x = {rr};

        consider x be Element of M such that

         A85: x = {rr} by A84;

        x in M;

        then

        consider s be Element of ( Bags n) such that

         A86: x = { p where p be Polynomial of n, L : p in I & ( HM (p,T)) = ( Monom (( 1. L),s)) & p <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s))) } and

         A87: s in S;

        rr in x by A85, TARSKI:def 1;

        then

        consider p be Polynomial of n, L such that

         A88: rr = p and p in I and

         A89: ( HM (p,T)) = ( Monom (( 1. L),s)) and p <> ( 0_ (n,L)) and

         A90: not (ex q be Polynomial of n, L st q in I & q < (p,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),s))) by A86;

        

         A91: ( 1. L) = ( coefficient ( HM (rr,T))) by A88, A89, POLYNOM7: 9

        .= ( HC (rr,T)) by TERMORD: 22;

        hence q is_monic_wrt T by A83;

        

         A92: s = ( term ( HM (rr,T))) by A88, A89, POLYNOM7: 10

        .= ( HT (q,T)) by A83, TERMORD: 22;

        now

          reconsider htq = ( HT (q,T)) as Element of R;

          assume q is_reducible_wrt ((G \ {q}),T);

          then

          consider pp be Polynomial of n, L such that

           A93: q reduces_to (pp,(G \ {q}),T) by POLYRED:def 9;

          consider g be Polynomial of n, L such that

           A94: g in (G \ {q}) and

           A95: q reduces_to (pp,g,T) by A93, POLYRED:def 7;

          

           A96: g in G by A94, XBOOLE_0:def 5;

          

           A97: not g in {q} by A94, XBOOLE_0:def 5;

          reconsider htg = ( HT (g,T)) as Element of R;

          consider b be bag of n such that

           A98: q reduces_to (pp,g,b,T) by A95, POLYRED:def 6;

          

           A99: b in ( Support q) by A98, POLYRED:def 5;

          

           A100: ex s be bag of n st (s + ( HT (g,T))) = b & pp = (q - (((q . b) / ( HC (g,T))) * (s *' g))) by A98, POLYRED:def 5;

          now

            per cases ;

              case

               A101: b = ( HT (q,T));

              set S9 = (S \ {htq});

              consider z be Polynomial of n, L such that

               A102: g = z and

               A103: ex x be Element of M st x = {z} by A96;

              consider x1 be Element of M such that

               A104: x1 = {z} by A103;

              x1 in M;

              then

              consider t be Element of ( Bags n) such that

               A105: x1 = { u where u be Polynomial of n, L : u in I & ( HM (u,T)) = ( Monom (( 1. L),t)) & u <> ( 0_ (n,L)) & not (ex q be Polynomial of n, L st q in I & q < (u,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),t))) } and

               A106: t in S;

              z in x1 by A104, TARSKI:def 1;

              then

              consider p1 be Polynomial of n, L such that

               A107: z = p1 and p1 in I and

               A108: ( HM (p1,T)) = ( Monom (( 1. L),t)) and p1 <> ( 0_ (n,L)) and not (ex q be Polynomial of n, L st q in I & q < (p1,T) & q <> ( 0_ (n,L)) & ( HM (q,T)) = ( Monom (( 1. L),t))) by A105;

              

               A109: t = ( term ( HM (p1,T))) by A108, POLYNOM7: 10

              .= htg by A102, A107, TERMORD: 22;

              now

                assume htg in {htq};

                then t = s by A92, A109, TARSKI:def 1;

                hence contradiction by A83, A85, A86, A97, A102, A104, A105, TARSKI:def 1;

              end;

              then

               A110: htg in S9 by A106, A109, XBOOLE_0:def 5;

              ( HT (g,T)) divides ( HT (q,T)) by A100, A101, PRE_POLY: 50;

              then [htg, htq] in ( DivOrder n) by Def5;

              then

               A111: htg <= htq by ORDERS_2:def 5;

               A112:

              now

                let a be Element of R;

                assume a in hti;

                then

                consider b be Element of R such that

                 A113: b in S and

                 A114: b <= a by A6, DICKSON:def 9;

                now

                  per cases ;

                    case b in S9;

                    hence ex b be Element of R st b in S9 & b <= a by A114;

                  end;

                    case not b in S9;

                    then b in {htq} by A113, XBOOLE_0:def 5;

                    then htg <= b by A111, TARSKI:def 1;

                    hence ex b be Element of R st b in S9 & b <= a by A110, A114, ORDERS_2: 3;

                  end;

                end;

                hence ex b be Element of R st b in S9 & b <= a;

              end;

               A115:

              now

                assume htq in S9;

                then not htq in {htq} by XBOOLE_0:def 5;

                hence contradiction by TARSKI:def 1;

              end;

              S9 c= S by XBOOLE_1: 36;

              then S9 c= hti by A10;

              then S9 is_Dickson-basis_of (hti,R) by A112, DICKSON:def 9;

              then S c= S9 by A7;

              hence q is_irreducible_wrt ((G \ {q}),T) by A87, A92, A115;

            end;

              case

               A116: b <> ( HT (q,T));

              b <= (( HT (q,T)),T) by A99, TERMORD:def 6;

              then b < (( HT (q,T)),T) by A116, TERMORD:def 3;

              

              then

               A117: (pp . ( HT (q,T))) = (q . ( HT (q,T))) by A98, POLYRED: 41

              .= ( 1. L) by A83, A91, TERMORD:def 7;

              ( 1. L) <> ( 0. L);

              then

               A118: ( HT (q,T)) in ( Support pp) by A117, POLYNOM1:def 4;

              now

                

                 A119: b <= (( HT (q,T)),T) by A99, TERMORD:def 6;

                assume

                 A120: ( HT (q,T)) < (( HT (pp,T)),T);

                then ( HT (q,T)) <= (( HT (pp,T)),T) by TERMORD:def 3;

                then b <= (( HT (pp,T)),T) & b <> ( HT (pp,T)) by A116, A119, TERMORD: 7, TERMORD: 8;

                then b < (( HT (pp,T)),T) by TERMORD:def 3;

                then ( HT (pp,T)) in ( Support q) iff ( HT (pp,T)) in ( Support pp) by A98, POLYRED: 40;

                then ( HT (pp,T)) <= (( HT (q,T)),T) by A118, TERMORD:def 6;

                hence contradiction by A120, TERMORD: 5;

              end;

              then

               A121: ( HT (pp,T)) <= (( HT (q,T)),T) by TERMORD: 5;

              ( HT (q,T)) <= (( HT (pp,T)),T) by A118, TERMORD:def 6;

              then ( HT (pp,T)) = ( HT (q,T)) by A121, TERMORD: 7;

              then ( Monom (( HC (pp,T)),( HT (pp,T)))) = ( Monom (( 1. L),s)) by A92, A117, TERMORD:def 7;

              then

               A122: ( HM (pp,T)) = ( HM (q,T)) by A83, A88, A89, TERMORD:def 8;

               A123:

              now

                assume pp = ( 0_ (n,L));

                

                then ( 0. L) = ( HC (pp,T)) by TERMORD: 17

                .= ( coefficient ( HM (pp,T))) by TERMORD: 22

                .= ( 1. L) by A83, A91, A122, TERMORD: 22;

                hence contradiction;

              end;

              consider m be Monomial of n, L such that

               A124: pp = (q - (m *' g)) by A95, Th1;

              reconsider gg = g, qq = q, mm = m as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

              reconsider gg, qq, mm as Element of ( Polynom-Ring (n,L));

              g in G by A94, XBOOLE_0:def 5;

              then (mm * gg) in I by A45, IDEAL_1:def 2;

              then ( - (mm * gg)) in I by IDEAL_1: 13;

              then

               A125: (qq + ( - (mm * gg))) in I by A45, A82, IDEAL_1:def 1;

              (mm * gg) = (m *' g) by POLYNOM1:def 11;

              then (q - (m *' g)) = (qq - (mm * gg)) by Lm2;

              then pp in I by A124, A125;

              hence contradiction by A83, A88, A89, A90, A95, A122, A123, POLYRED: 43;

            end;

          end;

          hence q is_irreducible_wrt ((G \ {q}),T);

        end;

        hence q is_irreducible_wrt ((G \ {q}),T);

      end;

      hence thesis;

    end;

    theorem :: GROEB_1:40

    for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)), G1,G2 be non empty finite Subset of ( Polynom-Ring (n,L)) st G1 is_Groebner_basis_of (I,T) & G1 is_reduced_wrt T & G2 is_Groebner_basis_of (I,T) & G2 is_reduced_wrt T holds G1 = G2

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, I be add-closed left-ideal non empty Subset of ( Polynom-Ring (n,L)), G,H be finite non empty Subset of ( Polynom-Ring (n,L));

      assume that

       A1: G is_Groebner_basis_of (I,T) and

       A2: G is_reduced_wrt T and

       A3: H is_Groebner_basis_of (I,T) and

       A4: H is_reduced_wrt T;

      

       A5: (H -Ideal ) = I by A3;

      set GH = ((G \/ H) \ (G /\ H));

      assume

       A6: G <> H;

      now

        assume GH = {} ;

        then

         A7: (G \/ H) c= (G /\ H) by XBOOLE_1: 37;

         A8:

        now

          let u be object;

          assume u in H;

          then u in (G \/ H) by XBOOLE_0:def 3;

          hence u in G by A7, XBOOLE_0:def 4;

        end;

        now

          let u be object;

          assume u in G;

          then u in (G \/ H) by XBOOLE_0:def 3;

          hence u in H by A7, XBOOLE_0:def 4;

        end;

        hence contradiction by A6, A8, TARSKI: 2;

      end;

      then

      reconsider GH as non empty Subset of ( Polynom-Ring (n,L));

       A9:

      now

        let u be object;

        assume

         A10: u in GH;

        then

         A11: not u in (G /\ H) by XBOOLE_0:def 5;

        

         A12: u in (G \/ H) by A10, XBOOLE_0:def 5;

        u in (G \ H) or u in (H \ G)

        proof

          assume

           A13: not u in (G \ H);

          now

            per cases by A13, XBOOLE_0:def 5;

              case not u in G;

              hence not u in G & u in H by A12, XBOOLE_0:def 3;

            end;

              case u in H;

              hence u in H & not u in G by A11, XBOOLE_0:def 4;

            end;

          end;

          hence thesis by XBOOLE_0:def 5;

        end;

        hence u in ((G \ H) \/ (H \ G)) by XBOOLE_0:def 3;

      end;

      consider g be Polynomial of n, L such that

       A14: g in GH and

       A15: for q be Polynomial of n, L st q in GH holds g <= (q,T) by POLYRED: 31;

      

       A16: (G -Ideal ) = I by A1;

       A17:

      now

        let u be set;

        assume

         A18: u in G or u in H;

        now

          per cases by A18;

            case

             A19: u in G;

            then

            reconsider u9 = u as Element of ( Polynom-Ring (n,L));

            reconsider u9 as Polynomial of n, L by POLYNOM1:def 11;

            u9 is_monic_wrt T by A2, A19;

            then

             A20: ( HC (u9,T)) = ( 1. L);

            ( 1. L) <> ( 0. L);

            hence u is Polynomial of n, L & u <> ( 0_ (n,L)) by A20, TERMORD: 17;

          end;

            case

             A21: u in H;

            then

            reconsider u9 = u as Element of ( Polynom-Ring (n,L));

            reconsider u9 as Polynomial of n, L by POLYNOM1:def 11;

            u9 is_monic_wrt T by A4, A21;

            then

             A22: ( HC (u9,T)) = ( 1. L);

            ( 1. L) <> ( 0. L);

            hence u is Polynomial of n, L & u <> ( 0_ (n,L)) by A22, TERMORD: 17;

          end;

        end;

        hence u is Polynomial of n, L & u <> ( 0_ (n,L));

      end;

      ( PolyRedRel (G,T)) is locally-confluent by A1;

      then for f be Polynomial of n, L st f in (G -Ideal ) holds ( PolyRedRel (G,T)) reduces (f,( 0_ (n,L))) by Th15;

      then for f be non-zero Polynomial of n, L st f in (G -Ideal ) holds f is_reducible_wrt (G,T) by Th16;

      then

       A23: for f be non-zero Polynomial of n, L st f in (G -Ideal ) holds f is_top_reducible_wrt (G,T) by Th17;

      

       A24: for u be Polynomial of n, L st u in G or u in H holds ( HC (u,T)) = ( 1. L) by Def6, A2, A4;

       A25:

      now

        let u be set;

        assume

         A26: u in GH;

        then not u in (G /\ H) by XBOOLE_0:def 5;

        then

         A27: not u in G or not u in H by XBOOLE_0:def 4;

        

         A28: u in (G \/ H) by A26, XBOOLE_0:def 5;

        now

          per cases by A28, XBOOLE_0:def 3;

            case u in G;

            hence u in (G \ H) by A27, XBOOLE_0:def 5;

          end;

            case u in H;

            hence u in (H \ G) by A27, XBOOLE_0:def 5;

          end;

        end;

        hence u in (G \ H) or u in (H \ G);

      end;

      now

        let u be object;

        assume

         A29: u in ((G \ H) \/ (H \ G));

        now

          per cases by A29, XBOOLE_0:def 3;

            case u in (G \ H);

            then u in G & not u in H by XBOOLE_0:def 5;

            hence u in (G \/ H) & not u in (G /\ H) by XBOOLE_0:def 3, XBOOLE_0:def 4;

          end;

            case u in (H \ G);

            then u in H & not u in G by XBOOLE_0:def 5;

            hence u in (G \/ H) & not u in (G /\ H) by XBOOLE_0:def 3, XBOOLE_0:def 4;

          end;

        end;

        hence u in GH by XBOOLE_0:def 5;

      end;

      then

       A30: GH = ((G \ H) \/ (H \ G)) by A9, TARSKI: 2;

      ( PolyRedRel (H,T)) is locally-confluent by A3;

      then for f be Polynomial of n, L st f in (H -Ideal ) holds ( PolyRedRel (H,T)) reduces (f,( 0_ (n,L))) by Th15;

      then for f be non-zero Polynomial of n, L st f in (H -Ideal ) holds f is_reducible_wrt (H,T) by Th16;

      then

       A31: for f be non-zero Polynomial of n, L st f in (H -Ideal ) holds f is_top_reducible_wrt (H,T) by Th17;

      per cases by A25, A14;

        suppose

         A32: g in (G \ H);

        then

         A33: g in G by XBOOLE_0:def 5;

        then

         A34: g <> ( 0_ (n,L)) by A17;

        then

        reconsider g as non-zero Polynomial of n, L by POLYNOM7:def 1;

        

         A35: G c= (G -Ideal ) by IDEAL_1:def 14;

        then ( HT (g,T)) in ( HT ((H -Ideal ),T)) by A16, A5, A33, A34;

        then

        consider b9 be bag of n such that

         A36: b9 in ( HT (H,T)) and

         A37: b9 divides ( HT (g,T)) by A31, Th18;

        consider h be Polynomial of n, L such that

         A38: b9 = ( HT (h,T)) and

         A39: h in H and

         A40: h <> ( 0_ (n,L)) by A36;

        reconsider h as non-zero Polynomial of n, L by A40, POLYNOM7:def 1;

        set f = (g - h);

        

         A41: h <> g by A32, A39, XBOOLE_0:def 5;

         A42:

        now

          assume

           A43: f = ( 0_ (n,L));

          h = (( 0_ (n,L)) + h) by POLYRED: 2

          .= ((g + ( - h)) + h) by A43, POLYNOM1:def 7

          .= (g + (( - h) + h)) by POLYNOM1: 21

          .= (g + ( 0_ (n,L))) by POLYRED: 3;

          hence contradiction by A41, POLYNOM1: 23;

        end;

        ( Support g) <> {} by A34, POLYNOM7: 1;

        then ( HT (g,T)) in ( Support g) by TERMORD:def 6;

        then

         A44: g is_reducible_wrt (h,T) by A37, A38, POLYRED: 36;

        then

         A45: ex r be Polynomial of n, L st g reduces_to (r,h,T) by POLYRED:def 8;

        now

          assume not h in (H \ G);

          then

           A46: h in G by A39, XBOOLE_0:def 5;

           not h in {g} by A41, TARSKI:def 1;

          then h in (G \ {g}) by A46, XBOOLE_0:def 5;

          then

          consider r be Polynomial of n, L such that

           A47: h in (G \ {g}) & g reduces_to (r,h,T) by A45;

          

           A48: g reduces_to (r,(G \ {g}),T) by A47, POLYRED:def 7;

          g is_irreducible_wrt ((G \ {g}),T) by A2, A33;

          hence contradiction by A48, POLYRED:def 9;

        end;

        then h in GH by A30, XBOOLE_0:def 3;

        then g <= (h,T) by A15;

        then not h < (g,T) by POLYRED: 29;

        then not ( HT (h,T)) < (( HT (g,T)),T) by POLYRED: 32;

        then

         A49: ( HT (g,T)) <= (( HT (h,T)),T) by TERMORD: 5;

        ( HT (h,T)) <= (( HT (g,T)),T) by A44, Th9;

        then

         A50: ( HT (h,T)) = ( HT (g,T)) by A49, TERMORD: 7;

        reconsider f as non-zero Polynomial of n, L by A42, POLYNOM7:def 1;

        ( Support f) <> {} by A42, POLYNOM7: 1;

        then

         A51: ( HT (f,T)) in ( Support f) by TERMORD:def 6;

        (f . ( HT (g,T))) = ((g + ( - h)) . ( HT (g,T))) by POLYNOM1:def 7

        .= ((g . ( HT (g,T))) + (( - h) . ( HT (g,T)))) by POLYNOM1: 15

        .= ((g . ( HT (g,T))) + ( - (h . ( HT (h,T))))) by A50, POLYNOM1: 17

        .= (( HC (g,T)) + ( - (h . ( HT (h,T))))) by TERMORD:def 7

        .= (( HC (g,T)) + ( - ( HC (h,T)))) by TERMORD:def 7

        .= (( 1. L) + ( - ( HC (h,T)))) by A24, A33

        .= (( 1. L) + ( - ( 1. L))) by A24, A39

        .= ( 0. L) by RLVECT_1: 5;

        then

         A52: ( HT (f,T)) <> ( HT (g,T)) by A51, POLYNOM1:def 4;

        ( HT (f,T)) <= (( max (( HT (g,T)),( HT (h,T)),T)),T) by Th7;

        then

         A53: ( HT (f,T)) <= (( HT (g,T)),T) by A50, TERMORD: 12;

        reconsider g9 = g, h9 = h as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        reconsider g9, h9 as Element of ( Polynom-Ring (n,L));

        H c= (H -Ideal ) by IDEAL_1:def 14;

        then (g9 - h9) in I by A16, A5, A33, A35, A39, IDEAL_1: 15;

        then f in I by Lm2;

        then

         A54: ( HT (f,T)) in ( HT (I,T)) by A42;

        ( Support (g + ( - h))) c= (( Support g) \/ ( Support ( - h))) by POLYNOM1: 20;

        then ( Support f) c= (( Support g) \/ ( Support ( - h))) by POLYNOM1:def 7;

        then

         A55: ( Support f) c= (( Support g) \/ ( Support h)) by Th5;

        now

          per cases by A51, A55, XBOOLE_0:def 3;

            case

             A56: ( HT (f,T)) in ( Support g);

            consider b9 be bag of n such that

             A57: b9 in ( HT (G,T)) and

             A58: b9 divides ( HT (f,T)) by A16, A23, A54, Th18;

            consider q be Polynomial of n, L such that

             A59: b9 = ( HT (q,T)) and

             A60: q in G and

             A61: q <> ( 0_ (n,L)) by A57;

            reconsider q as non-zero Polynomial of n, L by A61, POLYNOM7:def 1;

            g is_reducible_wrt (q,T) by A56, A58, A59, POLYRED: 36;

            then

            consider r be Polynomial of n, L such that

             A62: g reduces_to (r,q,T) by POLYRED:def 8;

            ( HT (q,T)) <= (( HT (f,T)),T) by A58, A59, TERMORD: 10;

            then q <> g by A53, A52, TERMORD: 7;

            then not q in {g} by TARSKI:def 1;

            then q in (G \ {g}) by A60, XBOOLE_0:def 5;

            then g reduces_to (r,(G \ {g}),T) by A62, POLYRED:def 7;

            then g is_reducible_wrt ((G \ {g}),T) by POLYRED:def 9;

            hence contradiction by A2, A33;

          end;

            case

             A63: ( HT (f,T)) in ( Support h);

            consider b9 be bag of n such that

             A64: b9 in ( HT (H,T)) and

             A65: b9 divides ( HT (f,T)) by A5, A31, A54, Th18;

            consider q be Polynomial of n, L such that

             A66: b9 = ( HT (q,T)) and

             A67: q in H and

             A68: q <> ( 0_ (n,L)) by A64;

            reconsider q as non-zero Polynomial of n, L by A68, POLYNOM7:def 1;

            h is_reducible_wrt (q,T) by A63, A65, A66, POLYRED: 36;

            then

            consider r be Polynomial of n, L such that

             A69: h reduces_to (r,q,T) by POLYRED:def 8;

            ( HT (q,T)) <= (( HT (f,T)),T) by A65, A66, TERMORD: 10;

            then q <> h by A50, A53, A52, TERMORD: 7;

            then not q in {h} by TARSKI:def 1;

            then q in (H \ {h}) by A67, XBOOLE_0:def 5;

            then h reduces_to (r,(H \ {h}),T) by A69, POLYRED:def 7;

            then h is_reducible_wrt ((H \ {h}),T) by POLYRED:def 9;

            hence contradiction by A4, A39;

          end;

        end;

        hence thesis;

      end;

        suppose

         A70: g in (H \ G);

        then

         A71: not g in G by XBOOLE_0:def 5;

        

         A72: g in H by A70, XBOOLE_0:def 5;

        then

         A73: g <> ( 0_ (n,L)) by A17;

        then

        reconsider g as non-zero Polynomial of n, L by POLYNOM7:def 1;

        

         A74: H c= (H -Ideal ) by IDEAL_1:def 14;

        then ( HT (g,T)) in ( HT ((G -Ideal ),T)) by A16, A5, A72, A73;

        then

        consider b9 be bag of n such that

         A75: b9 in ( HT (G,T)) and

         A76: b9 divides ( HT (g,T)) by A23, Th18;

        consider h be Polynomial of n, L such that

         A77: b9 = ( HT (h,T)) and

         A78: h in G and

         A79: h <> ( 0_ (n,L)) by A75;

        reconsider h as non-zero Polynomial of n, L by A79, POLYNOM7:def 1;

        set f = (g - h);

         A80:

        now

          assume

           A81: f = ( 0_ (n,L));

          h = (( 0_ (n,L)) + h) by POLYRED: 2

          .= ((g + ( - h)) + h) by A81, POLYNOM1:def 7

          .= (g + (( - h) + h)) by POLYNOM1: 21

          .= (g + ( 0_ (n,L))) by POLYRED: 3;

          hence contradiction by A71, A78, POLYNOM1: 23;

        end;

        ( Support g) <> {} by A73, POLYNOM7: 1;

        then ( HT (g,T)) in ( Support g) by TERMORD:def 6;

        then

         A82: g is_reducible_wrt (h,T) by A76, A77, POLYRED: 36;

        then

         A83: ex r be Polynomial of n, L st g reduces_to (r,h,T) by POLYRED:def 8;

        now

          assume not h in (G \ H);

          then

           A84: h in H by A78, XBOOLE_0:def 5;

           not h in {g} by A71, A78, TARSKI:def 1;

          then h in (H \ {g}) by A84, XBOOLE_0:def 5;

          then

          consider r be Polynomial of n, L such that

           A85: h in (H \ {g}) & g reduces_to (r,h,T) by A83;

          

           A86: g reduces_to (r,(H \ {g}),T) by A85, POLYRED:def 7;

          g is_irreducible_wrt ((H \ {g}),T) by A4, A72;

          hence contradiction by A86, POLYRED:def 9;

        end;

        then h in GH by A30, XBOOLE_0:def 3;

        then g <= (h,T) by A15;

        then not h < (g,T) by POLYRED: 29;

        then not ( HT (h,T)) < (( HT (g,T)),T) by POLYRED: 32;

        then

         A87: ( HT (g,T)) <= (( HT (h,T)),T) by TERMORD: 5;

        ( HT (h,T)) <= (( HT (g,T)),T) by A82, Th9;

        then

         A88: ( HT (h,T)) = ( HT (g,T)) by A87, TERMORD: 7;

        reconsider f as non-zero Polynomial of n, L by A80, POLYNOM7:def 1;

        ( Support f) <> {} by A80, POLYNOM7: 1;

        then

         A89: ( HT (f,T)) in ( Support f) by TERMORD:def 6;

        (f . ( HT (g,T))) = ((g + ( - h)) . ( HT (g,T))) by POLYNOM1:def 7

        .= ((g . ( HT (g,T))) + (( - h) . ( HT (g,T)))) by POLYNOM1: 15

        .= ((g . ( HT (g,T))) + ( - (h . ( HT (h,T))))) by A88, POLYNOM1: 17

        .= (( HC (g,T)) + ( - (h . ( HT (h,T))))) by TERMORD:def 7

        .= (( HC (g,T)) + ( - ( HC (h,T)))) by TERMORD:def 7

        .= (( 1. L) + ( - ( HC (h,T)))) by A24, A72

        .= (( 1. L) + ( - ( 1. L))) by A24, A78

        .= ( 0. L) by RLVECT_1: 5;

        then

         A90: ( HT (f,T)) <> ( HT (g,T)) by A89, POLYNOM1:def 4;

        ( HT (f,T)) <= (( max (( HT (g,T)),( HT (h,T)),T)),T) by Th7;

        then

         A91: ( HT (f,T)) <= (( HT (g,T)),T) by A88, TERMORD: 12;

        reconsider g9 = g, h9 = h as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

        reconsider g9, h9 as Element of ( Polynom-Ring (n,L));

        G c= (G -Ideal ) by IDEAL_1:def 14;

        then (g9 - h9) in I by A16, A5, A72, A74, A78, IDEAL_1: 15;

        then f in I by Lm2;

        then

         A92: ( HT (f,T)) in ( HT (I,T)) by A80;

        ( Support (g + ( - h))) c= (( Support g) \/ ( Support ( - h))) by POLYNOM1: 20;

        then ( Support f) c= (( Support g) \/ ( Support ( - h))) by POLYNOM1:def 7;

        then

         A93: ( Support f) c= (( Support g) \/ ( Support h)) by Th5;

        now

          per cases by A89, A93, XBOOLE_0:def 3;

            case

             A94: ( HT (f,T)) in ( Support g);

            consider b9 be bag of n such that

             A95: b9 in ( HT (H,T)) and

             A96: b9 divides ( HT (f,T)) by A5, A31, A92, Th18;

            consider q be Polynomial of n, L such that

             A97: b9 = ( HT (q,T)) and

             A98: q in H and

             A99: q <> ( 0_ (n,L)) by A95;

            reconsider q as non-zero Polynomial of n, L by A99, POLYNOM7:def 1;

            g is_reducible_wrt (q,T) by A94, A96, A97, POLYRED: 36;

            then

            consider r be Polynomial of n, L such that

             A100: g reduces_to (r,q,T) by POLYRED:def 8;

            ( HT (q,T)) <= (( HT (f,T)),T) by A96, A97, TERMORD: 10;

            then q <> g by A91, A90, TERMORD: 7;

            then not q in {g} by TARSKI:def 1;

            then q in (H \ {g}) by A98, XBOOLE_0:def 5;

            then g reduces_to (r,(H \ {g}),T) by A100, POLYRED:def 7;

            then g is_reducible_wrt ((H \ {g}),T) by POLYRED:def 9;

            hence contradiction by A4, A72;

          end;

            case

             A101: ( HT (f,T)) in ( Support h);

            consider b9 be bag of n such that

             A102: b9 in ( HT (G,T)) and

             A103: b9 divides ( HT (f,T)) by A16, A23, A92, Th18;

            consider q be Polynomial of n, L such that

             A104: b9 = ( HT (q,T)) and

             A105: q in G and

             A106: q <> ( 0_ (n,L)) by A102;

            reconsider q as non-zero Polynomial of n, L by A106, POLYNOM7:def 1;

            h is_reducible_wrt (q,T) by A101, A103, A104, POLYRED: 36;

            then

            consider r be Polynomial of n, L such that

             A107: h reduces_to (r,q,T) by POLYRED:def 8;

            ( HT (q,T)) <= (( HT (f,T)),T) by A103, A104, TERMORD: 10;

            then ( HT (q,T)) <> ( HT (h,T)) by A88, A91, A90, TERMORD: 7;

            then not q in {h} by TARSKI:def 1;

            then q in (G \ {h}) by A105, XBOOLE_0:def 5;

            then h reduces_to (r,(G \ {h}),T) by A107, POLYRED:def 7;

            then h is_reducible_wrt ((G \ {h}),T) by POLYRED:def 9;

            hence contradiction by A2, A78;

          end;

        end;

        hence thesis;

      end;

    end;